问题描述:

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.

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