Есть ли такие вещи, как "расширения типа" в 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? Если нет, как я должен справиться с этой ситуацией? Эта концепция "типа расширения" введет некоторую двусмысленность, но я считаю, что просто методы вывода типа не будут работать при использовании таких типов, как это, и я могу справиться с этим.

2 ответа

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

data PropQuantifiedLogic a = QuantifiedLogic (PropLogic a)
 | Exists (PropQuantifiedLogic a)
 | Forall (PropQuantifiedLogic a)


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

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)

licensed under cc by-sa 3.0 with attribution.