Преобразование нетипизированного представления DSL в типизированное представление - PullRequest
Новая
       1

Преобразование нетипизированного представления DSL в типизированное представление

5 голосов
/ 31 октября 2010

Если говорить простым языком, скажем 

data E where
  ValE :: Typeable a => a -> E
  AppE :: E -> E -> E

возможно ли затем преобразовать его в типизированное представление: 

data T a where
  ValT :: Typeable a => a -> T a
  AppT :: T (a -> b) -> T a -> T b
  deriving Typeable

Я пробовал разные подходы, например, следующее: 

e2t :: Typeable a => E -> Maybe (T a)
e2t (ValE x) = cast (ValT x)
e2t (AppE e1 e2) = liftM2 AppT (e2t e1) (e2t e2)

Это не работает, и я получаю следующее сообщение об ошибке:

Неопределенная переменная типа 'a' в ограничении:
'Typeable a'
в результате использования `e2t 'в ...
Возможное исправление: добавьте сигнатуру типа, которая исправляет эти переменные типа

Тем не менее, если мне так нравится 

e2t :: Typeable a => E -> Maybe (T a)
e2t (ValE x) = cast (ValT x)
e2t (AppE e1 e2) = liftM2 AppT (e2t e1) (e2t e2 :: Maybe (T Int))

компилируется.

1 Ответ

2 голосов
/ 31 октября 2010

Это верно. Вы можете не осознавать этого, но вы пытаетесь сделать вывод типа на своем языке. Если вы хотите преобразовать выражение f x в набранный вами GADT, недостаточно просто узнать тип результата. Мы могли бы иметь f :: Bool -> Int с x :: Bool, f :: (Int -> Int) -> Int с x :: Int -> Int и т. Д. И ваше типизированное представление утверждает, что знает об этом, тем более что для его констант требуется Typeable (возможно, вам удастся избежать неприятностей с ложью о том, что это за тип, если у вас не было ограничения Typeable.

e2t требует знания типа ожидаемого выражения. Вам нужен какой-то способ определить тип аргумента приложения. Может быть, вы можете обойти это, сказав что-то другое, а именно: 

e2t :: E -> Maybe (exists a. T a)

То есть, вы просто пытаетесь понять, может ли E быть дан тип, но вместо того, чтобы сообщить ему, какой это должен быть тип, он говорит вам. Это восходящий вывод, который обычно проще. Чтобы закодировать это: 

data AnyT where
    AnyT :: Typeable a => T a -> AnyT

Хм, поиграв с этим некоторое время, я понимаю, что вы столкнулись с точно такой же проблемой на пути назад. Я не думаю, что это можно сделать, используя только Data.Typeable. Вам нужно воссоздать что-то вроде dynApp из Data.Dynamic, но для T s вместо обычных типов Haskell. То есть вам придется выполнить некоторые операции на TypeRep с, а затем в какой-то момент вставить "просто доверьтесь мне" unsafeCoerce, как только вы поймете, что это безопасно. Но вы не можете убедить компилятор, что это безопасно, насколько я могу судить.

Это было бы возможно сделать в Agda, потому что эквивалентные упомянутые операции на TypeRep s были бы наблюдаемы для компилятора. Вероятно, это будет хорошим упражнением при изучении этого языка.

...