haskell - 防止类型统一

Question

给定这个整数包装器:

newtype MyProxy a = MyProxy Int

mkProxy :: Int -> MyProxy a
mkProxy a = MyProxy a

addProxy :: MyProxy a -> MyProxy a -> MyProxy  a
addProxy (MyProxy a1) (MyProxy a2) = MyProxy $ a1+a2

我可以执行以下操作:

a = mkProxy 1
b = mkProxy 2
c = addProxy a b

因为幻影参数会被统一。但我想阻止这种统一并在 c 行导致类型错误。

ST monad 使用 rank2 类型来实现类似的效果。我可能可以通过更改 addProxy 的类型来做类似的事情。但我特别不想这样做。我想以某种方式注释 a 类型变量，以防止它在 addProxy 调用中统一。

这在 Haskell 中可行吗？为什么这样的选择会很危险？

---

编辑:

让我详细说明部分解决方案(需要 -XScopedTypeVariables)。我可以将上面的代码重写为:

c :: forall a1 a2. MyProxy a1
c = addProxy a b
    where
        a = mkProxy 1 :: MyProxy a1
        b = mkProxy 2 :: MyProxy a2

这正确地导致了 c 的类型错误，因为 a1 和 a2 不能统一。但这有两个缺点: a 和 b 不能在顶层定义；并且您必须明确指定 mkProxy 的结果类型。

是否可以解决这些缺点？

Answer 1

不，你不能，至少不能不为 mkProxy 指定更多内容。

ST monad 的工作方式是要求转义计算生成 forall 类型的东西。 ST s a 防止 s 在 a 中出现。

然而，在您的情况下，您正在进行两个相同的计算，因此为每个计算生成不同的类型可能会被用来做坏事。例如，如果 mkInt 1 每次调用时生成不同的类型，

class Evil a b c | a, b -> c where
  foo :: a -> b -> c

let x = mkProxy 1 in foo x x

会不同于

 foo (mkProxy 1) (mkProxy 1)

而且我们在代码中丢失了一些非常好的属性。

不过，我们可以做一些额外的工作，让 a 和 b 不能明确统一

 {-# LANGUAGE DataKinds #-}

 data Nat = S Nat | Z
 data Proxy (n :: Nat) a = Proxy a

 based :: a -> Proxy Z a
 based = Proxy

 fresh :: Proxy n a -> a -> Proxy (S n) a
 fresh (Proxy _) a = Proxy a

所以现在你需要做一些类似的事情

a = based 1

b = fresh a 2