在State Monad Transformer中是否有可能存储一个GADT？

Question

在State Monad Transformer中是否有可能存储一个GADT？

4

假设我有一个像这样的 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 ()

- Don Klein

可能是削弱GADTs类型约束以处理不可预测数据的重复问题。 - radrow

在Lit构造函数上，您不应该需要Typeable a约束。 - dfeuer

或者，您也可以将Eq约束条件放在那里，并从ATerm构造函数中删除两个约束条件。示例 - dfeuer

感谢 @dfeuer 指出额外的限制，代码已更新。 - Don Klein

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- luqui · Accepted Answer

是的，您可以使用存在运算符

data ATerm where
   ATerm :: Term a -> ATerm

这是一个存储“任何类型 Term”的单态（monotype）。

但是您应该知道，您将失去类型信息，我有一种预感，在您的情况下这不会引起问题。如果您需要恢复它，您需要添加一些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 约束。