问题在于只要构造函数在作用域内,
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
是将newtype
Container p
与其表示类型进行转换的newtype
强制转换。 Sym
反转了这个过程,;
组合了两个约束条件。
将最终的约束条件称为γₓ
;然后整个类型推导过程为:
Sym :: (a ~ b) -> (b ~ a)
(;) :: (a ~ b) -> (b ~ c) -> (a ~ c)
γₙ :: 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
c4 :: Container 4
c4 = coerce c3
ContainerClient.hs:
{-# LANGUAGE DataKinds #-}
module ContainerClient where
import Container
import Data.Coerce
c3 :: Container 3
c3 = mempty
c4 :: Container 4
c4 = coerce c3
.hs
文件中执行会发生什么吗? GHCi 在模块边界方面可能会很奇怪。我非常确定hyperloglog
有自己的角色声明。 - dfeuer(mempty<>mempty) :: Container 1
会得到Container [0,0] ≠ mempty
。你可以使用mappend ∝ zipWith (+)
使其有效。 - leftaroundabout