[jhc] darcs patch: Improve lambda/pi printing code
naesten at gmail.com
Sun Apr 13 12:38:27 EDT 2008
On Sat, Apr 12, 2008 at 11:00 PM, John Meacham <john at repetae.net> wrote:
> 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.
But as I said, I accidentally suppressed the kind printing at the same time...
More information about the jhc