Comprendere i cast coinvolti in pattern corrispondenti a un tipo di dati che è indicizzato su un tipo definito dall'utente

Question

Quindi, stavo giocando con DataKinds e TypeFamilies in Haskell e ho iniziato a guardare il GHC Core generato.

qui è un po TestCase per motivare la mia domanda:

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE KindSignatures #-} 

module TestCase where 

data Ty = TyBool | TyInt 

type family InterpTy (t :: Ty) :: * 
type instance InterpTy TyBool = Bool 
type instance InterpTy TyInt = Int 

data Expr (a :: Ty) where 
    I :: Int -> Expr TyInt 
    B :: Bool -> Expr TyBool 

eval :: Expr a -> InterpTy a 
eval (I i) = i 
eval (B b) = b 

Diamo uno sguardo al Nucleo generato per la funzione eval

TestCase.eval = 
    \ (@ (a_aKM :: TestCase.Ty)) (ds_dL3 :: TestCase.Expr a_aKM) -> 
    case ds_dL3 of _ [Occ=Dead] { 
     TestCase.I dt_dLh i_as6 -> 
     i_as6 
     `cast` (Sub (Sym TestCase.TFCo:R:InterpTyTyInt[0]) 
       ; (TestCase.InterpTy (Sym dt_dLh))_R 
       :: GHC.Types.Int ~# TestCase.InterpTy a_aKM); 
     TestCase.B dt_dLc b_as7 -> 
     b_as7 
     `cast` (Sub (Sym TestCase.TFCo:R:InterpTyTyBool[0]) 
       ; (TestCase.InterpTy (Sym dt_dLc))_R 
       :: GHC.Types.Bool ~# TestCase.InterpTy a_aKM) 
    } 

Ovviamente abbiamo bisogno di portare in giro le informazioni su ciò che a potrebbe essere nel ramo specifico. Se non indicizzo su un Datakind e non utilizzerei TypeFamilies, il cast è molto più facile da capire.

sarebbe qualcosa di simile:

Main.eval = 
    \ (@ a_a1hg) (ds_d1sQ :: Main.Simpl a_a1hg) -> 
    case ds_d1sQ of _ [Occ=Dead] { 
     Main.I' dt_d1to i_aFa -> 
     i_aFa 
     `cast` (Sub (Sym dt_d1to) :: GHC.Integer.Type.Integer ~# a_a1hg); 
     Main.B' dt_d1tk b_aFb -> 
     b_aFb `cast` (Sub (Sym dt_d1tk) :: GHC.Types.Bool ~# a_a1hg) 
    } 

questo posso capire benissimo, quello che mi turba nell'esempio TypeFamilies è questa parte:

(Sub (Sym TestCase.TFCo:R:InterpTyTyInt[0]) 
     ; (TestCase.InterpTy (Sym dt_dLh))_R 
     :: GHC.Types.Int ~# TestCase.InterpTy a_aKM); 

La seconda linea è ciò che confonde realtà me. Cosa fa il punto e virgola? Sembra un po 'fuori luogo qui o mi sto perdendo qualcosa? C'è un posto dove posso leggere su questo (Colgo volentieri carte se si può raccomandare uno) per quanto riguarda

saluti,

raichoo

Answer 1

Il punto e virgola è sintassi per transitività coercizioni.

L'ultima (a partire da settembre 2014) la carta su System FC è "Safe Zero-Cost Coercions in Haskell" da ICFP 2014.

In particolare, nella figura 3 che la carta vediamo la sintassi di coercizioni. "γ₁; γ₂" è la transitività della coercizione. Se γ₁ è una coercizione che testimonia che "τ₁ ~ τ₂" e γ₂ sono una coercizione che testimonia che τ₂ ~ τ₃ allora "γ₁; γ₂" è una coercizione che testimonia τ₁ ~ τ₃.

Nell'esempio, quando si scrive eval (I i) = i ciò che il compilatore vede sul lato destro è un valore di tipo Int, e che cosa ha bisogno (dal tipo di ritorno della funzione) è qualcosa di InterpTy a. Quindi ora ha bisogno di costruire una dimostrazione che sia Int ~ InterpTy a.

Informalmente, (lettura da destra a sinistra e ignorando i ruoli - per i cui dettagli si vede la carta linked):

1. dal fare il pattern match GADT si apprende che "a ~ Int" (che è dt_dLh)
2. Quindi applichiamo Sym ad esso, per ottenere "Int ~ a".
3. Applicare quindi la famiglia InterpTy per ottenere "InterpTy Int ~ InterpTy a" (questo è un esempio di/congruenza /)
4. Poi componiamo che transitivamente con "Sym InterpTyTyInt" (che è la versione capovolta della assioma che afferma che "InterpTy TyInt ~ Int" per ottenere la coercizione che stiamo cercando: "Int ~ InterpTy a"