在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上使用翻譯解釋器

回答

相關問題