3

给定这个整数的包装器：

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.

是否有可能解决这些缺点？

4

2 回答 2

2

不，您不能，至少在不指定更多内容的情况下不能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

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

a = based 1

b = fresh a 2
于 2014-05-15T19:12:25.740 回答
0

我认为存在类型变量将适用于此。基本上，独立创建的两个存在类型变量不会统一。下面test因为无法统一两个MyProxys的类型变量而导致类型检查失败。

{-# LANGUAGE ExistentialQuantification #-}

newtype MyProxy a = MyProxy Int

data Exists f = forall a. Exists (f a)

mkProxy :: Int -> Exists MyProxy
mkProxy a = Exists (MyProxy a)

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

test :: Exists MyProxy -> Exists MyProxy -> Exists MyProxy
test (Exists a) (Exists b) = Exists (addProxy a b)
于 2014-05-15T21:04:13.383 回答