GADTs但不存在量化的问题。

Question

以下包含存在型的代码不能编译

{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}
module TestGadt () where

-- |Symbol only for arithmetic
data ArithSym = AInt Int | ASym String
-- |Symbol for arithmetic or strings or anything else
data GSym x = GInt Int | GStr String | GOther x
data Expr x = EAdd (Expr x) (Expr x) | E0 x deriving Functor
-- |Concatenate the string literals
concatStrings :: Expr (GSym x)  -> Expr (GSym x)
concatStrings = undefined
-- |Add the integer literals
addInts :: Expr (GSym x)  -> Expr (GSym x)
addInts = undefined
-- |Do some transform according to the sizes
otherOpt :: (e -> Int) -> Expr e  -> Expr e
otherOpt symSize = undefined


-- |Configuration to optimize an expression with symbols of type e.
data OptConfig e = OptConfig {
  ocSymSize :: e -> Int,
  ocGSymIso :: forall e0 . (e -> GSym e0,GSym e0 -> e)
  -- ^ this should be existential
  }

-- |Optimize given the configuration
opt :: OptConfig e -> Expr e -> Expr e
opt oc =
  otherOpt (ocSymSize oc)
  . fmap (snd $ ocGSymIso oc)
  . addInts
  . concatStrings
  . fmap (fst $ ocGSymIso oc)


arithConfig32 :: OptConfig ArithSym
arithConfig32 = OptConfig {
  ocSymSize=const 4,
  ocGSymIso=(\case{AInt i -> GInt i;ASym s -> GOther s},
             \case {GInt i -> AInt i;GOther a -> ASym a;_-> error "unreachable"})
  -- XXX: ^ ""Couldn't match type ‘e0’ with ‘String’"" even though e0
  -- should be existential!
  }

arithOpt :: Expr ArithSym -> Expr ArithSym
arithOpt = opt arithConfig32

但如果我把存在式改成GADT，它就会。

{-# LANGUAGE GADTs #-}
[...]

-- |Configuration to optimize an expression with symbols of type e.
data OptConfig e = OptConfig {
  ocSymSize :: e -> Int,
  ocGSymIso0 :: GIso e
  -- ^ this should be existential
  }
data GIso e where
  GIso :: (e -> GSym e0,GSym e0 -> e) -> GIso e

-- |Optimize given the configuration
opt :: OptConfig e -> Expr e -> Expr e
opt oc = case ocGSymIso0 oc of
  GIso (fromE,toE) ->
    otherOpt (ocSymSize oc)
    . fmap toE
    . addInts
    . concatStrings
    . fmap fromE


arithConfig32 :: OptConfig ArithSym
arithConfig32 = OptConfig {
  ocSymSize=const 4,
  ocGSymIso0=GIso
    (\case{AInt i -> GInt i;ASym s -> GOther s},
     \case {GInt i -> AInt i;GOther a -> ASym a;_-> error "unreachable"})
  -- XXX: It works now?
  }

[...]

谁能给我解释一下，为什么一个键入检查而另一个不检查？

Answer 1

后者是一个存在式，但前者不是：它是一个普遍的量化，而不是。

注意构造函数的类型。

-- first definition
OptConfig :: forall e. (e -> Int) -> (forall e0 . (e -> GSym e0,GSym e0 -> e))
          -> OptConfig e
-- second definition
OptConfig :: forall e e0. (e -> Int) -> (e -> GSym e0,GSym e0 -> e)
          -> OptConfig e

语句的位置 forall e0 不同，改变了量化符的有效含义，从普遍性变为存在性。

如果你不想使用GADT语法(我更倾向于使用GADT语法)，可以试试这个符号。

-- |Configuration to optimize an expression with symbols of type e.
data OptConfig e = forall e0 . OptConfig {
  ocSymSize :: e -> Int,
  ocGSymIso :: (e -> GSym e0,GSym e0 -> e)
  -- ^ this should be existential
  }