haskell - Haskell 中的类型化抽象语法和 DSL 设计

Question

我正在用 Haskell 设计一个 DSL，我想要一个赋值操作。像这样(下面的代码只是为了在有限的上下文中解释我的问题，我没有类型检查 Stmt 类型):

 data Stmt = forall a . Assign String (Exp a) -- Assignment operation
           | forall a. Decl String a          -- Variable declaration 
 data Exp t where
    EBool   :: Bool -> Exp Bool
    EInt    :: Int  -> Exp Int
    EAdd    :: Exp Int -> Exp Int -> Exp Int
    ENot    :: Exp Bool -> Exp Bool

在前面的代码中，我可以使用 GADT 对表达式强制类型约束。我的问题是如何强制赋值的左侧是:1)已定义，即必须在使用之前声明一个变量 2)右侧必须具有与左侧变量相同的类型?

我知道在完全依赖类型的语言中，我可以定义由某种类型上下文索引的语句，即已定义变量及其类型的列表。我相信这会解决我的问题。但是，我想知道是否有某种方法可以在 Haskell 中实现这一点。

任何指向示例代码或文章的指针都受到高度赞赏。

Answer 1

鉴于我的工作侧重于在类型级别编码的范围和类型安全的相关问题，我在谷歌搜索时偶然发现了这个古老的问题，并认为我会试一试。

我认为，这篇文章提供了一个与原始规范非常接近的答案。一旦你有了正确的设置，整个事情就会出奇的短。

首先，我将从一个示例程序开始，让您了解最终结果的样子:

program :: Program
program = Program
  $  Declare (Var :: Name "foo") (Of :: Type Int)
  :> Assign  (The (Var :: Name "foo")) (EInt 1)
  :> Declare (Var :: Name "bar") (Of :: Type Bool)
  :> increment (The (Var :: Name "foo"))
  :> Assign  (The (Var :: Name "bar")) (ENot $ EBool True)
  :> Done

范围界定

为了确保我们只能为之前声明的变量赋值，我们需要一个作用域的概念。
GHC.TypeLits为我们提供了类型级别的字符串(称为 Symbol )，因此如果我们愿意，我们可以很好地使用字符串作为变量名。并且因为我们要确保类型安全，每个变量声明都带有一个类型注释，我们将与变量名称一起存储。因此，我们的范围类型是:[(Symbol, *)] .

我们可以使用类型族来测试给定的 Symbol如果是这种情况，则在范围内并返回其关联类型:

type family HasSymbol (g :: [(Symbol,*)]) (s :: Symbol) :: Maybe * where
  HasSymbol '[]            s = 'Nothing
  HasSymbol ('(s, a) ': g) s = 'Just a
  HasSymbol ('(t, a) ': g) s = HasSymbol g s

根据这个定义，我们可以定义变量的概念:类型为 a 的变量。范围内 g是一个符号s使得 HasSymbol g s返回 'Just a .这是什么ScopedSymbol数据类型表示通过使用存在量化来存储 s .

data ScopedSymbol (g :: [(Symbol,*)]) (a :: *) = forall s.
  (HasSymbol g s ~ 'Just a) => The (Name s)

data Name (s :: Symbol) = Var

在这里，我故意到处滥用符号:The是类型 ScopedSymbol 的构造函数和 Name是 Proxy 具有更好的名称和构造函数的类型。这使我们能够写出这样的细节:

example :: ScopedSymbol ('("foo", Int) ': '("bar", Bool) ': '[]) Bool
example = The (Var :: Name "bar")

声明

现在我们有了作用域的概念和该作用域中类型良好的变量，我们可以开始考虑影响 Statement s应该有。鉴于可以在 Statement 中声明新变量，我们需要找到一种方法在范围内传播这些信息。关键的后见之明是有两个索引:输入和输出范围。

致 Declare新变量及其类型将使用变量名和相应类型的对扩展当前范围。
Assign另一方面，评论不修改范围。他们只是关联了一个 ScopedSymbol到相应类型的表达式。

data Statement (g :: [(Symbol, *)]) (h :: [(Symbol,*)]) where
  Declare :: Name s -> Type a -> Statement g ('(s, a) ': g)
  Assign  :: ScopedSymbol g a -> Exp g a -> Statement g g

data Type (a :: *) = Of

我们再一次引入了代理类型，以拥有更好的用户级语法。

example' :: Statement '[] ('("foo", Int) ': '[])
example' = Declare (Var :: Name "foo") (Of :: Type Int)

example'' :: Statement ('("foo", Int) ': '[]) ('("foo", Int) ': '[])
example'' = Assign (The (Var :: Name "foo")) (EInt 1)

Statement s 可以通过定义以下类型对齐序列的 GADT 以保留范围的方式链接:

infixr 5 :>
data Statements (g :: [(Symbol, *)]) (h :: [(Symbol,*)]) where
  Done :: Statements g g
  (:>) :: Statement g h -> Statements h i -> Statements g i

表达式

表达式与您的原始定义几乎没有变化，只是它们现在有作用域和一个新的构造函数 EVar让我们取消引用先前声明的变量(使用 ScopedSymbol )，从而为我们提供适当类型的表达式。

data Exp (g :: [(Symbol,*)]) (t :: *) where
  EVar    :: ScopedSymbol g a -> Exp g a
  EBool   :: Bool -> Exp g Bool
  EInt    :: Int  -> Exp g Int
  EAdd    :: Exp g Int -> Exp g Int -> Exp g Int
  ENot    :: Exp g Bool -> Exp g Bool

程式

一个 Program很简单，就是从空作用域开始的一系列语句。我们再次使用存在量化来隐藏我们最终得到的范围。

data Program = forall h. Program (Statements '[] h)

显然可以在 Haskell 中编写子程序并在您的程序中使用它们。在这个例子中，我有一个非常简单的 increment可以这样定义:

increment :: ScopedSymbol g Int -> Statement g g
increment v = Assign v (EAdd (EVar v) (EInt 1))

我已经上传了整个代码片段以及正确的 LANGUAGE此处列出的编译指示和示例 in a self-contained gist .然而，我没有在那里包含任何评论。