haskell - 删除类型参数的 GADT 的相等性

Question

我无法实现 Eq 的实例对于以下使用 GADT 实现的表达式的类型安全 DSL。

data Expr a where
  Num :: Int -> Expr Int
  Bool :: Bool -> Expr Bool
  Plus :: Expr Int -> Expr Int -> Expr Int
  If :: Expr Bool -> Expr a -> Expr a -> Expr a
  Equal :: Eq a => Expr a -> Expr a -> Expr Bool

表达式可以是 Bool 类型之一或 Int .有文字的构造函数 Bool和 Num有相应的类型。仅限 Int表达式可以相加(构造函数 Plus)。 If 中的条件表达式的类型应为 Bool而两个分支应该具有相同的类型。还有一个等式表达式 Equal其操作数应具有相同的类型，等式表达式的类型为 Bool .
我实现解释器没有问题 eval对于这个 DSL。它像魅力一样编译和工作:

eval :: Expr a -> a
eval (Num x) = x
eval (Bool x) = x
eval (Plus x y) = eval x + eval y
eval (If c t e) = if eval c then eval t else eval e
eval (Equal x y) = eval x == eval y

但是，我很难实现 Eq 的实例对于 DSL。我尝试了简单的句法相等:

instance Eq a => Eq (Expr a) where
  Num x == Num y = x == y
  Bool x == Bool y = x == y
  Plus x y == Plus x' y' = x == x' && y == y'
  If c t e == If c' t' e' = c == c' && t == t' && e == e'
  Equal x y == Equal x' y' = x == x' && y == y'
  _ == _ = False

它不进行类型检查(使用 ghc 8.6.5 )，错误如下:

[1 of 1] Compiling Main             ( Main.hs, Main.o )

Main.hs:17:35: error:
    • Could not deduce: a2 ~ a1
      from the context: (a ~ Bool, Eq a1)
        bound by a pattern with constructor:
                   Equal :: forall a. Eq a => Expr a -> Expr a -> Expr Bool,
                 in an equation for ‘==’
        at Main.hs:17:3-11
      ‘a2’ is a rigid type variable bound by
        a pattern with constructor:
          Equal :: forall a. Eq a => Expr a -> Expr a -> Expr Bool,
        in an equation for ‘==’
        at Main.hs:17:16-26
      ‘a1’ is a rigid type variable bound by
        a pattern with constructor:
          Equal :: forall a. Eq a => Expr a -> Expr a -> Expr Bool,
        in an equation for ‘==’
        at Main.hs:17:3-11
      Expected type: Expr a1
        Actual type: Expr a2
    • In the second argument of ‘(==)’, namely ‘x'’
      In the first argument of ‘(&&)’, namely ‘x == x'’
      In the expression: x == x' && y == y'
    • Relevant bindings include
        y' :: Expr a2 (bound at Main.hs:17:25)
        x' :: Expr a2 (bound at Main.hs:17:22)
        y :: Expr a1 (bound at Main.hs:17:11)
        x :: Expr a1 (bound at Main.hs:17:9)
   |
17 |   Equal x y == Equal x' y' = x == x' && y == y'
   |  

我相信原因是构造函数 Equal “忘记”类型参数的值 a它的子表达式，并且类型检查器无法确保子表达式 x和 y两者都具有相同的类型 Expr a .
我尝试向 Expr a 添加一个类型参数跟踪子表达式的类型:

data Expr a b where
  Num :: Int -> Expr Int b
  Bool :: Bool -> Expr Bool b
  Plus :: Expr Int b -> Expr Int b -> Expr Int b
  If :: Expr Bool b -> Expr a b -> Expr a b -> Expr a b
  Equal :: Eq a => Expr a a -> Expr a a -> Expr Bool a

instance Eq a => Eq (Expr a b) where
  -- same implementation

eval :: Expr a b -> a
  -- same implementation

这种方法对我来说似乎不可扩展，一旦添加了更多具有不同类型子表达式的构造函数。
这一切让我觉得我确实错误地使用了 GADT 来实现这种 DSL。有没有办法实现 Eq对于这种类型？如果不是，那么在表达式上表达这种类型约束的惯用方式是什么？
完整代码:

{-# LANGUAGE GADTs #-}
 
module Main where

data Expr a where
  Num :: Int -> Expr Int
  Bool :: Bool -> Expr Bool
  Plus :: Expr Int -> Expr Int -> Expr Int
  If :: Expr Bool -> Expr a -> Expr a -> Expr a
  Equal :: Eq a => Expr a -> Expr a -> Expr Bool

instance Eq a => Eq (Expr a) where
  Num x == Num y = x == y
  Bool x == Bool y = x == y
  Plus x y == Plus x' y' = x == x' && y == y'
  If c t e == If c' t' e' = c == c' && t == t' && e == e'
  Equal x y == Equal x' y' = x == x' && y == y'
  _ == _ = False

eval :: Expr a -> a
eval (Num x) = x
eval (Bool x) = x
eval (Plus x y) = eval x + eval y
eval (If c t e) = if eval c then eval t else eval e
eval (Equal x y) = eval x == eval y

main :: IO ()
main = do
  let expr1 = If (Equal (Num 13) (Num 42)) (Bool True) (Bool False)
  let expr2 = If (Equal (Num 13) (Num 42)) (Num 42) (Num 777)
  print (eval expr1)
  print (eval expr2)
  print (expr1 == expr1)

Answer 1

你的问题是在

Equal x y == Equal x' y' = ...

有可能 x和 x'有不同的类型。例如， Equal (Bool True) (Bool True) == Equal (Int 42) (Int 42)类型检查，但我们不能简单地比较 Bool True == Int 42正如我们可能会尝试在 Eq 中做的那样实例。
以下是一些替代解决方案。最后一个(将 == 推广到 eqExpr )对我来说似乎是最简单的，但其他的也很有趣。
使用单例和计算类型
我们从您的原始类型开始

{-# LANGUAGE GADTs #-}
module Main where

data Expr a where
  Num :: Int -> Expr Int
  Bool :: Bool -> Expr Bool
  Plus :: Expr Int -> Expr Int -> Expr Int
  If :: Expr Bool -> Expr a -> Expr a -> Expr a
  Equal :: Eq a => Expr a -> Expr a -> Expr Bool

并定义一个单例 GADT 来表示您拥有的类型

data Ty a where
  TyInt  :: Ty Int
  TyBool :: Ty Bool

然后我们证明你的类型只能是 Int或 Bool ，以及如何从表达式中计算它们。

tyExpr :: Expr a -> Ty a
tyExpr (Num _)     = TyInt
tyExpr (Bool _)    = TyBool
tyExpr (Plus _ _)  = TyInt
tyExpr (If _ t _)  = tyExpr t
tyExpr (Equal _ _) = TyBool

我们现在可以利用它并定义 Eq实例。

instance Eq (Expr a) where
  Num x     == Num y       = x == y
  Bool x    == Bool y      = x == y
  Plus x y  == Plus x' y'  = x == x' && y == y'
  If c t e  == If c' t' e' = c == c' && t == t' && e == e'
  Equal x y == Equal x' y' = case (tyExpr x, tyExpr x') of
     (TyInt,  TyInt ) -> x == x' && y == y'
     (TyBool, TyBool) -> x == x' && y == y'
     _                -> False
  _ == _ = False

使用可键入
我们对原来的 GADT 稍作修改:

import Data.Typeable
  
data Expr a where
  Num :: Int -> Expr Int
  Bool :: Bool -> Expr Bool
  Plus :: Expr Int -> Expr Int -> Expr Int
  If :: Expr Bool -> Expr a -> Expr a -> Expr a
  Equal :: (Typeable a, Eq a) => Expr a -> Expr a -> Expr Bool

然后我们可以尝试将值转换为正确的类型:如果转换失败，我们有两个 Equal s 在不同类型之间，所以我们可以返回 False .

instance Eq (Expr a) where
  Num x     == Num y       = x == y
  Bool x    == Bool y      = x == y
  Plus x y  == Plus x' y'  = x == x' && y == y'
  If c t e  == If c' t' e' = c == c' && t == t' && e == e'
  Equal x y == Equal x' y' = case cast (x,y) of
     Just (x2, y2) -> x2 == x' && y2 == y'
     Nothing       -> False
  _ == _ = False

泛化到异构平等
我们可以使用原始的 GADT:

data Expr a where
  Num :: Int -> Expr Int
  Bool :: Bool -> Expr Bool
  Plus :: Expr Int -> Expr Int -> Expr Int
  If :: Expr Bool -> Expr a -> Expr a -> Expr a
  Equal :: Eq a => Expr a -> Expr a -> Expr Bool

并编写一个异构相等测试，即使两个表达式的类型不同，它也可以工作:

eqExpr :: Expr a -> Expr b -> Bool
eqExpr (Num x)     (Num y)       = x == y
eqExpr (Bool x)    (Bool y)      = x == y
eqExpr (Plus x y)  (Plus x' y')  = eqExpr x x' && eqExpr y y'
eqExpr (If c t e)  (If c' t' e') = eqExpr c c' && eqExpr t t' && eqExpr e e'
eqExpr (Equal x y) (Equal x' y') = eqExpr x x' && eqExpr y y'
eqExpr _           _             = False

Eq实例是一个特例。

instance Eq (Expr a) where
  (==) = eqExpr

最后一点
正如 Joseph Sible 在评论中指出的那样，在所有这些方法中，我们不需要 Eq a实例中的上下文。我们可以简单地删除它:

instance {- Eq a => -} Eq (Expr a) where
   ...

此外，原则上我们甚至不需要 Eq a。在 Equal 的定义中，所以我们可以简化我们的 GADT:

data Expr a where
  Num :: Int -> Expr Int
  Bool :: Bool -> Expr Bool
  Plus :: Expr Int -> Expr Int -> Expr Int
  If :: Expr Bool -> Expr a -> Expr a -> Expr a
  Equal :: Expr a -> Expr a -> Expr Bool

但是，如果我们这样做， eval :: Expr a -> a 的定义在 Equal 中变得更加复杂在这种情况下，我们可能需要使用 tyExpr 之类的东西推断类型，以便我们可以使用 == .