Deaktivieren Haskell Typ Zwang

Question

Ich habe Beispiel basierend auf hyperloglog. Ich versuche, meine Container mit Größe zu parametrisieren, und reflection zu verwenden, um diesen Parameter in Funktionen auf Containern zu verwenden.

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 

Meine lahm Monoid Instanz definiert mempty basierend auf verdinglichten Parameter, und dabei einige „typsichere“ mappend. Es funktioniert perfekt, wenn ich versuche Container unterschiedlicher Größe zu summieren.

Allerdings ist es immer noch mit coerce dazu verleitet werden, und ich suche, wie es bei der Kompilierung zu blockieren:

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]} 

Typ Rolle nicht helfen

type role Container nominal 

Answer 1

ist das Hinzufügen der Ausgabe ist, dass newtype s zu ihrer Darstellung koerzitierbar sind, solange der Konstruktor in Reichweite ist - tatsächlich ist dies ein großer Teil der Motivation für Coercible. Und Coercible Constraints sind wie jede andere Typklassenbeschränkung und werden automatisch für Sie durchsucht, nur noch mehr. Somit wird coerce c3 finden, dass Sie

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

für alle p und p' und glücklich den Aufbau der Verbund Zwang für Sie haben über

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

Wenn Sie nicht die Container Konstruktor exportiere - wie Sie wahrscheinlich möchte sowieso machen! - dann ist es nicht mehr bekannt, dass die newtype seine Darstellung gleich ist (verlieren Sie die ersten beiden Instanzen oben) und die gewünschten Fehler in anderen Modulen erhalten:

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 

Allerdings werden Sie immer in der Lage sein, breche deine Invarianten in dem Modul, in dem du die newtype (über coerce oder anders) definierst.

---

Als Seite beachten, werden Sie wahrscheinlich wollen nicht hier einen Rekord-Stil Accessor verwenden und exportieren; Dadurch können Benutzer die Datensatzaktualisierungssyntax verwenden, um den Code unter Ihnen zu ändern. Daher wird

c3 :: Container 3 
c3 = mempty 

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

gültig. Stellen Sie runContainer stattdessen eine freistehende Funktion ein.

---

Wir können bestätigen, dass wir mit Blick auf die Core (via -ddump-simpl), um die Zusammensetzung der beiden newtype -Darstellung Zwänge sind immer: innerhalb des Moduls, das Container definiert (was ich auch Container genannt haben), der Ausgang ist

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) 

es ist ein bisschen schwer zu lesen, aber das Wichtigste ist, zu sehen ist Container.NTCo:Container[0] (wenn wir die Exportliste entfernen): die NTCo ist ein newtype Zwang zwischen den newtypeContainer p und s Darstellungstyp.Sym dreht sich um, und ; komponiert zwei Einschränkungen.

Nennen Sie die letzte Bedingung γₓ; dann ist die ganze Typisierung Ableitung

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 
γₓ = γ₃ ; γ₄′ 

---

Hier die Quelldateien, die ich verwendet:

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