<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Jun 7, 2020, at 10:45 PM, Jake McArthur <<a href="mailto:jake.mcarthur@gmail.com" class="">jake.mcarthur@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class="">I don't actually know much about GHC's type checker itself, but I think it uses a form of bidirectional type checking. A bidirectional type checker has two modes:<div class=""><br class=""></div><div class="">infer :: Term -> Type</div><div class="">check :: Term -> Type -> Bool</div><div class=""><br class=""></div><div class="">The syntax is divided into two classes. The types for one of these classes can be inferred, but the other can only be checked. Given a type checkable term, you can create a type inferable term by giving it a type annotation. That is, `infer (x :: T) = check x T`.</div></div></div></blockquote><div><br class=""></div><div>Exactly so. (Well, those types aren't the types of the relevant functions within GHC, but they are are very useful approximation.) This is explained in a relatively accessible way here: <a href="https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/putting.pdf" class="">https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/putting.pdf</a> Bidirectional type checking is needed in order to check higher-rank types; a higher-rank type has a `forall` to the left of an arrow, like the type in `foo :: (forall a. a -> a) -> Int`.</div><br class=""><blockquote type="cite" class=""><div class=""><br class=""><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, Jun 7, 2020 at 4:19 PM Olaf Klinke <<a href="mailto:olf@aatal-apotheke.de" class="">olf@aatal-apotheke.de</a>> wrote:<br class=""></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">> f 0 x = 0<br class="">
> f 1 x = f 0 ()<br class="">
> f n x = f (n-1) 'a'<br class="">
<br class="">
That's very interesting, I learned something new about GHC today. I<br class="">
used to believe that my Haskell compiler always type checks<br class="">
declarations on its own, and after that unifies its result with the<br class="">
type declaration that I provide. Polymorphic recursion yields a case<br class="">
where the compiler's inference procedure is evidently not independent<br class="">
of my provided type declaration. Can the above be abused to compile<br class="">
programs containing false type declarations? (It seems the answer is<br class="">
no, but maybe I lack the fantasy.)<br class=""></blockquote></div></div></blockquote><div><br class=""></div><div>Interestingly, bidirectional type checking, in all its power, is not needed to support polymorphic recursion, which can get away with weaker propagation of types when checking terms. Also, as far as I know, this aspect of Haskell is not unique to GHC, but is included in Haskell 98 and should be supported by other compilers.</div><div><br class=""></div><div>Can this be abused? I hope not! :)</div><div><br class=""></div><div>Richard</div><br class=""><blockquote type="cite" class=""><div class=""><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<br class="">
Thanks,<br class="">
Olaf<br class="">
<br class="">
_______________________________________________<br class="">
Haskell-Cafe mailing list<br class="">
To (un)subscribe, modify options or view archives go to:<br class="">
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank" class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br class="">
Only members subscribed via the mailman list are allowed to post.</blockquote></div>
_______________________________________________<br class="">Haskell-Cafe mailing list<br class="">To (un)subscribe, modify options or view archives go to:<br class=""><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br class="">Only members subscribed via the mailman list are allowed to post.</div></blockquote></div><br class=""></body></html>