Има ли нещо като разширения за типове в 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