在GADT上使用翻译解释器

几周前，我读了Writing an interpreter using fold。我尝试将这种方法应用到我正在处理的项目上，但由于GADT存在错误。这是产生相同问题的玩具代码。在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 [email protected](Alg val _) (Val n) = val n 
fold [email protected](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 [email protected](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中具有全量化类型变量，并且类型签名必须处理特定信息。

+这里是原代码

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 [email protected](FormA prim _ _ _) (Prim p m) = prim p m 
foldForm [email protected](FormA _ simple _ _) (Simple p m) = simple p m 
foldForm [email protected](FormA _ _ derived _) (Derived f s) = 
    derived (foldForm alg f) s 
foldForm [email protected](FormA _ _ _ complex) (Complex f1 i f2) = 
    complex (foldForm alg f1) i (foldForm alg f2)

来源

2017-02-18 Mossid

正确的定义是'Alg ::（n - > a） - > ... - > Alg n a' - 类型'存在n。 n - > a'与'a'是同构的，因为你可以用函数做的唯一事情就是应用它，但你对'n'类型一无所知，所以你只能将这个函数应用到'undefined'。但似乎你知道这一点 - “所以答案可能是提升内部变量的数据类型签名”。 “但是，不像在这个例子中，它不能用在原始代码上” - 那么它就是你应该发布的原始代码。 – user2407038

为了确保内部Alg的n是正确的，可以公开它作为一个参数传递给Alg类型构造。

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

fold :: Alg n a -> Expr n -> a 
fold [email protected](Alg val _) (Val n) = val n 
fold [email protected](Alg _ plus) (Plus n1 n2) = plus (fold alg n1) (fold alg n2)

在Form代码中，这看起来更难。那里有很多存在量化的类型变量。我们需要找到一种方法来揭露这些类型中的所有人，这样他们可以被要求在Form和FormA中相同。

来源

2017-02-18 09:52:26 chi

在GADT上使用翻译解释器

回答

相关问题