ハスケル型強制を無効にする

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 

マイラメモノイドインスタンスが具体化パラメータに基づいて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

問題が解決しない：それはまだcoerceでだまさすることができます、と私はコンパイル時に、それをブロックする方法を探していますが

コンストラクターが範囲内にある限り、newtypeはその表現に対して強制的です。実際、これはCoercibleの動機の大きな部分です。 Coercibleの制約は、他の型のクラス制約と似ていて、自動的に検索されてまとめられます。あなたとしておそらく - あなたはContainerコンストラクタをエクスポートしない場合はこのように、coerce c3あなたはすべてのpとp'、と喜ん

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

を経由してあなたのための複合強制を構築するための

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

を持っていることを見つけることですとにかくやりたい！あなたはいつものことができます、しかし

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はその表現に等しいことが知られています（あなたは、上記の最初の2つのインスタンスを失っていない）、そして、あなたは他のモジュールで必要なエラーが出ますnewtype（coerceまたはそれ以外の方法で）を定義するモジュールでインバリアントを解除します。サイドノートとして

---

、おそらくは、ここでは、レコード形式のアクセサを使用し、それをエクスポートする必要はありません。ユーザーがレコードの更新構文を使用してコードを変更することができるようにするため、

が有効になります。代わりにrunContainerをフリースタンディング関数にしてください。

---

我々は（-ddump-simpl経由）コアを見て2つのnewtype -representation制約の組成を取得していることを確認することができますContainerを定義するモジュール内の（私もContainer呼ばれてきました）、 NTCoはnewtypeContainer pと、それとの間にnewtype強制である：（私たちはエクスポートリストを削除する場合）出力が

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]ですs表現タイプ。Symはこれを変え、;は2つの制約を構成します。

最終的な制約γₓを呼び出します。その後、全体のタイピングの導出はここ

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