On Fri, Feb 10, 2006 at 01:41:03AM -0500, David Menendez wrote:
are very different. The first essentially takes two arguments, a type |a| and a value of type |a -> a|. The second takes a single argument of type |forall a. a -> a|.
There are some type systems (like JHC core, IIRC) which treat "forall" and "->" as special cases of the dependent product. That is, "T -> U" is short for "Pi _:T. U" and "forall a. T" is short for "Pi a:*. T". Using that syntax, the types above become:
Pi a:*. Pi _:(Pi _:a. a). Int
and
Pi _:(Pi a:*. Pi _:a. a). Int
Yup. that is exactly right. when pretty printing I show the pi's in a more human digestable form (foralls and function arrows), but internally they are all represented as Pi's. John -- John Meacham - ⑆repetae.net⑆john⑈