6

我正在尝试使用类型系统来确保永远不会从 monad M 中取出 X。我希望它的工作方式类似于runST,在这种情况下,不可能混合来自不同线程的环境。

data X s = X Int
type M s = State Int

newX :: M s (X s)
newX = X <$> get

eval :: (forall s. M s a) -> a
eval x = evalState x 0

但是,以下代码不会导致类型错误:

ghci> x = eval newX
ghci> :t x
x :: X s

为什么 ST monad 中的类似代码会抛出错误而我的不会?据我了解,sinM s a应该被绑定,使sinX s成为自由类型变量,从而导致类型检查器出错。

4

1 回答 1

5

要强制执行类型抽象,您必须使用dataor newtype, not type

同义词中未使用的参数type完全没有效果:

type M s = State Int

所以这些是等价的:

newX :: M s (X s)
newX :: State Int (X s)

eval :: (forall s. M s a) -> a
eval :: State Int a -> a

eval实际上不是更高级别的。

于 2020-02-04T14:37:43.487 回答