Преобразование нетипизированное AST для простого языка напечатанного в GADT

Question

У меня есть ADT, представляющий AST для простого языка:

data UTerm = UTrue 
     | UFalse 
     | UIf UTerm UTerm UTerm 
     | UZero 
     | USucc UTerm 
     | UIsZero UTerm 

Эта структура данных может представлять недопустимые термины, которые не следуют правилам типа языка, как UIsZero UFalse, так что я хотел бы использовать GADT что навязывает а-typedness:

{-# LANGUAGE GADTs #-} 

data TTerm a where 
    TTrue :: TTerm Bool 
    TFalse :: TTerm Bool 
    TIf :: TTerm Bool -> TTerm a -> TTerm a -> TTerm a 
    TZero :: TTerm Int 
    TSucc :: TTerm Int -> TTerm Int 
    TIsZero :: TTerm Int -> TTerm Bool 

Моя проблема заключается в тип проверки UTerm и превратить его в Tterm. Мой первый мысль была UTerm -> Maybe (TTerm a), но это, конечно, не работает, потому что недействителен для всех a s. Я даже не знаю, какой будет тип, потому что мы не знаем, будет ли a Int или Bool. Тогда я думал, что я мог бы написать другой функции проверки типа для каждого из возможных значений a:

import Control.Applicative 

typecheckbool :: UTerm -> Maybe (TTerm Bool) 
typecheckbool UTrue = Just TTrue 
typecheckbool UFalse = Just TFalse 
typecheckbool (UIsZero a) = TIsZero <$> typecheckint a 
typecheckbool _ = Nothing 

typecheckint :: UTerm -> Maybe (TTerm Int) 
typecheckint UZero = Just TZero 
typecheckint (USucc a) = TSucc <$> typecheckint a 
typecheckint (UIf a b c) = TIf <$> typecheckbool a <*> typecheckint b <*> typecheckint c 
typecheckint UTrue = Nothing 
typecheckint UFalse = Nothing 
typecheckint (UIsZero _) = Nothing 

Это работает для некоторых случаев, для подмножества языка, где TIF требует его следствия и альтернативы являются Ints (Но TIf TTrue TFalse TTrue на самом деле полностью действителен), и где мы знаем тип цели выражения, мы печатаем .

Какой способ конвертировать из UTerm в TTerm?

Answer 1

Стандартный метод для определения экзистенциального типа:

data ETerm_ where 
    ETerm_ :: TTerm a -> ETerm 

В этом случае, вы можете также некоторый срок на уровень доказательства того, какой тип у вас есть; например

data Type a where 
    TInt :: Type Int 
    TBool :: Type Bool 

тогда реальный ETerm будет выглядеть следующим образом:

data ETerm where 
    ETerm :: Type a -> TTerm a -> ETerm 

Интересный случай проверки типа является то что-то вроде

typeCheck (UIf ucond ut uf) = do 
    ETerm TBool tcond <- typeCheck ucond 
    ETerm tyt tt <- typeCheck ut 
    ETerm tyf tf <- typeCheck uf 
    case (tyt, tyf) of 
     (TBool, TBool) -> return (ETerm TBool (TIf tcond tt tf)) 
     (TInt , TInt) -> return (ETerm TInt (TIf tcond tt tf)) 
     _ -> fail "branches have different types" 

Answer 2

В качестве небольшого дополнения @ DanielWagner отвечают, вам может хотеть разложить такие проверки на равенство типа, такие как

... 
case (tyt, tyf) of 
     (TBool, TBool) -> return (ETerm TBool (TIf tcond tt tf)) 
     (TInt , TInt) -> return (ETerm TInt (TIf tcond tt tf)) 
     _ -> fail "branches have different types" 

Один из способов сделать это является использование свидетелей равенства:

import Data.Type.Equality 

typeEq :: Type a -> Type b -> Maybe (a :~: b) 
typeEq TInt TInt = Just Refl 
typeEq TBool TBool = Just Refl 
typeEq _  _  = Nothing 

typeCheck :: UTerm -> Maybe ETerm 
typeCheck (UIf ucond ut uf) = do 
    ETerm TBool tcond <- typeCheck ucond 
    ETerm tyt tt <- typeCheck ut 
    ETerm tyf tf <- typeCheck uf 
    case typeEq tyt tyf of 
     Just Refl -> return (ETerm tyt (TIf tcond tt tf)) 
     _   -> fail "branches have different types" 

Это разложение удобно, если вам нужно проверить тип равенства в различных частях вашей обычной проверки типа. Он также позволяет расширять язык с помощью парных типов, таких как (t1,t2), которые требуют структурного рекурсивного подхода для проверки равенства типов.

Можно даже написать полный решающий для типа равенства

{-# LANGUAGE EmptyCase #-} 
typeEq2 :: Type a -> Type b -> Either (a :~: b) ((a :~:b) -> Void) 
typeEq2 TInt TInt = Left Refl 
typeEq2 TInt TBool = Right (\eq -> case eq of) 
typeEq2 TBool TBool = Left Refl 
typeEq2 TBool TInt = Right (\eq -> case eq of) 

, но это, я думаю, вероятно, не будет необходимости, если вы пытаетесь смоделировать довольно продвинутые типы (например, GADTs).

В приведенном выше коде используется и пустой чехол для проверки всех возможных значений eq. Так как он имеет тип, например. Int :~: Bool, и нет конструкторов, соответствующих этому типу, мы остаемся без возможных значений для eq, и поэтому не требуется ветвь case. Это будет не вызвать предупреждение об исчерпании, поскольку на самом деле нет случаев, когда необработанные случаи (OT: я хочу, чтобы эти предупреждения были фактическими ошибками).

Вместо того, чтобы использовать EmptyCase, вы также можете использовать что-то вроде case eq of _ -> undefined, но используя кубы в доказательстве, подобные приведенному выше, является подозрительным.