[jhc] darcs patch: Improve lambda/pi printing code

John Meacham john at repetae.net
Sat Apr 12 23:00:34 EDT 2008


On Sat, Apr 12, 2008 at 10:19:47PM -0400, Samuel Bronson wrote:
> >  the uppercase lambda is not valid for kinds other than *, actually, the
> >  uppercase lambda is just there to help people used to system F, there is
> >  no such thing in jhc core since PTS's 'pi' terms subsume explicit type
> >  application terms as well as functional types. papers on PTS's (pure
> >  type systems) such as the henk paper have more details on the difference
> >  between PTS's and system F.
> 
> Eh? How can it be invalid when uppercase lambda is just sugar for
> lowercase lambda? Henk paper didn't say anything about that...

Well, when I originally made the shorthand, I just wanted terms in
System F2 to look the same in jhc core. Since F2 doesn't have functions
at the type level, I made only * turn into a capital lambda. 

But I suppose it does make sense to expand the shorthand to higher
ordered types since jhc core is more powerful than system F2... so yeah,
expanding capital lambda to all kind terms does make sense. cool.

        John

-- 
John Meacham - ⑆repetae.net⑆john⑈


More information about the jhc mailing list