Trasformare la rappresentazione senza tipo di un DSL in rappresentanza digitato

Question

Dato un linguaggio semplice, dicono

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

è allora possibile trasformarlo in una rappresentazione digitato:

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

ho provato vari approcci, per esempio il seguente:

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

Questo non funziona, e ottengo il seguente messaggio di errore:

tipo ambiguo variabile 'a' nel vincolo:
'tipizzabile un'
derivante da una uso di `E2T' a ...
correzione probabile: aggiungere una firma tipo che consente di risolvere questi variabile di tipo (s)

Tuttavia, se mi piace questo

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

compila.

Answer 1

Proprio così. Potresti non rendertene conto, ma stai cercando di fare inferenza di tipo sulla tua lingua. Se vuoi convertire l'espressione f x nel tuo GADT digitato, non è sufficiente conoscere il tipo di risultato. Potremmo avere f :: Bool -> Int con x :: Bool, f :: (Int -> Int) -> Int con x :: Int -> Int, ecc. E la tua rappresentazione tipizzata afferma di conoscerla, specialmente dal momento che richiede Typeable sulle sue costanti (potresti essere in grado di farla finita con la menzogna sul sapere di che tipo si tratta se non hai fatto t avere il vincolo Typeable).

e2t richiede la conoscenza del tipo di espressione previsto. Hai bisogno di un modo per determinare quale tipo si suppone che sia l'argomento di un'applicazione. Forse si può andare in giro che necessitano di questo dicendo qualcosa di diverso, vale a dire:

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

vale a dire, si sta solo cercando di vedere se E può essere dato un tipo, ma invece di raccontarla che tipo dovrebbe essere, ti dice. Questa è inferenza dal basso verso l'alto, che è generalmente più facile. Per codificare questo:

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

Hmm, dopo aver giocato con questo per un po ', mi rendo conto si esegue in esattamente lo stesso problema sulla via del ritorno in su. Non penso sia possibile farlo usando solo Data.Typeable. È necessario ricreare qualcosa come dynApp da Data.Dynamic, ma per T s invece di tipi Haskell regolari. Cioè dovrai fare alcune operazioni su TypeRep se poi a un certo punto inserisci un "mi fidi" unsafeCoerce una volta che sai che è sicuro. Ma non puoi convincere il compilatore che è sicuro, per quanto ne so.

Questo sarebbe possibile fare in Agda, perché le operazioni equivalenti su TypeRep s sarebbero osservabili al compilatore. Probabilmente sarebbe un buon esercizio quando imparerai quella lingua.