[Haskell-cafe] Generalization of types during inference

[Richard Eisenberg]

> On Jun 7, 2020, at 10:45 PM, Jake McArthur <jake.mcarthur at gmail.com> wrote:
> 
> 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:
> 
> infer :: Term -> Type
> check :: Term -> Type -> Bool
> 
> 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`.

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: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/putting.pdf   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`.

> 
> On Sun, Jun 7, 2020 at 4:19 PM Olaf Klinke <olf at aatal-apotheke.de <mailto:olf at aatal-apotheke.de>> wrote:
> > f 0 x = 0
> > f 1 x = f 0 ()
> > f n x = f (n-1) 'a'
> 
> That's very interesting, I learned something new about GHC today. I
> used to believe that my Haskell compiler always type checks
> declarations on its own, and after that unifies its result with the
> type declaration that I provide. Polymorphic recursion yields a case
> where the compiler's inference procedure is evidently not independent
> of my provided type declaration. Can the above be abused to compile
> programs containing false type declarations? (It seems the answer is
> no, but maybe I lack the fantasy.)

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.

Can this be abused? I hope not! :)

Richard

> 
> Thanks,
> Olaf
> 
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe <http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe>
> Only members subscribed via the mailman list are allowed to post.
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200608/59121918/attachment.html>