Lowering functions to an embedded language

How can I lower a Haskell function to an embedded language in as typesafe a manner as possible. In particular, let's assume I have a value type like

data Type t where
  Num  :: Type Int
  Bool :: Type Bool

data Ty = TNum | TBool deriving Eq

data Tagged t = Tagged (Type t) t deriving Typeable
data Dynamic  = forall t . Typeable t => Dynamic (Tagged t) deriving Typeable

forget :: Typeable t => Tagged t -> Dynamic
forget = Dynamic

remember :: Typeable b => Dynamic -> Maybe b
remember (Dynamic c) = cast c

and I want to convert a function like (isSucc :: Int -> Int -> Bool) to product of its dynamic form and some type information, like this

data SplitFun = SF { dynamic    :: [Dynamic] -> Dynamic 
                   , inputTypes :: [Ty] 
                   , outputType :: Ty
                   }

such that for some apply function

(\(a:b:_) -> isSucc a b) == apply (makeDynamicFn isSucc)

modulo some possible exceptions that could be thrown if the dynamic types actually don't match. Or, more explicitly, I'd like to find makeDynamicFn :: FunType -> SplitFun. Obviously that isn't a proper Haskell type and there's unlikely to be a way to pull the types from isSucc itself, so it might be something more like

anInt . anInt . retBool $ isSucc :: SplitFun

where anInt and retBool have printf-style types.

Is such a thing possible? Is there a way to simulate it?

Solution

To implement a function of type FunType -> SplitFun, we'll use standard type class machinery to deconstruct function types.

Now, implementing this function directly turns out to be fairly hard. To get inputTypes and outputType from the recursive case, you have to apply your function; but you can only apply the function inside the dynamic field, which gives you no way to fill the other fields. Instead, we'll split the task into two: one function will give us the Ty information, other will construct the [Dynamic] -> Dynamic function.

data Proxy a = Proxy

class Split r where
    dynFun :: r -> [Dynamic] -> Dynamic
    tyInfo :: Proxy r -> ([Ty], Ty)

    split :: r -> SplitFun
    split f = let (i, o) = tyInfo (Proxy :: Proxy r)
              in  SF (dynFun f) i o

Now, tyInfo doesn't actually need the function, we use Proxy just to pass the type information without needing to use undefined all over the place. Note that we need ScopedTypeVariables to be able to refer to the type variable r from instance declaration. Clever use of asTypeOf might also work.

We have two base cases: Bool and Int:

instance Split Int where
    dynFun i _ = forget (Tagged Num i)
    tyInfo _ = ([], TNum)

instance Split Bool where
    dynFun b _ = forget (Tagged Bool b)
    tyInfo _ = ([], TBool)

There are no input types and since we already have a value, we do not need to ask for more Dynamic values and we simply return Dynamic of that particular value.

Next, we have two recursive cases: Bool -> r and Int -> r

instance (Split r) => Split (Int -> r) where
    dynFun f (d:ds) = case remember d :: Maybe (Tagged Int) of
        Just (Tagged _ i) -> dynFun (f i) ds
        Nothing           -> error "dynFun: wrong dynamic type"
    dynFun f []     = error "dynFun: not enough arguments"

    tyInfo _ = case tyInfo (Proxy :: Proxy r) of
         (i, o) -> (TNum:i, o)

instance (Split r) => Split (Bool -> r) where
    dynFun f (d:ds) = case remember d :: Maybe (Tagged Bool) of
        Just (Tagged _ b) -> dynFun (f b) ds
        Nothing           -> error "dynFun: wrong dynamic type"
    dynFun f []     = error "dynFun: not enough arguments"

    tyInfo _ = case tyInfo (Proxy :: Proxy r) of
         (i, o) -> (TBool:i, o)

These two need FlexibleInstances. dynFun examines the first Dynamic argument and if it's okay, we can safely apply the function f to it and continue from there. We could also make dynFun :: r -> [Dynamic] -> Maybe Dynamic, but that's fairly trivial change.

Now, there's some duplication going on. We could introduce another class, such as:

class Concrete r where
    getTy   :: Proxy r -> Ty
    getType :: Proxy r -> Type r

And then write:

instance (Typeable r, Concrete r) => Split r where
    dynFun r _ = forget (Tagged (getType (Proxy :: Proxy r)) r)
    tyInfo _ = ([], getTy (Proxy :: Proxy r))

instance (Typeable r, Concrete r, Split s) => Split (r -> s) where
    dynFun f (d:ds) = case remember d :: Maybe (Tagged r) of
        Just (Tagged _ v) -> dynFun (f v) ds
        -- ...

    tyInfo _ = case tyInfo (Proxy :: Proxy s) of
        (i, o) -> (getTy (Proxy :: Proxy r):i, o)

But this needs both OverlappingInstances and UndecidableInstances.