Как я могу восстановить общий доступ в GADT?

В типобезопасном совместном доступе к наблюдаемым в Haskell Энди Гилл показывает, как восстановить общий доступ, существовавший на уровне Haskell, в DSL. Его решение реализовано в пакете data-reify. Можно ли изменить этот подход для работы с GADT? Например, учитывая этот GADT:

data Ast e where
  IntLit :: Int -> Ast Int
  Add :: Ast Int -> Ast Int -> Ast Int
  BoolLit :: Bool -> Ast Bool
  IfThenElse :: Ast Bool -> Ast e -> Ast e -> Ast e

Я хотел бы восстановить совместное использование путем преобразования вышеуказанного AST в

type Name = Unique

data Ast2 e where
  IntLit2 :: Int -> Ast2 Int
  Add2 :: Ast2 Int -> Ast2 Int -> Ast2 Int
  BoolLit2 :: Bool -> Ast2 Bool
  IfThenElse2 :: Ast2 Bool -> Ast2 e -> Ast2 e -> Ast2 e
  Var :: Name -> Ast2 e

по функции

recoverSharing :: Ast -> (Map Name, Ast2 e1, Ast2 e2)

(Я не уверен насчет типа recoverSharing.)

Обратите внимание, что мне не нужно вводить новые привязки с помощью конструкции let, а только восстановить восстановление совместного использования, существовавшее на уровне Haskell. Вот почему у меня recoverSharing вернуть Map,

Если это не может быть сделано как пакет многократного использования, может ли это быть сделано по крайней мере для конкретного GADT?

Источник

2 ответа

Решение

Интересная головоломка! Оказывается, вы можете использовать data-reify с GADT. Что вам нужно, это обертка, которая скрывает тип в экзисте. Тип может быть впоследствии получен путем сопоставления с образцом на Type тип данных.

data Type a where
  Bool :: Type Bool
  Int :: Type Int

data WrappedAst s where
  Wrap :: Type e -> Ast2 e s -> WrappedAst s

instance MuRef (Ast e) where
  type DeRef (Ast e) = WrappedAst
  mapDeRef f e = Wrap (getType e) <$> mapDeRef' f e
    where
      mapDeRef' :: Applicative f => (forall b. (MuRef b, WrappedAst ~ DeRef b) => b -> f u) -> Ast e -> f (Ast2 e u)
      mapDeRef' f (IntLit i) = pure $ IntLit2 i
      mapDeRef' f (Add a b) = Add2 <$> (Var Int <$> f a) <*> (Var Int <$> f b)
      mapDeRef' f (BoolLit b) = pure $ BoolLit2 b
      mapDeRef' f (IfThenElse b t e) = IfThenElse2 <$> (Var Bool <$> f b) <*> (Var (getType t) <$> f t) <*> (Var (getType e) <$> f e)

getVar :: Map Name (WrappedAst Name) -> Type e -> Name -> Maybe (Ast2 e Name)
getVar m t n = case m ! n of Wrap t' e -> (\Refl -> e) <$> typeEq t t'

Вот весь код: https://gist.github.com/3590197

Редактировать: мне нравится использование Typeable в другом ответе. Так что я сделал версию моего кода с Typeable тоже: https://gist.github.com/3593585. Код значительно короче. Type e -> заменяется Typeable e =>, что также имеет недостаток: мы больше не знаем, что возможные типы ограничены Int а также BoolЭто означает, что должен быть Typeable e ограничение в IfThenElse,

Источник

Я постараюсь показать, что это можно сделать для конкретных GADT, используя ваш GADT в качестве примера.

Я буду использовать пакет Data.Reify. Это требует от меня определения новой структуры данных, в которой рекурсивные позиции заменяются параметром.

data AstNode s where
  IntLitN :: Int -> AstNode s
  AddN :: s -> s -> AstNode s
  BoolLitN :: Bool -> AstNode s
  IfThenElseN :: TypeRep -> s -> s -> s -> AstNode s

Обратите внимание, что я удаляю много информации о типах, которая была доступна в исходном GADT. Для первых трех конструкторов ясно, что это был за тип (Int, Int и Bool). Для последнего я буду помнить тип, используя TypeRep (доступно в Data.Typeable). Экземпляр MuRef, требуемый пакетом reify, показан ниже.

instance Typeable e => MuRef (Ast e) where
  type DeRef (Ast e)     = AstNode
  mapDeRef f (IntLit a)  = pure $ IntLitN a
  mapDeRef f (Add a b)   = AddN <$> f a <*> f b
  mapDeRef f (BoolLit a) = pure $ BoolLitN a
  mapDeRef f (IfThenElse a b c :: Ast e) = 
    IfThenElseN (typeOf (undefined::e)) <$> f a <*> f b <*> f c

Теперь мы можем использовать reifyGraph для восстановления общего доступа. Однако много информации о типах было потеряно. Давайте попробуем восстановить его. Я немного изменил ваше определение Ast2:

data Ast2 e where
  IntLit2 :: Int -> Ast2 Int
  Add2 :: Unique -> Unique -> Ast2 Int
  BoolLit2 :: Bool -> Ast2 Bool
  IfThenElse2 :: Unique -> Unique -> Unique -> Ast2 e

График из пакета reify выглядит следующим образом (где e = AstNode):

data Graph e = Graph [(Unique, e Unique)] Unique

Давайте создадим новую структуру данных графа, где мы можем хранить Ast2 Int и Ast2 Bool отдельно (таким образом, где информация о типе была восстановлена):

data Graph2 = Graph2 [(Unique, Ast2 Int)] [(Unique, Ast2 Bool)] Unique 
            deriving Show

Теперь нам нужно только найти функцию от Graph AstNode (результат reifyGraph) до Graph2:

recoverTypes :: Graph AstNode -> Graph2
recoverTypes (Graph xs x) = Graph2 (catMaybes $ map (f toAst2Int) xs) 
                                   (catMaybes $ map (f toAst2Bool) xs) x where
  f g (u,an) = do a2 <- g an
                  return (u,a2)

  toAst2Int (IntLitN a) = Just $ IntLit2 a
  toAst2Int (AddN a b)  = Just $ Add2 a b
  toAst2Int (IfThenElseN t a b c) | t == typeOf (undefined :: Int) 
                        = Just $ IfThenElse2 a b c
  toAst2Int _           = Nothing

  toAst2Bool (BoolLitN a) = Just $ BoolLit2 a
  toAst2Bool (IfThenElseN t a b c) | t == typeOf (undefined :: Bool) 
                          = Just $ IfThenElse2 a b c
  toAst2Bool _            = Nothing

Давайте сделаем пример:

expr = Add (IntLit 42) expr  

test = do
  graph <- reifyGraph expr
  print graph
  print $ recoverTypes graph

Печать:

let [(1,AddN 2 1),(2,IntLitN 42)] in 1
Graph2 [(1,Add2 2 1),(2,IntLit2 42)] [] 1

Первая строка показывает нам, что reifyGraph правильно восстановил общий доступ. Вторая строка показывает нам, что были найдены только типы Ast2 Int (что также правильно).

Этот метод легко адаптируется для других конкретных GADT, но я не понимаю, как его можно сделать полностью универсальным.

Полный код можно найти по адресу http://pastebin.com/FwQNMDbs.

Источник
Другие вопросы по тегам