Re: [Haskell-cafe] translation between two flavors of lexically-scoped type variables
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 - G Int GB :: Bool - G Bool evG :: G a - a evG (GI x) = x evG (GB x) = x To type check the first clause of evG, we assume the equality (a ~ Int) for the duration of type checking the clause. To type-check the second clause, we assume the equality (a ~ Bool) for the clause. We sort of assumed that a is universally quantified, so we may indeed think that it could reasonably be an Int or a Bool. Now consider that evG above was actually a part of a larger function foo = ... where evG :: G a - a evG (GI x) = x evG (GB x) = x bar x = ... x :: Int ... x::a ... We were happily typechecking evG thinking that a is universally quantified when in fact it wasn't. And some later in the code it is revealed that a is actually an Int. Now, one of our assumptions, a ~ Bool (which we used to typecheck the second clause of evG) no longer makes sense. One can say that logically, from the point of view of _material implication_, this is not a big deal. If a is Int, the GB clause of evG can never be executed. So, there is no problem here. This argument is akin to saying that in the code let x = any garbage in 1 any garbage will never be evaluated, so we just let it to be garbage. People don't buy this argument. For the same reason, GHC refuses to type check the following evG1 :: G Int - Int evG1 (GI x) = x evG1 (GB x) = x Thus, modular type checking of GADTs requires us to differentiate between schematic variables (which are akin to `logical' variables, free at one time and bound some time later) and quantified variables, which GHC calls `rigid' variables, which can't become bound (within the scope of the quantifier). For simplicity, GHC just banned schematic variables. The same story is now played in OCaml, only banning of the old type variables was out of the question to avoid breaking a lot of code. GADTs forced the introduction of rigid variables, which are syntactically distinguished from the old, schematic type variables. We thus have two type variables: schematic 'a and rigid a (the latter unfortunately look exactly like type constants, but they are bound by the `type' keyword). There are interesting and sometimes confusing interactions between the two. OCaml 4 will be released any hour now. It is interesting to see how the interaction of the two type variables plays out in practice. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] translation between two flavors of lexically-scoped type variables
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 what looks like a
type-lambda, the occurrences of that type lambda are greatly
restricted. It may only come at the beginning of a polymorphic
definition (it cannot occur in an argument, for example).
data Ap = forall a. Ap [a] ([a] - Int)
Why isn't it possible to write something like:
fun 'a revap (Ap (xs : 'a list) f) = f ys
where
ys :: 'a list
ys = reverse xs
in SML?
This looks like a polymorphic function: an expression of the form
/\a.body has the type forall a. type. However, the Haskell function
revap :: Ap - Int
revap (Ap (xs :: [a]) f) = f ys
where
ys :: [a]
ys = reverse xs
you meant to emulate is not polymorphic. Both Ap and Int are concrete
types. Therefore, your SML code cannot correspond to the Haskell code.
That does not mean we can't use SML-style type variables (which must
be forall-bound) with existentials. We have to write the
elimination principle for existentials explicitly
{-# LANGUAGE ExistentialQuantification, RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
data Ap = forall a. Ap [a] ([a] - Int)
-- Elimination principle
deconAp :: Ap - (forall a. [a] - ([a] - Int) - w) - w
deconAp (Ap xs f) k = k xs f
revap :: Ap - Int
revap ap = deconAp ap revap'
revap' :: forall a. [a] - ([a] - Int) - Int
revap' xs f = f ys
where
ys :: [a]
ys = reverse xs
Incidentally, GHC now uses SML-like design for type
variables. However, there is a special exception for
existentials. Please see
7.8.7.4. Pattern type signatures
of the GHC user manual. The entire section 7.8.7 is worth reading.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] translation between two flavors of lexically-scoped type variables
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, o...@okmij.org 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 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 what looks like a
type-lambda, the occurrences of that type lambda are greatly
restricted. It may only come at the beginning of a polymorphic
definition (it cannot occur in an argument, for example).
data Ap = forall a. Ap [a] ([a] - Int)
Why isn't it possible to write something like:
fun 'a revap (Ap (xs : 'a list) f) = f ys
where
ys :: 'a list
ys = reverse xs
in SML?
This looks like a polymorphic function: an expression of the form
/\a.body has the type forall a. type. However, the Haskell function
revap :: Ap - Int
revap (Ap (xs :: [a]) f) = f ys
where
ys :: [a]
ys = reverse xs
you meant to emulate is not polymorphic. Both Ap and Int are concrete
types. Therefore, your SML code cannot correspond to the Haskell code.
That does not mean we can't use SML-style type variables (which must
be forall-bound) with existentials. We have to write the
elimination principle for existentials explicitly
{-# LANGUAGE ExistentialQuantification, RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
data Ap = forall a. Ap [a] ([a] - Int)
-- Elimination principle
deconAp :: Ap - (forall a. [a] - ([a] - Int) - w) - w
deconAp (Ap xs f) k = k xs f
revap :: Ap - Int
revap ap = deconAp ap revap'
revap' :: forall a. [a] - ([a] - Int) - Int
revap' xs f = f ys
where
ys :: [a]
ys = reverse xs
Incidentally, GHC now uses SML-like design for type
variables. However, there is a special exception for
existentials. Please see
7.8.7.4. Pattern type signatures
of the GHC user manual. The entire section 7.8.7 is worth reading.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] translation between two flavors of lexically-scoped type variables
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 existential quantification in addition to universal quantification. As an example, they give this code: data Ap = forall a. Ap [a] ([a] - Int) The constructor `Ap` has the type: Ap :: forall a. [a] - ([a] - Int) - Ap And one can write a function: revap :: Ap - Int revap (Ap (xs :: [a]) f) = f ys where ys :: [a] ys = reverse xs with the annotations on `xs` and `ys` being existential instead of universal. But I'm a little confused about *why* type-lambdas don't allow this. Aren't both Haskell and SML translatable into System F, from which type-lambda is directly taken? What does the translation for the above code even look like? Why isn't it possible to write something like: fun 'a revap (Ap (xs : 'a list) f) = f ys where ys :: 'a list ys = reverse xs in SML? -Kangyuan Niu ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
