[ghc-steering-committee] Discussion on #155 Type Variable in Labmdas

[Richard Eisenberg]

> On Mar 5, 2019, at 11:34 AM, Simon Peyton Jones <simonpj at microsoft.com> wrote:
> 
> I haven't thought through the consequences of this fully, but it does seem plausible.
>  
> It says we must generalise over some ‘a’, but which ‘a’?  What type does (\@a (\x. x)) have?

My understanding of Eric's idea is that GHC would give (\x.x) the type (alpha -> alpha), as usual. Then (\ @a (\x.x)) gets the type forall a. alpha -> alpha. Later, we might solve for alpha or generalize over it, perhaps leading a type like forall b a. b -> b.

> But someone would need to write down a type system.

I agree here. I think we'd need more Medium Thought (not quite Hard Thought) before committing to this plan, but it still seems plausible.

Richard
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20190305/79494277/attachment.html>