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

Question

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

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

По сути, у нас есть 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?

Answer 1

Не существует правильного способа решить эту проблему с помощью uniplate, но есть правильный способ решить эту проблему с помощью того же механизма. Библиотека uniplate не поддерживает uniplating тип данных с видом * -> *, но мы можем создать другой класс, чтобы приспособиться к этому. Вот небольшая минимальная библиотека 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 Функция, которую я написал в своем ответе на исходный вопрос, за исключением того, что этот экземпляр помещает каждый элемент в ApplicativeFunctor, 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