Come specificare il tipo per una raccolta eterogenea in un AST formulato GADT?

Question

Mi piacerebbe creare un AST digitato per un linguaggio dinamico. Al momento, sono bloccato a gestire le collezioni. Ecco un esempio di codice rappresentante:

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

data Box = forall s. B s 

data BinOp = Add | Sub | Mul | Div 
      deriving (Eq, Show) 

data Flag = Empty | NonEmpty 

data List :: Flag -> * -> * where 
    Nil :: List Empty a 
    Cons :: a -> List f a -> List NonEmpty a 

data Expr ty where 
    EInt :: Integer -> Expr Integer 
    EDouble :: Double -> Expr Double 
-- EList :: List -> Expr List 

Mentre posso costruire istanze di List abbastanza bene:

*Main> :t (Cons (B (EInt 1)) (Cons (B (EDouble 2.0)) Nil)) 
(Cons (B (EInt 1)) (Cons (B (EDouble 2.0)) Nil)) 
    :: List Box 'NonEmpty 

io non sono affatto sicuro come codificare questo tipo in Expr per EList. Sono anche sulla strada giusta qui?

Answer 1

Un modo per affrontare questo problema consiste nel taggare i valori con i rappresentanti del tipo di runtime. Sto canalizzando Stephanie Weirich, qui. Facciamo un piccolo esempio. Per prima cosa, dai una rappresentazione ad alcuni tipi. Questo è in genere fatto con una costruzione singleton.

data Type :: * -> * where 
    Int :: Type Int 
    Char :: Type Char 
    List :: Type x -> Type [x] 

Così Type Int contiene un valore, che ho chiamato anche Int, perché agisce come rappresentante di run-time di tipo Int. Se è possibile vedere il colore anche nelle cose monocromatiche, lo :: a sinistra dello :: è rosso e lo Type è blu dopo lo .

Ora possiamo eseguire il packaging esistenziale, preservando l'utilità.

data Cell :: * where 
(:::) :: x -> Type x -> Cell 

Un Cell è un valore etichettato con un rappresentante runtime di questo tipo. Puoi recuperare l'utilità del valore leggendo il suo tag type. In effetti, poiché i tipi sono strutture di primo ordine, possiamo controllarli per l'uguaglianza in un modo utile.

data EQ :: k -> k -> * where 
    Refl :: EQ x x 

typeEQ :: Type x -> Type y -> Maybe (EQ x y) 
typeEQ Int Int = Just Refl 
typeEQ Char Char = Just Refl 
typeEQ (List s) (List t) = case typeEQ s t of 
    Just Refl -> Just Refl 
    Nothing -> Nothing 
typeEQ _ _ = Nothing 

Un uguaglianza booleana sui rappresentanti di tipo serve a nulla: abbiamo bisogno del test di uguaglianza per costruire il prove che i tipi rappresentate possono essere unificati. Con il test di prova-produzione, possiamo scrivere

gimme :: Type x -> Cell -> Maybe x 
gimme t (x ::: s) = case typeEQ s t of 
    Just Refl -> Just x 
    Nothing -> Nothing 

Naturalmente, scrivere i tag di tipo è un fastidio. Ma perché tenere un cane e abbaiare te stesso?

class TypeMe x where 
    myType :: Type x 

instance TypeMe Int where 
    myType = Int 

instance TypeMe Char where 
    myType = Char 

instance TypeMe x => TypeMe [x] where 
    myType = List myType 

cell :: TypeMe x => x -> Cell 
cell x = x ::: myType 

E ora siamo in grado di fare le cose come

myCells :: [Cell] 
myCells = [cell (length "foo"), cell "foo"] 

e quindi ottenere

> gimme Int (head myCells) 
Just 3 

Naturalmente, tutto sarebbe molto più ordinato, se non abbiamo dovuto fare lo costruzione singleton e potrebbe solo eseguire il pattern-match su tipi che potremmo scegliere di mantenere in fase di esecuzione. Mi aspetto che ci arriveremo quando il mitico quantificatore pi diventa meno mitico.