Che cos'è la sintassi Haskell (operatori di livello testo?)

Question

Che cosa significa '[] o ': nel codice Haskell? Alcuni esempi -

Example 1:

data OrderPacket replies where 
    NoOrders :: OrderPacket '[] 

Example 2:

data Elem :: [a] -> a -> * where 
    EZ :: Elem (x ': xs) x 

Answer 1

Dalla sezione manuale d'uso Haskell sulla Promoted list and tuple lists:

Con -XDataKinds, lista e tuple tipi di Haskell sono nativamente promossi a tipi, e ingiunge y stesso comoda sintassi al livello tipo, seppur preceduto da un preventivo:

data HList :: [*] -> * where 
    HNil :: HList '[] 
    HCons :: a -> HList t -> HList (a ': t) 

data Tuple :: (*,*) -> * where 
    Tuple :: a -> b -> Tuple '(a,b) 

foo0 :: HList '[] 
foo0 = HNil 

foo1 :: HList '[Int] 
foo1 = HCons (3::Int) HNil 

foo2 :: HList [Int, Bool] 
foo2 = ... 

(Nota: la dichiarazione di HCons richiede inoltre -XTypeOperators perché di operatori tipo infisso (: ').) Per dell'omologazione liste di livello di due o più elementi , come la firma di foo2 sopra, la citazione può essere omessa perché il significato è inequivocabile. Ma per gli elenchi di uno o degli elementi zero (come in foo0 e foo1), la citazione è obbligatoria, poiché i tipi [] e [Int] hanno significati esistenti in Haskell.

Quindi fondamentalmente è la stessa sintassi preceduta da una singola virgola ma che opera a livello di tipo. Alcuni giochi utilizzando ghci con il codice sopra:

λ> :t HNil 
HNil :: HList '[] 
λ> :t HCons 
HCons :: a -> HList t -> HList (a : t) 
λ> let x = 3 `HCons` HNil 
λ> :t x 
x :: Num a => HList '[a] 
λ> let x = Tuple 3 "spj" 
λ> :t x 
x :: Num a => Tuple '(a, [Char])