3

我正在尝试将简单的 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 处理这个问题的方式相当 冗长：

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数据类型并让编译器找出所有类型都匹配。

4

1 回答 1

1

您可以Op1使用 kind 类型参数在目标语言中使数据类型参数化* -> Constraint。看看 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
于 2013-07-19T16:58:24.840 回答