Re: [Haskell-cafe] translation between two flavors of lexically-scoped type variables

2012-07-07 Thread oleg
> Do you know why they switched over in GHC 6.6? If I were to speculate, I'd say it is related to GADTs. Before GADTs, we can keep conflating quantified type variables with schematic type variables. GADTs seem to force us to make the distinction. Consider this code: data G a where GI :: Int

Re: [Haskell-cafe] translation between two flavors of lexically-scoped type variables

2012-07-06 Thread Kangyuan Niu
Thanks, I think I understand it now. Do you know why they switched over in GHC 6.6? -Kangyuan Niu On Fri, Jul 6, 2012 at 3:11 AM, wrote: > > Kangyuan Niu wrote: > > Aren't both Haskell and SML translatable into System F, from which > > type-lambda is directly taken? > > The fact that both Hask

Re: [Haskell-cafe] translation between two flavors of lexically-scoped type variables

2012-07-06 Thread oleg
Kangyuan Niu wrote: > Aren't both Haskell and SML translatable into System F, from which > type-lambda is directly taken? The fact that both Haskell and SML are translatable to System F does not imply that Haskell and SML are just as expressive as System F. Although SML (and now OCaml) does have

[Haskell-cafe] translation between two flavors of lexically-scoped type variables

2012-07-05 Thread Kangyuan Niu
The paper "Lexically scoped type variables" by Simon Peyton Jones and Mark Shields describes two ways to give type variables lexical scoping. They state that one of the advantages of the GHC-style type-sharing approach over the SML-style type-lambda approach is that the former allows for existentia