GADT 但不是存在量化

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 语法（我更喜欢），请尝试使用此表示法：

-- |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
  }

GADT 但不是存在量化

GADTs but not existential quantification

haskell

existential-type

gadt