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

Samuel Bronson 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 mailing list