haskell - 不同eDSL之间的转换(不同类型类别约束)

Question

我正在尝试将一个简单的 eDSL“编译”为 Atom语言。这里出现的一个问题是，我的类型/函数的类型类约束与 Atom 语言的约束不匹配。

一个编译为 Atom 的 eDSL 是 copilot ，它也有同样的问题，并以相当冗长的方式解决它。以下是所涉及数据类型的简化版本:

{-# 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和Op1是新eDSL的一部分，NumE和Exp属于编译目标。为了在某​​些时候在 eDSL 之间进行转换，我需要一个具有以下类型的函数 op2exp:

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

现在 Atom 处理这个问题的方式是 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

这可行，但相当麻烦且充满重复。

问题:

有没有一种方法，也许可以使用新的语言功能，以更简单的方式编写 op2exp 函数？理想的情况是:

op2exp (Neg t) = ENeg

理想情况下，我什至不需要 Type 数据类型，并让编译器找出所有类型都匹配。

Answer 1

您可以通过使用 * -> Constraint 类型参数，以目标语言将 Op1 数据类型参数化。看看 Atom 和 Ivory 库，我认为这样的东西应该可以工作:

{-# 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