Fix, «добавление» конструкторов и деконструкция [Haskell]

[arseniiv]

Решил написать кое-что для манипулирования формулами нулевого и первого порядка. Притом, чтобы не дублировать код, сделал так:

Используется синтаксис Haskell

data ShallowFormula0 a uo bo f = Atom a
                               | Un uo f
                               | Bin bo f f
                               deriving (Eq, Ord)

data ShallowFormula1 a uo bo q f = F0 (ShallowFormula0 a uo bo f)
                                 | Q q f
                                 deriving (Eq, Ord)

type Formula0 = Fix (ShallowFormula0 Prop UnOp BinOp)

type Formula1 = Fix (ShallowFormula1 (Pred Term) UnOp BinOp Quantifier)

и сделал их также инстансами класса

Используется синтаксис Haskell

class Formula f a uo bo | f -> a, f -> uo, f -> bo where
  -- smart constructors
  atom       :: a -> f
  unary      :: uo -> f -> f
  binary     :: bo -> f -> f -> f
  quantif    :: Quantifier -> f -> Formula1
  -- преобразования туда-сюда без потерь и с потерями
  firstOrder :: f -> Formula1
  truncate   :: f -> Formula0
  -- и, из-за использования индексов де Брёйна в Formula1,
  isValid    :: f -> Bool

позволяющего конструировать их единообразно. А что делать с деконструкцией? Включить в класс набор функций asAtom :: f -> Maybe a, asQuantif :: f -> (q, f) etc.? Чего-то резко забыл, как принято деконструировать ADT’ы.

Заодно принимаю предложения по переименованию (Formula1 как-то не с тем ассоциируется) и переделке этих типов — сейчас в коде инстанса Formula Formula1 (Pred Term) UnOp BinOp в двух методах двухуровневый матчинг, в одном из уровней по конструкторам ShallowFormula0, что явно не дело (может, есть смысл сделать по типу на конструктор, а потом собрать их в оба нужных типа как-то иначе, перераспределив код (отфакторизовав какие-нибудь классы и инстансы, возможно) к этим мелким типам, а не двум конечным? Я явно что-то упускаю.

Возможно, и ну его, и работать только с формулами первого порядка, т. к. формулы нулевого полностью вкладываются (пропозициональные переменные = нульместные предикатные символы), но ещё подумываю, начав с одного представления правил вывода

Используется синтаксис Haskell

data InfRule f = InfRule {
  arity :: Int,
  tryApply :: [f] -> Maybe f,
  isApplied :: [f] -> f -> Bool
}

-- пример:
ruleHypothesis :: Formula f a uo bo => f -> InfRule f
ruleHypothesis fh = InfRule {
  arity = 0,
  tryApply = tryApply',
  isApplied = isApplied'
} where
  tryApply' [] = Just fh
  tryApply' _  = Nothing
  isApplied' [] fh -> True
  isApplied' _  _  -> False

перейти потом к более правильному на основе схем формул. Их тип получился бы аналогично ShallowFormula1 «добавлением конструктора». Так что в любом случае issue имеется.

[Xaositect]

arseniiv в сообщении #1031144 писал(а):

позволяющего конструировать их единообразно. А что делать с деконструкцией? Включить в класс набор функций asAtom :: f -> Maybe a, asQuantif :: f -> (q, f) etc.? Чего-то резко забыл, как принято деконструировать ADT’ы.

Катаморфизмы же. (a -> x) -> (uo -> x -> x) -> (bo -> x -> x -> x) -> (Formula0 -> x)

Как-то я плохо понимаю этот Ваш класс Formula. Если он для формул первого порядка, то почему там не упоминается параметр для типа кванторов, как в Formula1?

[arseniiv]

Xaositect в сообщении #1031155 писал(а):

Как-то я плохо понимаю этот Ваш класс Formula. Если он для формул первого порядка, то почему там не упоминается параметр для типа кванторов, как в Formula1?

Есть и инстанс Formula Formula0 Prop UnOp BinOp.

Xaositect в сообщении #1031155 писал(а):

Катаморфизмы же. (a -> x) -> (uo -> x -> x) -> (bo -> x -> x -> x) -> (Formula0 -> x)

О, спасибо. Катаморфизмы я уже даже немного использовал как раз здесь, но с конкретными типами, а в класс поместить метод как-то не догадался.

[Xaositect]

А кстати, чем квантор не унарный оператор?

[arseniiv]

Хорошее замечание, я как-то не усмотрел, а сейчас тоже вижу. Теперь есть что переписать и сравнить.

[arseniiv]

[Time skip]

Со времени этой темы прошло сколько-то времени и я успел найти, что есть более удобный, чем Data.Fix, пакет для обобщённых свёрток, recursion-schemes. Можно определять свои типы данных нормальным образом и выводить по ним соответствующие функторы с помощью Template Haskell; можно также определять функтор и «замкнутый тип» оба отдельно (или брать например имеющиеся — допустим, Maybe и Natural) и писать для их связи несколько инстансов, которые этот пакет и использует в определении свёрток. Притом там всё так же есть и Fix, если понадобится. И ещё куча вещей, в которых я не разбираюсь, но которые могут внезапно понадобиться при обобщении кода.