darcs patch: Improve lambda/pi printing code
Fri Apr 11 19:01:59 EDT 2008 Samuel Bronson
On 4/11/08, Samuel Bronson
Fri Apr 11 19:01:59 EDT 2008 Samuel Bronson
* Improve lambda/pi printing code Only only put as many lambda/pi abstractions on a line as will fit. Use sortKindLike to get the uppercase lambdas for type variables of kind other than *. (For instance, * -> *.)
Hmm. I accidentally disabled kind-printing in doing this... so don't apply this.
On Fri, Apr 11, 2008 at 07:20:33PM -0400, Samuel Bronson wrote:
Fri Apr 11 19:01:59 EDT 2008 Samuel Bronson
* Improve lambda/pi printing code Only only put as many lambda/pi abstractions on a line as will fit. Use sortKindLike to get the uppercase lambdas for type variables of kind other than *. (For instance, * -> *.)
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. John -- John Meacham - ⑆repetae.net⑆john⑈
On Sat, Apr 12, 2008 at 8:53 PM, John Meacham
On Fri, Apr 11, 2008 at 07:20:33PM -0400, Samuel Bronson wrote:
Fri Apr 11 19:01:59 EDT 2008 Samuel Bronson
* Improve lambda/pi printing code Only only put as many lambda/pi abstractions on a line as will fit. Use sortKindLike to get the uppercase lambdas for type variables of kind other than *. (For instance, * -> *.) 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...
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⑈
On Sat, Apr 12, 2008 at 11:00 PM, John Meacham
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...
participants (2)
-
John Meacham -
Samuel Bronson