La transformación de la representación sin tipo de DSL en representación mecanografiado

Question

Dado un lenguaje sencillo, dicen

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

es entonces posible transformarla en una representación escrito:

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

He intentado varios enfoques, p.ej lo siguiente:

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

Esto no funciona, y me sale el siguiente mensaje de error:

tipo ambiguo variable 'a' en la restricción:
'tipificables un'
que surge de una uso de `e2t' en ...
solución probable: añadir una firma tipo que fija estas variables (s) tipo de

Sin embargo, si me gusta esta

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

Correcto. Puede que no te des cuenta, pero estás tratando de hacer una inferencia de tipo en tu idioma. Si desea convertir la expresión f x en su GADT tipado, no es suficiente simplemente conocer el tipo de resultado. Podríamos tener f :: Bool -> Int con x :: Bool, f :: (Int -> Int) -> Int con x :: Int -> Int, etc. Y su representación mecanografiada afirma saber eso, especialmente porque requiere Typeable en sus constantes (puede ser capaz de salirse con la mía al saber qué tipo es si no lo hiciera t tiene la restricción Typeable).

e2t requiere conocimiento de qué tipo se espera que sea la expresión. Necesita alguna forma de determinar qué tipo se espera que sea el argumento de una aplicación. Tal vez usted puede conseguir alrededor de necesidad esta diciendo algo diferente, a saber:

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

Es decir, se está tratando de ver si E se puede dar un tipo, pero en lugar de decirle qué tipo debe ser, Te dijo. Esta es una inferencia ascendente, que generalmente es más fácil. Para codificar esta:

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

Hmm, después de jugar con esto por un tiempo, se dan cuenta de que se encuentra con exactamente el mismo problema en el camino de vuelta. No creo que sea posible hacerlo con solo Data.Typeable. Necesitará volver a crear algo como dynApp desde Data.Dynamic, pero para T s en lugar de tipos regulares de Haskell. Es decir. tendrá que hacer algunas operaciones en TypeRep sy luego, en algún momento, inserte un "confía en mí" unsafeCoerce una vez que sepa que es seguro. Pero no se puede convencer al compilador de que es seguro, hasta donde sé.

Esto podría hacerse en Agda, porque el equivalente de dichas operaciones en TypeRep s sería observable para el compilador. Probablemente sería un buen ejercicio para aprender ese idioma.