GADT公式ASTの異種コレクションのタイプを指定するにはどうすればよいですか？

Question

私は、動的言語用の型付けされたASTを作成したいと思います。現在、私はコレクションの取り扱いについていません。ここでは代表的なコードサンプルです：

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

私は十分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 

私は全然EListためExprでこのタイプをエンコードするかどうかはわかりません。私はここでも正しい道を歩いていますか？

Answer 1

この問題にアプローチする1つの方法は、値に実行時の型の代表をタグ付けすることです。私はStephanie Weirichにチャットしています。小さな例があります。まず、いくつかの種類の表現を与える。これは通常、シングルトンの構築で行われます。

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

それはタイプIntの実行時の代表として動作するので、そうType Intは、私もInt呼ばれてきた一つの値が含まれています。白黒のものでも色が見える場合は、::の左にあるIntは赤、Typeの後にはIntが青です。

今、私たちは実用的なパッケージングを行い、実用性を保つことができます。

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

Cellは、そのタイプの実行時の代表でタグ付けされた値です。 typeタグを読み取ることによって、値のユーティリティを回復できます。実際、型は一次構造であるため、それらが等価であることを有用な方法で確認することができます。

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 

タイプの代表のブール平等には使用されません：我々は表現型が統一することができ証拠を構築するために平等のテストを必要としています。証拠作成テストでは、書くことができます

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

もちろん、タイプタグを書くことは迷惑です。しかし、なぜ犬を飼って、あなた自身を吠えるのですか？私たちが行う必要はありませんでした場合

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 

そして今、我々は

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

のようなものを行い、その後、もちろん

> gimme Int (head myCells) 
Just 3 

を得ることができますが、それはすべてとても整然とだろう実行時に保持することができるような型のパターンマッチングを行うことができます。私は、神話のpi限定記号があまり神秘的でなくなったときにそこに着くことを期待しています。