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

Question

假设我有这样的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))国家单子变压器内部，作为内部状态的值？

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

编辑：ATerm解决了如何GADT在状态中存储不同状态的最初问题，现在的问题是由于类型丢失了，因此似乎无法比较新旧状态。

编辑：最终答案。

在使用@luqui来回切换之后，下面是完整的代码片段，可以回答这个问题。

随意分叉此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 ()

Answer 1

是的，您可以使用存在性

data ATerm where
   ATerm :: Term a -> ATerm

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

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

编辑

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

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

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

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

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

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

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

您还需要将其添加Typeable到任何隐藏的变量（结果类型中未出现的变量）

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

粗略地说，如果要比较类型，则需要Typeable在某个地方对它们进行约束。