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 => NumEInstnumEInst :: 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.
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