Disabilitare la coercizione di tipo Haskell

Question

Ho un esempio basato su hyperloglog. Sto cercando di parametrizzare il mio Container con le dimensioni e utilizzare reflection per utilizzare questo parametro nelle funzioni sui contenitori.

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 

mio zoppo esempio Monoide definisce mempty sulla base di parametri reificato, e facendo qualche "type-safe" mappend. Funziona perfettamente quando sto cercando di sommare contenitori di dimensioni diverse, in mancanza di errore di tipo.

Tuttavia è ancora può essere ingannato con coerce, e sto cercando modo di bloccarla al momento della compilazione:

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

Aggiunta di ruolo di tipo non aiuta

type role Container nominal 

Answer 1

La questione è che newtype s sono coercibili alla loro rappresentazione purché il costruttore sia in ambito - anzi, questa è una grande parte della motivazione per Coercible. E i vincoli Coercible sono come qualsiasi altro vincolo di classe di tipo, e vengono automaticamente cercati e messi insieme per te, solo ancora di più. Così, coerce c3 sta trovando che avete

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

per tutti p e p', e felicemente la costruzione della coercizione composito per voi via

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

Se non si esporta il costruttore Container - come probabilmente voglio fare comunque! - allora non è più noto che il newtype è pari alla sua rappresentazione (si perdono i primi due casi sopra), e si ottiene l'errore desiderato in altri moduli:

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 

Tuttavia, sarai sempre in grado di rompere i tuoi invarianti nel modulo in cui definisci il newtype (via coerce o altro).

---

Come nota a margine, probabilmente non desidera utilizzare una funzione di accesso record di stile qui ed esportarla; che consente agli utenti di utilizzare la sintassi di registrazione-update per cambiare fuori il codice da sotto, così

c3 :: Container 3 
c3 = mempty 

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

diventa valido. Rendi invece runContainer una funzione indipendente.

---

Possiamo verificare che stiamo ottenendo la composizione delle due newtype -Rappresentazione vincoli, cercando al centro (via -ddump-simpl): all'interno del modulo che definisce Container (che ho anche chiamato Container), l'uscita è (se togliamo la lista di esportazione)

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) 

è un po 'difficile da leggere, ma la cosa importante da vedere è Container.NTCo:Container[0]: il NTCo è un newtype coercizione tra il newtypeContainer p e s tipo di rappresentazione.Sym gira questo intorno e ; compone due vincoli.

Chiamare il vincolo finale γₓ; allora l'intera digitazione derivazione è

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

---

Qui ci sono i file di origine che ho usato:

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