Блог

Главная - Вопросы по программированию - Равенство для GADTS, которые стирают параметр типа

Равенство для GADTS, которые стирают параметр типа

#haskell #gadt

Вопрос:

Я не могу реализовать экземпляр Eq для следующего типобезопасного DSL для выражений, реализованных с помощью GADTs.

 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' amp;amp; y == y'
  If c t e == If c' t' e' = c == c' amp;amp; t == t' amp;amp; e == e'
  Equal x y == Equal x' y' = x == x' amp;amp; 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 ‘(amp;amp;)’, namely ‘x == x'’
      In the expression: x == x' amp;amp; 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' amp;amp; y == y'
   |

I believe the reason is that the constructor Equal «forgets» the value of the type parameter a of its subexpressions and there is no way for the typechecker to ensure subexpressions x and y both have the same type Expr a .

I tried adding one more type parameter to Expr a to keep track of the type of subexpressions:

 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

Этот подход мне не кажется масштабируемым, еще раз добавляются конструкторы с подвыражениями разных типов.

Все это заставляет меня думать, что я неправильно использую GADTs для реализации такого рода 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' amp;amp; y == y'
  If c t e == If c' t' e' = c == c' amp;amp; t == t' amp;amp; e == e'
  Equal x y == Equal x' y' = x == x' amp;amp; 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)

Ответ №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' amp;amp; y == y'
  If c t e  == If c' t' e' = c == c' amp;amp; t == t' amp;amp; e == e'
  Equal x y == Equal x' y' = case (tyExpr x, tyExpr x') of
     (TyInt,  TyInt ) -> x == x' amp;amp; y == y'
     (TyBool, TyBool) -> x == x' amp;amp; 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' amp;amp; y == y'
  If c t e  == If c' t' e' = c == c' amp;amp; t == t' amp;amp; e == e'
  Equal x y == Equal x' y' = case cast (x,y) of
     Just (x2, y2) -> x2 == x' amp;amp; 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' amp;amp; eqExpr y y'
eqExpr (If c t e)  (If c' t' e') = eqExpr c c' amp;amp; eqExpr t t' amp;amp; eqExpr e e'
eqExpr (Equal x y) (Equal x' y') = eqExpr x x' amp;amp; eqExpr y y'
eqExpr _           _             = False

В Eq таком случае данный экземпляр является особым случаем.

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

Заключительная нота

Как отметил Джозеф Сибл в комментариях, во всех этих подходах нам не нужен 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 вывода типа, чтобы мы могли использовать == .

Комментарии:

1. Я собирался опубликовать ответ, в котором говорится, что вы можете реализовать Equal x y == Equal x' y' , выполнив анализ случаев x, y, x’ и y’, поскольку это дает вам представление о параметрах типа. Но реализация этого в качестве общей функции гетерогенного равенства, а не захоронение одного и того же кода в одном случае экземпляра Eq, намного лучше, чем моя идея.

2. Этот ответ должен быть обязательным для чтения для всех, кто говорит, что шашки типа просто мешают им. Отличный прагматичный пример использования системы типов для подтверждения свойств ваших типов данных.

3. Вам это нужно instance Eq a => Eq (Expr a) where ? Разве это не может быть просто так instance Eq (Expr a) where ?

4. @JosephSible-Восстанови права на монику! Нам действительно это не нужно. Мы также не нуждаемся Eq a в GADT.

Метки: ,