在 GADT 上使用折叠解释器答案

【问题标题】：Using fold-interpreter on GADT在 GADT 上使用折叠解释器
【发布时间】：2017-02-18 05:33:32
【问题描述】：

几周前，我读到了Writing an interpreter using fold。我尝试将此方法应用于我正在处理的项目，但由于 GADT 出现错误。这是产生同样问题的玩具代码。

{-# LANGUAGE GADTs, KindSignatures #-} 


data Expr :: * -> * where
    Val  :: n ->                Expr n
    Plus :: Expr n -> Expr n -> Expr n

data Alg :: * -> * where
    Alg :: (n ->      a) 
        -> (a -> a -> a) 
        -> Alg a

fold :: Alg a -> Expr n -> a
fold alg@(Alg val _) (Val n) = val n
fold alg@(Alg _ plus) (Plus n1 n2) = plus (fold alg n1) (fold alg n2)

这是错误信息。

/home/mossid/Code/Temforai/src/Temforai/Example.hs:16:36: error:
    • Couldn't match expected type ‘n1’ with actual type ‘n’
      ‘n’ is a rigid type variable bound by
        the type signature for:
          fold :: forall a n. Alg a -> Expr n -> a
        at /home/mossid/Code/Temforai/src/Temforai/Example.hs:15:9
      ‘n1’ is a rigid type variable bound by
        a pattern with constructor:
          Alg :: forall a n. (n -> a) -> (a -> a -> a) -> Alg a,
        in an equation for ‘fold’
        at /home/mossid/Code/Temforai/src/Temforai/Example.hs:16:11
    • In the first argument of ‘val’, namely ‘n’
      In the expression: val n
      In an equation for ‘fold’: fold alg@(Alg val _) (Val n) = val n
    • Relevant bindings include
        n :: n
          (bound at /home/mossid/Code/Temforai/src/Temforai/Example.hs:16:27)
        val :: n1 -> a
          (bound at /home/mossid/Code/Temforai/src/Temforai/Example.hs:16:15)
        fold :: Alg a -> Expr n -> a
          (bound at /home/mossid/Code/Temforai/src/Temforai/Example.hs:16:1)

我认为编译器无法推断出n 和n1 是相同的类型，因此答案可能是将内部变量提升为数据类型的签名。但是，与此示例不同，它不能用于原始代码。原始代码在Expr 中有forall-quantified 类型变量，类型签名必须处理特定信息。

+ 这是原始代码

data Form :: * -> * where
    Var     :: Form s
    Prim    :: (Sat s r) => Pred s -> Marker r          -> Form s
    Simple  :: (Sat s r) => Pred s -> Marker r          -> Form s
    Derived ::              Form r -> Suffix r s        -> Form s
    Complex :: (Sat s r, Sat t P) => 
                            Form s -> Infix r -> Form t -> Form s

data FormA a where
    FormA :: (Pred s -> Marker t -> a) 
          -> (Pred u -> Marker v -> a)
          -> (a -> Suffix w x    -> a)
          -> (a -> y -> a        -> a)
          -> FormA a

foldForm :: FormA a -> Form s -> a
foldForm alg@(FormA prim _ _ _) (Prim p m) = prim p m
foldForm alg@(FormA _ simple _ _) (Simple p m) = simple p m
foldForm alg@(FormA _ _ derived _) (Derived f s) = 
    derived (foldForm alg f) s
foldForm alg@(FormA _ _ _ complex) (Complex f1 i f2) = 
    complex (foldForm alg f1) i (foldForm alg f2)

【问题讨论】：

正确的定义是 Alg :: (n -> a) -> ... -> Alg n a - exists n . n -> a 类型与 a 同构，因为你可以对函数做的唯一事情就是应用它，但你对 @987654331 类型一无所知@，所以你只能将此函数应用于undefined。但是您似乎意识到了这一点-“因此答案可能是将内部变量提升为数据类型的签名”。 “但是，与此示例不同，它不能用于原始代码” - 那么它是您应该发布的原始代码。

标签： haskell gadt

【解决方案1】：

为确保Alg 中的n 是正确的，您可以将其作为参数公开给Alg 类型的构造函数。

data Alg :: * -> * -> * where
    Alg :: (n ->      a) 
        -> (a -> a -> a) 
        -> Alg n a

fold :: Alg n a -> Expr n -> a
fold alg@(Alg val _) (Val n) = val n
fold alg@(Alg _ plus) (Plus n1 n2) = plus (fold alg n1) (fold alg n2)

在Form 代码中，这看起来更难。那里有很多存在量化的类型变量。需要找到一种方法在类型中公开所有它们，以便在 Form 和 FormA 中要求它们相同。

【讨论】：