Есть ли в Haskell такие вещи, как расширения типов?

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

У меня есть полиморфный тип Haskell для представления терминов в пропозициональной логике:

 data PropLogic a = Prop a | Tautology | Contradiction | And (PropLogic a) (PropLogic a)
                | Or (PropLogic a) (PropLogic a) | Implies (PropLogic a) (PropLogic a)
                | Not (PropLogic a)
     deriving (Eq,Show)

Проблема в том, что мне также нужен аналогичный полиморфный тип для логики высказываний с операторами квантификации:

data PropQuantifiedLogic a = Prop a | Tautology | Contradiction | And (PropQuantifiedLogic a) (PropQuantifiedLogic a)
                | Or (PropQuantifiedLogic a) (PropQuantifiedLogic a) | Implies (PropQuantifiedLogic a) (PropQuantifiedLogic a)
                | Not (PropQuantifiedLogic a) | Forall (PropQuantifiedLogic a)
                | Exists (PropQuantifiedLogic a)
     deriving (Eq,Show)

Теперь я мог бы просто добавить префикс к имени каждого конструктора значений, где и PropLogic, и PropQuantifiedLogic имеют конфликтующие имена, но дело в том, что я хочу создать много таких типов, которые будут иметь много конфликтующих конструкторов значений: Модальная логика тип, тип временной логики и т. д., и создание новых префиксов для каждого из них быстро станет уродливым.

То, что я действительно хочу сделать, это что-то вроде:

extendtype PropQuantifiedLogic a = PropLogic a | Exists (PropQuantifiedLogic a)
                                 | Forall (PropQuantifiedLogic a)

что было бы эквивалентно первому определению PropQuantifiedLogic и выполняло бы проверку типов.

Можно ли сделать что-то подобное в Haskell? Если нет, то как мне поступить в этой ситуации? Эта концепция «типа расширения» внесла бы некоторую двусмысленность, но я считаю, что просто вывод типа не будет работать при использовании таких типов, и я могу с этим справиться.


haskell algebraic-data-types
person Nathan BeDell    schedule 06.08.2014    source источник
comment
Ocaml имеет функцию полиморфных вариантов, которая делает что-то похожее на то, что вы просите. Насколько я знаю, нет аналога Haskell.   -  person hugomg    schedule 06.08.2014

Ответы (2)


arrow_upward
7
arrow_downward

Вы всегда можете реализовать это как

 data PropFrame a b = OrF b b | AndF b b ... | Prop a | Top

А потом

type Prop a = Fix (PropFrame a)

Затем вы можете добавить новый примитив

data QualifiedF a b = All (b -> b) | Exists (b -> b) | LiftProp (PropFrame a b)
type Qualified a = Fix (QualifiedF a)

Это немного уродливее, но его можно подсластить с помощью -XPatternSynonyms. Основная идея здесь состоит в том, чтобы выделить проблемный рекурсивный случай в явный параметр и использовать Fix для восстановления рекурсии.

Пример использования

qand :: Qualified a -> Qualified a -> Qualified a
qand l r = Fix (LiftProp (AndF l r))

orOrAll :: (Qualified a -> Qualified a) -> Qualified a
orOrAll f = Fix (All f) `qand` Fix (Exists f)
person Daniel Gratzer    schedule 06.08.2014

arrow_upward
1
arrow_downward

Вы можете использовать PropLogic a и добавить дополнительный конструктор QuantifiedLogic:

data PropQuantifiedLogic a =  QuantifiedLogic (PropLogic a)
                            | Exists (PropQuantifiedLogic a)
                            | Forall (PropQuantifiedLogic a)
person viorior    schedule 06.08.2014