Подтвердить что ты не робот

Упрощение GADT с Uniplate

Я пытаюсь ответить на qaru.site/info/413509/..., но единственное решение, которое я придумал до сих пор, довольно уродливо.

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

В принципе, у нас есть GADT, который разрешает либо Expression Int, либо Expression Bool (игнорируя codataIf = If (B True) codataIf codataIf):

data Expression a where
    I :: Int -> Expression Int
    B :: Bool -> Expression Bool
    Add :: Expression Int  -> Expression Int  -> Expression Int
    Mul :: Expression Int  -> Expression Int  -> Expression Int
    Eq  :: Expression Int  -> Expression Int  -> Expression Bool
    And :: Expression Bool -> Expression Bool -> Expression Bool
    Or  :: Expression Bool -> Expression Bool -> Expression Bool
    If  :: Expression Bool -> Expression a    -> Expression a -> Expression a

И (в моей версии проблемы) мы хотим иметь возможность оценить дерево выражений снизу вверх, используя простую операцию, чтобы объединить листья в новый лист:

step :: Expression a -> Expression a
step = \case
  Add (I x) (I y)   -> I $ x + y
  Mul (I x) (I y)   -> I $ x * y
  Eq (I x) (I y)    -> B $ x == y
  And (B x) (B y)   -> B $ x && y
  Or (B x) (B y)    -> B $ x || y
  If (B b) x y      -> if b then x else y
  z                 -> z

Я с трудом использовал DataDeriving для вывода экземпляров uniplate и Biplate (которые, возможно, должны были быть красным флагом), поэтому Я применил собственные экземпляры uniplate для Expression Int, Expression Bool и Biplate экземпляров для (Expression a) (Expression a), (Expression Int) (Expression Bool) и (Expression Bool) (Expression Int).

Позвольте мне придумать эти восходящие обходы:

evalInt :: Expression Int -> Expression Int
evalInt = transform step

evalIntBi :: Expression Bool -> Expression Bool
evalIntBi = transformBi (step :: Expression Int -> Expression Int)

evalBool :: Expression Bool -> Expression Bool
evalBool = transform step

evalBoolBi :: Expression Int -> Expression Int
evalBoolBi = transformBi (step :: Expression Bool -> Expression Bool)

Но так как каждый из них может выполнять только одно преобразование (объедините Int листья или Bool листья, но не все), они не могут выполнить полное упрощение, но должны быть связаны друг с другом вручную:

λ example1
If (Eq (I 0) (Add (I 0) (I 0))) (I 1) (I 2)
λ evalInt it
If (Eq (I 0) (I 0)) (I 1) (I 2)
λ evalBoolBi it
If (B True) (I 1) (I 2)
λ evalInt it
I 1
λ example2
If (Eq (I 0) (Add (I 0) (I 0))) (B True) (B False)
λ evalIntBi it
If (Eq (I 0) (I 0)) (B True) (B False)
λ evalBool it
B True

Моим хакерским обходным решением было определить экземпляр uniplate для Either (Expression Int) (Expression Bool):

type  WExp = Either (Expression Int) (Expression Bool)

instance Uniplate WExp where
  uniplate = \case
      Left (Add x y)    -> plate (i2 Left Add)  |* Left x  |* Left y
      Left (Mul x y)    -> plate (i2 Left Mul)  |* Left x  |* Left y
      Left (If b x y)   -> plate (bi2 Left If)  |* Right b |* Left x  |* Left y
      Right (Eq x y)    -> plate (i2 Right Eq)  |* Left x  |* Left y
      Right (And x y)   -> plate (b2 Right And) |* Right x |* Right y
      Right (Or x y)    -> plate (b2 Right Or)  |* Right x |* Right y
      Right (If b x y)  -> plate (b3 Right If)  |* Right b |* Right x |* Right y
      e                 -> plate e
    where i2 side op (Left x) (Left y) = side (op x y)
          i2 _ _ _ _ = error "type mismatch"
          b2 side op (Right x) (Right y) = side (op x y)
          b2 _ _ _ _ = error "type mismatch"
          bi2 side op (Right x) (Left y) (Left z) = side (op x y z)
          bi2 _ _ _ _ _ = error "type mismatch"
          b3 side op (Right x) (Right y) (Right z) = side (op x y z)
          b3 _ _ _ _ _ = error "type mismatch"

evalWExp :: WExp -> WExp
evalWExp = transform (either (Left . step) (Right . step))

Теперь я могу сделать полное упрощение:

λ evalWExp . Left $ example1
Left (I 1)
λ evalWExp . Right $ example2
Right (B True)

Но количество error и обертывание/разворот, которые я должен был сделать, чтобы сделать эту работу, просто заставляет это чувствовать себя нелестно и неправильно для меня.

Есть ли правильный способ решить эту проблему с помощью uniplate?

4b9b3361

Ответ 1

Невозможно решить эту проблему с помощью uniplate, но есть правильный способ решить эту проблему с помощью того же механизма. Библиотека uniplate не поддерживает унификацию типа данных с типом * -> *, но мы можем создать другой класс для его размещения. Здесь небольшая минимальная библиотека для разных типов * -> *. Он основан на текущей версии git Uniplate, которая была изменена для использования Applicative вместо Str.

{-# LANGUAGE RankNTypes #-}

import Control.Applicative
import Control.Monad.Identity

class Uniplate1 f where
    uniplate1 :: Applicative m => f a -> (forall b. f b -> m (f b)) -> m (f a)

    descend1 :: (forall b. f b -> f b) -> f a -> f a
    descend1 f x = runIdentity $ descendM1 (pure . f) x

    descendM1 :: Applicative m => (forall b. f b -> m (f b)) -> f a -> m (f a)
    descendM1 = flip uniplate1

transform1 :: Uniplate1 f => (forall b. f b -> f b) -> f a -> f a
transform1 f = f . descend1 (transform1 f)

Теперь мы можем написать экземпляр Uniplate1 для Expression:

instance Uniplate1 Expression where
    uniplate1 e p = case e of
        Add x y -> liftA2 Add (p x) (p y)
        Mul x y -> liftA2 Mul (p x) (p y)
        Eq  x y -> liftA2 Eq  (p x) (p y)
        And x y -> liftA2 And (p x) (p y)
        Or  x y -> liftA2 Or  (p x) (p y)
        If  b x y -> pure If <*> p b <*> p x <*> p y
        e -> pure e

Этот экземпляр очень похож на функцию emap, которую я написал в мой ответ на исходный вопрос, за исключением того, что этот экземпляр помещает каждый элемент в Applicative Functor. descend1 просто поднимает свой аргумент на Identity и runIdentity результат, делая desend1 идентичным emap. Таким образом, transform1 идентичен postmap из предыдущего ответа.

Теперь мы можем определить reduce в терминах transform1.

reduce = transform1 step

Этого достаточно, чтобы запустить пример:

"reduce"
If (And (B True) (Or (B False) (B True))) (Add (I 1) (Mul (I 2) (I 3))) (I 0)
I 7