haskell - 是否可以在 GADT 定义中使用类型别名？

Question

我一直在为 WebAssembly 指令定义 GADT。许多指令构造函数具有相同的签名:

data Instruction result where
    Add :: Instruction r -> Instruction r -> Instruction r
    Sub :: Instruction r -> Instruction r -> Instruction r
    Mul :: Instruction r -> Instruction r -> Instruction r

使用普通值，您可以简单地为这些二元运算符声明类型别名:

type Binop r = Instruction r -> Instruction r -> Instruction r

但是，当我在 GADT 定义中使用别名时:

{-# LANGUAGE GADTs #-}

module Data.Instruction where

type Binop r = Instruction r -> Instruction r -> Instruction r

data Instruction result where
    Add :: Binop r
    Sub :: Binop r
    Mul :: Binop r

编译失败:

[6 of 6] Compiling Data.Instruction ( src/Data/Instruction.hs, .stack-work/dist/x86_64-osx/Cabal-2.0.1.0/build/Data/Instruction.o )

.../src/Data/Instruction.hs:8:5: error:
    • Data constructor ‘Add’ returns type ‘Binop r’
        instead of an instance of its parent type ‘Instruction result’
    • In the definition of data constructor ‘Add’
      In the data type declaration for ‘Instruction’
   |
11 |     Add :: Binop r
   |     ^

有什么办法可以用 GHC 来实现这一点吗？如果不是，限制的原因是什么？

Answer 1

这是可能的，但不是以您的方式实现的。这在这里确实有效:

type Foo = Bar Int

data Bar a where
  Bar :: Foo

...因为 Foo 实际上具有 Bar a 形式，其中包含 a ~ Int。但是，这不会:

type Foo = Int -> Bar Int

data Bar a where
  Bar :: Foo

它无法工作，因为 GADT 构造函数

data Bar a where
  Bar :: Int -> Bar Int

实际上并没有声明“可逆函数”Bar::Int -> Bar Int。相反，它声明了如下内容:

data Bar' a = Bar' (a <a href="http://hackage.haskell.org/package/base-4.11.0.0/docs/Data-Type-Equality.html#t::-126-:" rel="noreferrer noopener nofollow">:~:</a> Int) Int

即，它封装了一个(运行时可读的)证明，证明a参数类型实际上是Int。 GADT 语法将其隐藏在幕后，但这意味着您不能仅用类型同义词替换 Int -> Bar Int，因为该类型同义词不知道如何封装这个类型相等证明。

...考虑一下，我不确定为什么我的第一个示例实际上有效，因为它似乎遇到了同样的问题...