GADTで折りたたみ通訳を使用する

Question

数週間前、私は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型変数を持ち、型シグネチャは特定の情報を処理する必要があります。

+ここでは、あなたがAlg型コンストラクタにパラメータとして、それを公開することができ、Alg内部nが正しいものであることを確認するには、元のコード

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) 

Answer 1

です。

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で同じである必要があります。