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.
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,
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.
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.
participants (2)
-
Kangyuan Niu -
oleg＠okmij.org