Transforming untyped representation of a DSL into typed representation

Question

Given a simple language, say

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

is it then possible to transform it into a typed representation:

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

I have tried various approaches, e.g. the following:

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

This doesn't work, and I get the following error message:

Ambiguous type variable 'a' in the constraint:
'Typeable a'
arising from a use of `e2t' at ...
Probable fix: add a type signature that fixes these type variable(s)

However, if I do like this

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

it compiles.

Answer 1

That's right. You may not realize it, but you are trying to do type inference on your language. If you want to convert the expression f x to your typed GADT, it is not enough simply to know the result type. We could have f :: Bool -> Int with x :: Bool, f :: (Int -> Int) -> Int with x :: Int -> Int, etc. And your typed representation claims to know that, especially since it requires Typeable on its constants (you may be able to get away with lying about knowing what type it is if you didn't have the Typeable constraint).

e2t requires knowledge of what type the expression is expected to be. You need some way to determine what type the argument of an application is expected to be. Maybe you can get around needing this by saying something different, namely:

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

That is, you are just trying to see if E can be given a type, but instead of telling it what type it should be, it tells you. This is bottom-up inference, which is generally easier. To encode this:

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

Hmm, after playing with this for a while, I realize you run into exactly the same problem on the way back up. I don't think it's possible to do this using only Data.Typeable. You need to recreate something like dynApp from Data.Dynamic, but for Ts instead of regular Haskell types. I.e. you will have to do some operations on TypeReps and then at some point insert a "just trust me" unsafeCoerce once you know it is safe. But you can't convince the compiler it is safe, as far as I can tell.

This would be possible to do in Agda, because the equivalent said operations on TypeReps would be observable to the compiler. It would probably be a good exercise when learning that language.