haskell - 是否可以将GADT存储在State monad变压器中？

假设我有这样的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转换器中，作为内部状态的值？

这里的问题是这两个是不同类型的，我不知道应该如何键入s的StateT s m a。

编辑: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 ()

最佳答案

是的，您可以使用存在性

data ATerm where
   ATerm :: Term a -> ATerm

这是存储“任何类型的Term”的单型。

但是，您应该知道您会丢失类型信息，我很想知道这不会对您造成任何问题。如果确实需要恢复它，则将需要添加一些Typeable约束或一些其他技巧-如果没有关于您正在做的事情的更多上下文，这很难说。

编辑

要获取类型信息，您需要将其包含在ATerm中

data ATerm where
    ATerm :: (Typeable a, Eq a) => Term a -> ATerm

令人遗憾的是，此更改可能导致Typeable约束感染了相当数量的代码。就是这样。我们还包括Eq a，因为如果我们在比较ATerms并发现它们的类型相同，则需要对该类型进行比较。

然后，要比较两个ATerm，首先需要比较它们的类型，然后比较它们的值。这可以通过 Typeable 库完成。

instance Eq ATerm where
    ATerm t == ATerm u
        | Just t' <- cast t = t' == u
        | otherwise = False

幸运的是，您的Term GADT不会隐藏任何类型。例如，如果您有类似的情况

data Term a where
    ...
    Apply :: Func a b -> Term a -> Term b

您还需要将Typeable也添加到任何隐藏变量(未出现在结果类型中的变量)

    Apply :: (Typeable a) => Func a b -> Term a -> Term b

大致来说，如果要比较类型，则需要在某处对它们进行Typeable约束。