如何在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

我一点儿也不知道如何这种类型的编码Expr为EList.我甚至走在正确的道路上吗？

Answer 1

解决此问题的一种方法是使用运行时类型代表标记值.我在这里引导Stephanie Weirich.我们有一个小例子.首先,给出一些类型的表示.这通常采用单件结构.

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

所以Type Int包含一个值,我也称之为Int,因为它充当了类型的运行时代表Int.即使在单色的东西中你也可以看到颜色,Int左边::是红色,Int后面Type是蓝色.

现在我们可以做存在包装,保留实用性.

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

A Cell是一个标记有运行时代表其类型的值.您可以通过读取其类型标记来恢复该值的实用程序.实际上,由于类型是一阶结构,我们可以以有用的方式检查它们是否相等.

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量词变得不那么神秘时我们会到达那里.