Comment spécifier le type d'une collection hétérogène dans un AST formulé par GADT?

Question

Je voudrais faire un AST typé pour une langue dynamique. À l'heure actuelle, je suis bloqué sur la gestion des collections. Voici un exemple de code représentatif:

{-# 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 

Alors que je peux construire des instances de suffisamment List:

*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 

Je ne suis pas sûr du tout comment coder ce type dans Expr pour EList. Suis-je même sur le bon chemin ici?

Answer 1

Une façon d'aborder ce problème est de marquer des valeurs avec des représentants de type à l'exécution. Je canalise Stephanie Weirich, ici. Ayons un petit exemple. D'abord, donnez une représentation à certains types. Cela est généralement fait avec une construction singleton.

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

donc Type Int contient une valeur, que je l'ai aussi appelé Int, car il agit en tant que représentant du temps d'exécution du type Int. Si vous pouvez voir la couleur même dans les choses monochromes, le Int à gauche du :: est rouge, et le Int après Type est bleu.

Maintenant nous pouvons faire l'emballage existentiel, préservant l'utilité.

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

A Cell est une valeur étiqueté avec un représentant d'exécution de ce type. Vous pouvez récupérer l'utilité de la valeur en lisant sa balise de type. En effet, comme les types sont des structures de premier ordre, nous pouvons les vérifier pour l'égalité d'une manière 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 

Une égalité booléenne sur les représentants du type ne sert à rien: nous avons besoin du test d'égalité pour construire la preuve qui peuvent être unifiés les types représentés. Avec le test de production de preuves, nous pouvons écrire

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

Bien sûr, l'écriture des étiquettes de type est une nuisance. Mais pourquoi garder un chien et aboyer vous-même?

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 

Et maintenant, nous pouvons faire des choses comme

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

puis obtenir

> gimme Int (head myCells) 
Just 3 

Bien sûr, tout cela serait tellement plus net si nous ne devions pas faire la construction singleton et pourrait juste correspondre à des types que nous pourrions choisir de conserver au moment de l'exécution. Je pense que nous y arriverons lorsque le quantificateur mythique deviendra moins mythique.