防止类型统一

Mike Izbicki 发表于 Dev

迈克·伊兹比基（Mike Izbicki）

鉴于此包装整数：

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。

有可能解决这些缺陷吗？

丹尼尔·格拉泽（Daniel Gratzer）

不，您不能，至少在不指定之前mkProxy。

ST monad的工作方式是要求转义计算生成某种类型的内容forall s. 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

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