禁用Haskell类型转换

Question

我有一个基于hyperloglog的例子。我正在尝试使用大小对我的Container进行参数化，并使用reflection在容器函数中使用此参数。

import           Data.Proxy
import           Data.Reflection

newtype Container p = Container { runContainer :: [Int] }
    deriving (Eq, Show)

instance Reifies p Integer => Monoid (Container p) where
  mempty = Container $ replicate (fromIntegral (reflect (Proxy :: Proxy p))) 0
  mappend (Container l) (Container r) = undefined

我的Monoid实例有些简陋，它基于具体化的参数来定义mempty，并且进行一些“类型安全”的mappend操作。当我尝试对不同大小容器进行求和时，它可以完美地工作，但会失败并出现类型错误。

然而，它仍然可以被coerce欺骗，并且我正在寻找一种在编译时阻止它的方法:

ghci> :set -XDataKinds
ghci> :m +Data.Coerce
ghci> let c3 = mempty :: Container 3
ghci> c3
ghci> Container {runContaner: [0,0,0]}
ghci> let c4 = coerce c3 :: Container 4
ghci> :t c4
ghci> c4 :: Container 4
ghci> c4
ghci> Container {runContainer: [0,0,0]} 

添加类型角色并没有帮助

type role Container nominal

- Eugene Zhulenev

---

GHC 7.10由于原始代码中缺少“LANGUAGE”注释而会抛出许多错误。你能加上它们吗？ - Zeta

你有检查过在 .hs 文件中执行会发生什么吗？ GHCi 在模块边界方面可能会很奇怪。我非常确定 hyperloglog 有自己的角色声明。 - dfeuer

奇怪...角色注释确实应该防止这些强制转换。 - chi

这里不相关，而且你可能已经知道了，但我要指出这不是一个有效的单子实例，因为(mempty<>mempty) :: Container 1会得到 Container [0,0] ≠ mempty。你可以使用mappend ∝ zipWith (+)使其有效。 - leftaroundabout

@leftaroundabout 哦，是的，我最好在那里放置未定义。 - Eugene Zhulenev

Answer 1

问题在于只要构造函数在作用域内，newtype 就可以强制转换为其表示形式 - 实际上，这是 Coercible 的重要动机之一。而且，Coercible 约束就像任何其他类型类约束一样，会自动搜索并组合，甚至更加自动化。因此，coerce c3 发现您有：

instance Coercible (Container p) [Int]
instance Coercible [Int] (Container p')

对于所有的p和p'，我们通过以下方式愉快地为您构建复合强制转换。

instance (Coercible a b, Coercible b c) => Coercible a c

如果您不导出Container构造函数 - 通常情况下您是想这样做的！ - 那么就不再知道newtype等于其表示（您将失去上面的前两个实例），并且您可以在其他模块中获得所需的错误提示：

ContainerClient.hs:13:6:
    Couldn't match type ‘4’ with ‘3’
    arising from trying to show that the representations of
      ‘Container 3’ and
      ‘Container 4’ are the same
    Relevant role signatures: type role Container nominal nominal
    In the expression: coerce c3
    In an equation for ‘c4’: c4 = coerce c3

然而，在定义newtype的模块中，您始终可以通过coerce或其他方式打破不变量。

---

顺便说一下，在这里您可能不想使用记录样式的访问器并将其导出；这会让用户使用记录更新语法从您的代码中更改内容，因此

c3 :: Container 3
c3 = mempty

c3' :: Container 3
c3' = c3{runContainer = []}

变得有效。将runContainer转化为一个独立的函数。

---

我们可以通过查看核心代码（通过-ddump-simpl）来验证我们正在获得两个新类型表示约束的组合：在定义Container的模块中（我也称之为Container），输出为（如果我们删除导出列表）：

c4 :: Container 4
[GblId, Str=DmdType]
c4 =
  c3
  `cast` (Container.NTCo:Container[0] <GHC.TypeLits.Nat>_N <3>_N
          ; Sym (Container.NTCo:Container[0] <GHC.TypeLits.Nat>_N <4>_N)
          :: Container 3 ~R# Container 4)

这段文字有些难以理解，但需要注意的是Container.NTCo:Container[0]：其中NTCo是将newtypeContainer p与其表示类型进行转换的newtype强制转换。 Sym反转了这个过程，;组合了两个约束条件。

将最终的约束条件称为γₓ；然后整个类型推导过程为：

Sym :: (a ~ b) -> (b ~ a)
-- Sym is built-in

(;) :: (a ~ b) -> (b ~ c) -> (a ~ c)
-- (;) is built-in

γₙ :: k -> (p :: k) -> Container p ~ [Int]
γₙ k p = Container.NTCo:Container[0] <k>_N <p>_N

γ₃ :: Container 3 ~ [Int]
γ₃ = γₙ GHC.TypeLits.Nat 3

γ₄ :: Container 4 ~ [Int]
γ₄ = γₙ GHC.TypeLits.Nat 4

γ₄′ :: [Int] ~ Container 4
γ₄′ = Sym γ₄

γₓ :: Container 3 ~ Container 4
γₓ = γ₃ ; γ₄′

这里是我使用的源文件：

Container.hs:

{-# LANGUAGE FlexibleContexts, UndecidableInstances, ScopedTypeVariables,
             RoleAnnotations, PolyKinds, DataKinds #-}

module Container (Container(), runContainer) where

import Data.Proxy
import Data.Reflection
import Data.Coerce

newtype Container p = Container { runContainer :: [Int] }
    deriving (Eq, Show)
type role Container nominal

instance Reifies p Integer => Monoid (Container p) where
  mempty = Container $ replicate (fromIntegral (reflect (Proxy :: Proxy p))) 0
  mappend (Container l) (Container r) = Container $ l ++ r

c3 :: Container 3
c3 = mempty

-- Works
c4 :: Container 4
c4 = coerce c3

ContainerClient.hs:

{-# LANGUAGE DataKinds #-}

module ContainerClient where

import Container
import Data.Coerce

c3 :: Container 3
c3 = mempty

-- Doesn't work :-)
c4 :: Container 4
c4 = coerce c3

- Antal Spector-Zabusky