假设我有一个像这样的 GADT:
data Term a where
Lit :: a -> Term a
Succ :: Term Int -> Term Int
IsZero :: Term Int -> Term Bool
If :: Term Bool -> Term a -> Term a -> Term a
能否将 Succ (Lit 2)
和 IsZero (Succ (Lit 2))
存储在 State monad transformer 中,作为内部状态的值?
问题在于这两个值的类型不同,我不知道 StateT s m a
中的 s
应该如何被编写。
编辑:ATerm 解决了如何在状态中存储不同 GADT 的初始问题,现在的问题是由于类型丢失,似乎无法比较旧状态和新状态。
编辑:最终答案。
与 @luqui 反复讨论后,这里是完整的代码片段,可以回答这个问题。
请随意 fork 这个 repl 并尝试。
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
import Data.Typeable
data Term a where
Lit :: a -> Term a
Succ :: Term Int -> Term Int
IsZero :: Term Int -> Term Bool
If :: Term Bool -> Term a -> Term a -> Term a
deriving instance (Eq a) => Eq (Term a)
data ATerm where
ATerm :: (Typeable a, Eq a) => Term a -> ATerm
instance Eq ATerm where
ATerm t == ATerm u
| Just t' <- cast t = t' == u
| otherwise = False
main :: IO ()
main = return ()
Lit
构造函数上,您不应该需要Typeable a
约束。 - dfeuerEq
约束条件放在那里,并从ATerm
构造函数中删除两个约束条件。示例 - dfeuer