Conversione di un AST non tipizzata per un semplice linguaggio digitato in un GADT

Question

Ho un ADT che rappresenta l'AST per un linguaggio semplice:

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

Questa struttura di dati può rappresentare termini non validi che non seguono le regole di tipo della lingua, come UIsZero UFalse, quindi mi piacerebbe usare un GADT che fa rispettare ben 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 

il mio problema è quello di digitare controllare un UTerm e convertirlo in un Tterm. Il mio primo pensato era UTerm -> Maybe (TTerm a), ma questo naturalmente non funziona perché non è valido per tutti a s. Non so nemmeno quale sarebbe il tipo, perché non sappiamo se a sarà Int o Bool. Poi ho pensato di scrivere un differente funzione controllo di tipo per ciascuno dei possibili valori di 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 

Questo funziona per alcuni casi, per un sottoinsieme del linguaggio in cui TSe richiede ai suoi conseguente ed alternativi sono Ints (Ma lo TIf TTrue TFalse TTrue è in realtà totalmente valido) e dove conosciamo il tipo di destinazione dell'espressione siamo digitando.

Qual è il modo corretto per convertire da un UTerm a un TTerm?

Answer 1

La tecnica standard è quello di definire un tipo esistenziale:

data ETerm_ where 
    ETerm_ :: TTerm a -> ETerm 

In questo caso, si potrebbe anche voler alcune prove termine a livello del quale tipo avete; per esempio.

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

poi il vero ETerm sarebbe simile a questa:

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

Il caso interessante di controllo di tipo è quindi qualcosa di simile

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

Come un minore complemento @ di DanielWagner risposta, potrebbe voler ridurre i controlli di uguaglianza di tipo come

... 
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" 

Un modo per farlo che sta usando i testimoni di uguaglianza:

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" 

Questa fattorizzazione è conveniente se avete bisogno di controllare il tipo uguaglianza in più parti del tuo tipo di routine di controllo. Consente inoltre di estendere la lingua con tipi di coppie come (t1,t2), che richiedono un approccio ricorsivo strutturale per controllare l'uguaglianza di tipo.

Si potrebbe anche scrivere un decisore completo per il tipo di uguaglianza

{-# 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) 

ma questo, immagino, sarà probabilmente non è necessaria a meno che non si sta cercando di modellare i tipi molto avanzati (ad esempio GADTs).

Il codice sopra utilizza e caso vuoto per esaminare tutti i possibili valori eq possono avere. Poiché ha tipo per es. Int :~: Bool e non ci sono costruttori corrispondenti a quel tipo, non ci sono valori possibili per eq e quindi non è necessario alcun ramo di caso. Questo sarà non innescare un avvertimento esaustivo, poiché non ci sono in effetti nessun caso lasciato non gestito (OT: vorrei che questi avvisi fossero errori effettivi).

Invece di utilizzare EmptyCase, è possibile utilizzare anche qualcosa come case eq of _ -> undefined, ma l'utilizzo di fondi in termini di prova come quello precedente è molto interessante.