Чистая альтернатива обширному сопоставлению шаблонов в Haskell

Ответ 1

Одна вещь, которую вы можете сделать, - это упростить, когда вы строите, а не сначала конструируете, а затем многократно разрушаете. Итак:

module Simple (Expression, true, false, var, not, or, and) where

import Prelude hiding (not, or, and)

data Expression
    = Literal Bool
    | Variable String
    | Not Expression
    | Or Expression Expression
    | And Expression Expression
    deriving (Eq, Ord, Read, Show)

true = Literal True
false = Literal False
var = Variable

not (Literal True) = false
not (Literal False) = true
not x = Not x

or (Literal True) _ = true
or _ (Literal True) = true
or x y = Or x y

and (Literal False) _ = false
and _ (Literal False) = false
and x y = And x y

Мы можем попробовать это в ghci:

> and (var "x") (and (var "y") false)
Literal False

Обратите внимание, что конструкторы не экспортируются: это гарантирует, что люди, создающие один из них, не смогут избежать процесса упрощения. На самом деле это может быть недостатком; иногда приятно видеть "полную" форму. Стандартный подход к решению этого - сделать экспортированные интеллектуальные конструкторы частью типа-класса; вы можете использовать их для создания "полной" формы или "упрощенного" способа. Чтобы избежать необходимости определять тип дважды, мы могли бы использовать параметр newtype или phantom; Я буду выбирать для последнего здесь, чтобы уменьшить шум при сопоставлении с образцом.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
module Simple (Format(..), true, false, var, not, or, and) where

import Prelude hiding (not, or, and)

data Format = Explicit | Simplified

data Expression (a :: Format)
    = Literal Bool
    | Variable String
    | Not (Expression a)
    | Or (Expression a) (Expression a)
    | And (Expression a) (Expression a)
    deriving (Eq, Ord, Read, Show)

class Expr e where
    true, false :: e
    var :: String -> e
    not :: e -> e
    or, and :: e -> e -> e

instance Expr (Expression Explicit) where
    true = Literal True
    false = Literal False
    var = Variable
    not = Not
    or = Or
    and = And

instance Expr (Expression Simplified) where
    true = Literal True
    false = Literal False
    var = Variable

    not (Literal True) = false
    not (Literal False) = true
    not x = Not x

    or (Literal True) _ = true
    or _ (Literal True) = true
    or x y = Or x y

    and (Literal False) _ = false
    and _ (Literal False) = false
    and x y = And x y

Теперь в ghci мы можем "запустить" один и тот же термин двумя разными способами:

> :set -XDataKinds
> and (var "x") (and (var "y") false) :: Expression Explicit
And (Variable "x") (And (Variable "y") (Literal False))
> and (var "x") (and (var "y") false) :: Expression Simplified
Literal False

Возможно, вам захочется добавить дополнительные правила позже; например, возможно, вы хотите:

and (Variable x) (Not (Variable y)) | x == y = false
and (Not (Variable x)) (Variable y) | x == y = false

Повторяя оба "заказа" шаблонов, это немного раздражает. Мы должны отвлечься от этого! Объявление данных и классы будут одинаковыми, но мы добавим вспомогательную функцию eitherOrder и используем ее в определениях and и or. Здесь более полный набор упрощений, использующих эту идею (и нашу окончательную версию модуля):

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
module Simple (Format(..), true, false, var, not, or, and) where

import Data.Maybe
import Data.Monoid
import Prelude hiding (not, or, and)
import Control.Applicative ((<|>))

data Format = Explicit | Simplified

data Expression (a :: Format)
    = Literal Bool
    | Variable String
    | Not (Expression a)
    | Or (Expression a) (Expression a)
    | And (Expression a) (Expression a)
    deriving (Eq, Ord, Read, Show)

class Expr e where
    true, false :: e
    var :: String -> e
    not :: e -> e
    or, and :: e -> e -> e

instance Expr (Expression Explicit) where
    true = Literal True
    false = Literal False
    var = Variable
    not = Not
    or = Or
    and = And

eitherOrder :: (e -> e -> e)
            -> (e -> e -> Maybe e)
            -> e -> e -> e
eitherOrder fExplicit fSimplified x y = fromMaybe
    (fExplicit x y)
    (fSimplified x y <|> fSimplified y x)

instance Expr (Expression Simplified) where
    true = Literal True
    false = Literal False
    var = Variable

    not (Literal True) = false
    not (Literal False) = true
    not (Not x) = x
    not x = Not x

    or = eitherOrder Or go where
        go (Literal True) _ = Just true
        go (Literal False) x = Just x
        go (Variable x) (Variable y) | x == y = Just (var x)
        go (Variable x) (Not (Variable y)) | x == y = Just true
        go _ _ = Nothing

    and = eitherOrder And go where
        go (Literal True) x = Just x
        go (Literal False) _ = Just false
        go (Variable x) (Variable y) | x == y = Just (var x)
        go (Variable x) (Not (Variable y)) | x == y = Just false
        go _ _ = Nothing

Теперь в ghci мы можем сделать более сложные упрощения, например:

> and (not (not (var "x"))) (var "x") :: Expression Simplified
Variable "x"

И хотя мы только написали один порядок правила перезаписи, оба заказа работают правильно:

> and (not (var "x")) (var "x") :: Expression Simplified
Literal False
> and (var "x") (not (var "x")) :: Expression Simplified
Literal False

Ответ 2

В основном проблема заключается в том, что вы должны снова и снова выписывать simplify подвыражений в каждом разделе. Было бы лучше сначала получить все подвыражения, сделанные до рассмотрения законов, связанных с оператором верхнего уровня. Один простой способ - добавить вспомогательную версию simplify, которая не перезаписывает:

simplify :: Expression -> Expression
simplify (Literal b) = Literal b
simplify (Variable s) = Variable s
simplify (Not e) = simplify' . Not $ simplify e
simplify (And a b) = simplify' $ And (simplify a) (simplify b)
simplify (Or a b) = simplify' $ Or (simplify a) (simplify b)

simplify' :: Expression -> Expression
simplify' (Not (Literal b)) = Literal $ not b
simplify' (And (Literal False) _) = Literal False
...

С небольшим количеством операций, которые у вас есть в буле, это, вероятно, самый разумный подход. Однако с большим количеством операций дублирование в simplify все равно можно было бы избежать. С этой целью вы можете объединить унарные и двоичные операции с общим конструктором:

data Expression 
    = Literal Bool 
    | Variable String
    | BoolPrefix BoolPrefix Expression 
    | BoolInfix BoolInfix Expression Expression 
    deriving Eq

data BoolPrefix = Negation
data BoolInfix  = AndOp | OrOp

а затем у вас есть только

simplify (Literal b) = Literal b
simplify (Variable s) = Variable s
simplify (BoolPrefix bpf e) = simplify' . BoolPrefix bpf $ simplify e
simplify (BoolInfix bifx a b) = simplify' $ BoolInfix bifx (simplify a) (simplify b)

Очевидно, что это делает simplify' более неудобным, хотя, возможно, не такая хорошая идея. Однако вы можете обойти эти синтаксические накладные расходы, указав специализированные синтаксисы шаблонов :

{-# LANGUAGE PatternSynonyms #-}

pattern Not :: Expression -> Expression
pattern Not x = BoolPrefix Negation x

infixr 3 :∧
pattern (:∧) :: Expression -> Expression -> Expression
pattern a:∧b = BoolInfix AndOp a b

infixr 2 :∨
pattern (:∨) :: Expression -> Expression -> Expression
pattern a:∨b = BoolInfix OrOp a b

В этом отношении, возможно, также

pattern F, T :: Expression
pattern F = Literal False
pattern T = Literal True

С этим вы можете написать

simplify' :: Expression -> Expression
simplify' (Not (Literal b)) = Literal $ not b
simplify' (F :∧ _) = F
simplify' (_ :∧ F) = F
simplify' (T :∨ _) = T
simplify' (a :∧ Not b) | a==b  = T
...

Я должен добавить оговорку: когда я попытался что-то похожее на синтаксисы шаблонов, а не на логические, но аффинные сопоставления, это сделало компилятор чрезвычайно медленным. (Кроме того, GHC-7.10 еще не поддерживал синонимы полиморфных паттернов, это немного изменилось.)

Отметим также, что все это, как правило, не дает простейшей возможной формы - для этого вам нужно найти неподвижную точку simplify.

Ответ 3

Я думаю, Эйнштейн сказал: "Упростите как можно больше, но не более". У вас есть сложный тип данных и, соответственно, сложная концепция, поэтому я предполагаю, что любая техника может быть настолько чище для данной проблемы.

Тем не менее, первый вариант заключается в использовании структуры case.

simplify x = case x of
   Literal _  -> x
   Variable _ -> x
   Not e      -> simplifyNot $ simplify e
   ...
   where
     sharedFunc1 = ...
     sharedFunc2 = ...

Это имеет дополнительное преимущество, включая общие функции, которые будут использоваться во всех случаях, но не в пространстве имен верхнего уровня. Мне также нравится, как дела освобождаются от их круглых скобок. (Также обратите внимание, что в первых двух случаях я просто возвращаю исходный термин, а не создавая новый). Я часто использую эту структуру, чтобы просто вырвать другие упрощенные функции, как в случае Not.

Эта проблема, в частности, может основываться на Expression на базовом функторе, так что вы можете fmap упростить подвыражения, а затем выполнить конкретные комбинации данного случая. Он будет выглядеть примерно так:

simplify :: Expression' -> Expression'
simplify = Exp . reduce . fmap simplify . unExp

Шаги в этом разворачивают Expression' в базовое представление функтора, сопоставляя упрощение по лежащему в его основе термину, а затем уменьшая это упрощение и завершая создание нового Expression'

{-# Language DeriveFunctor #-}

newtype Expression' = Exp { unExp :: ExpressionF Expression' }

data ExpressionF e
  = Literal Bool 
  | Variable String
  | Not e 
  | Or e e
  | And e e
  deriving (Eq,Functor)

Теперь я переместил сложность в функцию reduce, которая лишь немного менее сложна, потому что ей не нужно беспокоиться о том, чтобы сначала уменьшить подтермер. Но теперь он будет содержать только бизнес-логику объединения одного термина с другим.

Это может быть или не быть хорошей техникой для вас, но это может облегчить некоторые улучшения. Например, если на вашем языке можно сформировать недопустимые выражения, вы можете упростить это с помощью Maybe ошибок с оценкой.

simplifyMb :: Expression' -> Maybe Expression'
simplifyMb = fmap Exp . reduceMb <=< traverse simplifyMb . unExp

Здесь traverse применит simplfyMb к подтемам ExpressionF, что приведет к выражению Maybe subterms, ExpressionF (Maybe Expression'), а затем, если любые подтермы Nothing, он вернет Nothing, если все Just x, оно вернет Just (e::ExpressionF Expression'). Траверс фактически не разделен на отдельные этапы, но это легче объяснить, как если бы это было так. Также обратите внимание, вам понадобятся языковые прагмы для DeriveTraversable и DeriveFoldable, а также вывод операторов типа ExpressionF.

Недостаток? Ну, для одного грязь вашего кода будет тогда в куче Exp оберток повсюду. Рассмотрим применение simplfyMb простого слова ниже:

simplifyMb (Exp $ Not (Exp $ Literal True))

Это также очень полезно, если вы поймете traverse и fmap шаблон выше, вы можете использовать его во многих местах, так что хорошо. Я также считаю, что определение упрощения таким образом делает его более надежным, чем могут возникнуть конкретные конструкции ExpressionF. Он не упоминает их, поэтому глубокое упрощение не будет затронуто рефакторами. С другой стороны функция уменьшения.

Ответ 4

Выполняя свою идею Binary Op Expression Expression, у нас может быть тип данных:

data Expression
    = Literal Bool
    | Variable String
    | Not Expression
    | Binary Op Expression Expression
    deriving Eq

data Op = Or | And deriving Eq

И вспомогательная функция

{-# LANGUAGE ViewPatterns #-}

simplifyBinary  :: Op -> Expression -> Expression -> Expression
simplifyBinary  binop (simplify -> leftexp) (simplify -> rightexp) =
    case oneway binop leftexp rightexp ++ oneway binop rightexp leftexp of
        simplified : _ -> simplified
        []             -> Binary binop leftexp rightexp
  where
    oneway :: Op -> Expression -> Expression -> [Expression]
    oneway And (Literal False) _ = [Literal False]
    oneway Or  (Literal True)  _ = [Literal True]
    -- more cases here
    oneway _   _               _ = []

Идея состоит в том, что вы ставите случаи упрощения в oneway, а затем simplifyBinary позаботится об изменении аргументов, чтобы избежать необходимости писать симметричные случаи.

Ответ 5

Вы можете написать общий упроститель для всех двоичных операций:

simplifyBinWith :: (Bool -> Bool -> Bool) -- the boolean operation
                -> (Expression -> Expression -> Expression) -- the constructor
                -> Expression -> Expression -- the two operands
                -> Expression) -- the simplified result
simplifyBinWith op cons a b = case (simplify a, simplify b) of
    (Literal x, Literal y) -> Literal (op x y)
    (Literal x, b')        -> tryAll (x `op`) b'
    (a',        Literal y) -> tryAll (`op` y) a'
    (a',        b')        -> cons a' b'
  where
    tryAll f term = case (f True, f False) of -- what would f do if term was true of false
      (True,  True)  -> Literal True
      (True,  False) -> term
      (False, True)  -> Not term
      (False, False) -> Literal False

Таким образом, ваша функция simplify станет

simplify :: Expression -> Expression
simplify (Not e)   = case simplify e of
    (Literal b) -> Literal (not b)
    e'          -> Not e'
simplify (And a b) = simplifyBinWith (&&) And a b
simplify (Or a b)  = simplifyBinWith (||) Or a b
simplify t         = t

и может быть легко перенесена на более двоичные операции. Это также хорошо работает с идеей Binary Op Expression Expression, вы передадите Op вместо конструктора Expression на simplifyBinWith, и шаблон в simplify может быть обобщен:

simplify :: Expression -> Expression
simplify (Not e)         = case simplify e of
    (Literal b) -> Literal (not b)
    e'          -> Not e'
simplify (Binary op a b) = simplifyBinWith (case op of
    And -> (&&)
    Or -> (||)
    Xor -> (/=)
    Implies -> (<=)
    Equals -> (==)
    …
  ) op a b
simplify t               = t
  where
    simplifyBinWith f op a b = case (simplify a, simplify b) of
      (Literal x, Literal y) -> Literal (f x y)
      …
      (a',        b')        -> Binary op a' b'