禁用Haskell类型强制

Question

我有基于hyperloglog的示例.我正在尝试Container使用大小参数化我的参数,并使用反射在容器上的函数中使用此参数.

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

Answer 1

问题在于,newtype只要构造函数在范围内,s就可以强制表示 - 事实上,这是动机的重要组成部分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改为做一个独立的功能.

newtype通过查看Core(via -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是和它的表示类型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