Conversion between different eDSLs (different type class constraints)

Question

I'm trying to "compile" a simple eDSL to the Atom language. A problem that arises here is, that the type class constraints on my types/functions do not match those of the Atom language.

One eDSL which compiles to Atom is copilot, which also has this very same problem an solves it in a rather verbose way. What follows is a simplified version of the involved datatypes:

{-# LANGUAGE GADTs #-}

data Type a where   
    TFloat :: Type Float

data Op1 a b where
    Neg :: Type a -> Op1 a a

class NumE a where
instance NumE Float

data Exp e where
    ENeg :: NumE a => Exp a -> Exp a

Type and Op1 are part of the new eDSL, NumE and Exp belong to the compilation target. To convert between the eDSLs at some point I need a function op2exp with the following type:

op2exp :: Op1 a b -> Exp a -> Exp b

Now the way Atom handles this is rather verbose:

data NumEInst e = NumE e => NumEInst

numEInst :: Type a -> NumEInst a
numEInst TFloat = NumEInst

op2exp :: Op1 a b -> Exp a -> Exp b
op2exp op = case op of
    Neg t -> case numEInst t of NumEInst -> ENeg

This works, but is quite cumbersome and full of repetition.

Question:

Is there a way, maybing using new language features, to write the op2exp function in an easier way? Ideally something along the lines of:

op2exp (Neg t) = ENeg

Ideally, I wouldn't even need the Type data type and have the compiler figure out that all the types match.

Answer 1

You could make the Op1 datatype parametric in the target language, by using a type parameter of kind * -> Constraint. Looking at the Atom and Ivory libraries, I think something like this should work:

{-# LANGUAGE GADTs, ConstraintKinds #-}

data Op1 expr a b where
    Neg :: (expr a, Num a) => Op1 expr a a

class AtomExpr a where
instance AtomExpr Float

data AtomExp e where
    ENeg :: (AtomExpr a, Num a) => AtomExp a -> AtomExp a

op2exp :: Op1 AtomExpr a b -> AtomExp a -> AtomExp b
op2exp Neg = ENeg