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

Question

Учитывая простой язык, скажут

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) 

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

Неопределенный тип переменной «а» в ограничении:
«печатаемые а»
, вытекающее из использование `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)) 

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

Answer 1

Правильно. Вы можете не осознавать этого, но вы пытаетесь сделать вывод типа на своем языке. Если вы хотите преобразовать выражение f x в свой напечатанный GADT, недостаточно просто узнать тип результата. Мы могли бы иметь f :: Bool -> Int с x :: Bool, f :: (Int -> Int) -> Int с x :: Int -> Int и т. Д. И ваше типизированное представление заявляет, что оно известно, тем более, что для его констант требуется Typeable (вы можете уйти от лжи, зная, что это за тип, если вы этого не сделали, t имеет ограничение 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 с, а затем в какой-то момент вставьте «just trust me» unsafeCoerce, как только вы поймете, что это безопасно. Насколько я могу судить, вы не можете убедить компилятор в безопасности.

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