Rappresentazione runtime speciale di [] tipo?

Question

consideri la semplice definizione di un vettore di lunghezza-indicizzato:

data Nat = Z | S Nat 

infixr 5 :> 
data Vec (n :: Nat) a where 
    V0 :: Vec 'Z a 
    (:>) :: a -> Vec n a -> Vec ('S n) a 

Naturalmente sarebbe ad un certo punto hanno bisogno la seguente funzione:

vec2list :: Vec n a -> [a] 

Tuttavia, questa funzione è in realtà solo l'identità di fantasia. Credo che le rappresentazioni runtime di questi due tipi siano le stesse, quindi

vec2list :: Vec n a -> [a] 
vec2list = unsafeCoerce 

dovrebbe funzionare. Ahimè, non è così:

>vec2list ('a' :> 'b' :> 'c' :> V0) 
"" 

Ogni input restituisce semplicemente la lista vuota. Quindi presumo che manchi la mia comprensione. Per provarlo, definisco il seguente:

data List a = Nil | Cons a (List a) deriving (Show) 

vec2list' :: Vec n a -> List a 
vec2list' = unsafeCoerce 

test1 = vec2list' ('a' :> 'b' :> 'c' :> V0) 

data SomeVec a = forall n . SomeVec (Vec n a) 

list'2vec :: List a -> SomeVec a 
list'2vec x = SomeVec (unsafeCoerce x) 

Sorprendentemente questo funziona! Di certo non è un problema con il GADT (il mio pensiero iniziale).

Penso che il tipo List sia identico in fase di esecuzione a []. Provo a testare anche questo:

list2list :: [a] -> List a 
list2list = unsafeCoerce 

test2 = list2list "abc" 

e funziona! Sulla base di questo fatto, devo concludere che [a] e List a devono avere la stessa rappresentazione runtime. Eppure, il seguente

list2list' :: List a -> [a] 
list2list' = unsafeCoerce 

test3 = list2list' (Cons 'a' (Cons 'b' (Cons 'c' Nil))) 

non funziona. list2list' restituisce sempre sempre la lista vuota. Credo che "avere identiche rappresentazioni di runtime" debba essere una relazione simmetrica, quindi questo non sembra avere senso.

Ho iniziato a pensare che forse c'è qualcosa di divertente con i tipi "primitivi" - ma ho sempre creduto che lo [] sia solo sintatticamente speciale, non semanticamente. Sembra che sia il caso:

data Pair a b = Pair a b deriving (Show, Eq, Ord) 

tup2pair :: (a,b) -> Pair a b 
tup2pair = unsafeCoerce 

pair2tup :: Pair a b -> (a,b) 
pair2tup = unsafeCoerce 

I primi lavori di funzione e la seconda non lo fa - come il nel caso di List e []. Anche se in questo caso, pair2tup segfaults anziché restituire sempre la lista vuota.

Sembra essere coerentemente asimmetrico rispetto ai tipi che utilizzano la sintassi "built-in". Torna all'esempio Vec, il seguente

list2vec :: [a] -> SomeVec a 
list2vec x = SomeVec (unsafeCoerce x) 

funziona bene pure! Il GADT non è davvero speciale.

La domanda è: in che modo le rappresentazioni di runtime dei tipi che utilizzano la sintassi "incorporata" differiscono da quelle che non lo sono?

In alternativa, come si scrive una coercizione a costo zero da Vec n a a [a]? Questo non risponde alla domanda, ma risolve il problema.

Il test è stato eseguito con GHC 7.10.3.

---

Come notato da un commentatore, questo comportamento è presente solo nell'interpretazione. Una volta compilato, tutte le funzioni funzionano come previsto. La domanda vale ancora, solo per la rappresentazione di runtime nell'interpretazione di.

Answer 1

Ora per rispondere alla tua domanda principale, this thread appears to have the answer: iniziare ghci con -fobject-code:

$ ghci /tmp/vec.hs 
GHCi, version 7.10.3: http://www.haskell.org/ghc/ :? for help 
[1 of 1] Compiling Main    (/tmp/vec.hs, interpreted) 
Ok, modules loaded: Main. 
*Main> print $ vec2list ('a' :> 'b' :> 'c' :> V0) 
"" 

Con -fobject-code:

$ ghci -fobject-code /tmp/vec.hs 
GHCi, version 7.10.3: http://www.haskell.org/ghc/ :? for help 
[1 of 1] Compiling Main    (/tmp/vec.hs, /tmp/vec.o) 
Ok, modules loaded: Main. 
Prelude Main> print $ vec2list ('a' :> 'b' :> 'c' :> V0) 
"abc" 

I moduli che contengono [] e (,) sono tutti compilati, il che fa sì che la loro rappresentazione runtime sia diversa dai tipi di dati isomorfi in moduli interpretati. Secondo Simon Marlow sul thread che ho collegato, i moduli interpretati aggiungono annotazioni per il debugger. Penso che questo spieghi anche perché lo tup2pair funzioni e lo pair2tup no: le annotazioni mancanti non rappresentano un problema per i moduli interpretati, ma i moduli compilati soffocano sulle annotazioni aggiuntive.

-fobject-code ha alcuni aspetti negativi: tempo di compilazione più lungo, porta solo le funzioni esportate in ambito, ma ha il vantaggio aggiuntivo che l'esecuzione del codice è molto più veloce.

Answer 2

Per rispondere solo alla tua domanda alternativa, è possibile creare un newtype con un costruttore non esportato per dare un elenco di lunghezza tipo di livello e di una coazione a costo zero per le liste:

{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE DataKinds #-} 

module Vec (Nat(..), Vec, v0, (>:>), vec2list) where 

data Nat = Z | S Nat 

newtype Vec (n :: Nat) a = Vec { unVec :: [a] } 

v0 :: Vec Z a 
v0 = Vec [] 

infixr 5 >:> 
(>:>) :: a -> Vec n a -> Vec ('S n) a 
a >:> (Vec as) = Vec (a : as) 

vec2list :: Vec n a -> [a] 
vec2list (Vec as) = as 

Finché il costruttore Vec non è nel campo di applicazione (quindi solo v0 e >:> possono essere utilizzati per costruire vettori) l'invariante che il numero di livello del tipo rappresenta la lunghezza non può essere violato.

(questo approccio è sicuramente la mia preferenza rispetto unsafeCoerce, come qualsiasi cosa con unsafeCoerce potrebbe rompere con ogni aggiornamento del GHC o su diverse piattaforme.)