haskell - 禁用 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 。当我尝试对不同大小的容器求和时，它完美地工作，但因类型错误而失败。

但是它仍然可以通过强制来欺骗，我正在寻找在编译时阻止它的方法:

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

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 的模块中破坏不变量(通过强制 或其他方式)。

<小时/>

顺便说一句，您可能不想在这里使用记录样式访问器并将其导出；允许用户使用记录更新语法来更改您下面的代码，因此

c3 :: Container 3
c3 = mempty

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

生效。让 runContainer 成为一个独立的函数。

<小时/>

我们可以通过查看核心(通过 -ddump-simpl)来验证我们是否获得了两个 newtype 表示约束的组合:在模块内定义 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 是一个 newtype newtype Container p 与其表示类型之间的强制转换。 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