Тип класса из подмножества класса рекурсивного типа (или тип из рекурсивного типа) - PullRequest
1 голос
/ 28 апреля 2011

Как мне создать класс рекурсивного типа, который ведет себя как другой класс рекурсивного типа, но не имеет столько экземпляров, как класс «родительский»?

Вот пример:

data Atom = Atom
data (Formula a) => Negation a = Negation a

class Formula a where
instance Formula Atom where
instance (Formula a) => Formula (Negation a) where

class SubFormula a where
instance SubFormula Atom where

Этот код компилируется просто отлично, но когда я добавляю функцию, которая преобразует экземпляр класса супертипа в один из классов подтипа

formulaToSubFormula :: (Formula a, SubFormula b) => a -> b
formulaToSubFormula _ = Atom

Я получаю ошибку

test.hs:12:25:
    Could not deduce (b ~ Atom)
    from the context (Formula a, SubFormula b)
      bound by the type signature for
                 formulaToSubFormula :: (Formula a, SubFormula b) => a -> b
      at test.hs:12:1-28
      `b' is a rigid type variable bound by
          the type signature for
            formulaToSubFormula :: (Formula a, SubFormula b) => a -> b
          at test.hs:12:1
    In the expression: Atom
    In an equation for `formulaToSubFormula':
        formulaToSubFormula _ = Atom

Моим первоначальным намерением было сделать это с обычными типами, но с классами типов проблема кажется более доступной и, как правило, более гибкой.

Например:

data Formula = Atom | Negation Formula | Conjunction Formula Formula
data SubFormula = Atom | Negation SubFormula

Редактировать

Чтобы прояснить, чего я пытаюсь достичь: я хочу проверить на уровне типа, что операция с типом ввода вернет в качестве результата только подмножество этого типа.

Расширенный пример (логика высказываний; нет допустимого синтаксиса Haskell):

data Formula = Atom
             | Negation Formula
             | Disjunction Formula Formula
             | Implication Formula Formula
data SimpleFormula = Atom
                   | Negation SimpleFormula
                   | Disjunction SimpleFormula SimpleFormula

-- removeImplication is not implemented correctly but shows what I mean
removeImplication :: Formula -> SimpleFormula
removeImplication (Implication a b) = (Negation a) `Disjunction` b
removeImplication a = a

Позже у меня может быть формула в конъюнктивной нормальной форме (без действительного синтаксиса Haskell)

data CNF = CNFElem
         | Conjunction CNF CNF
data CNFElem = Atom
             | Negation Atom
             | Disjunction CNFElem CNFElem

Поэтому мне нужен инструмент для представления этой иерархии.

Ответы [ 5 ]

2 голосов
/ 28 апреля 2011

Я сделал это ответом, потому что он довольно длинный, и я хотел форматировать. На самом деле, я бы посчитал это комментарием, так как это скорее мнение, чем решение.

Похоже, что вам нужен расширяемый / модульный синтаксис, хотя вы формулируете свои потребности от общего до определенного - в большинстве статей о расширяемом синтаксисе используется другое представление и рассматривается возможность добавления дополнительные случаи, чтобы сделать «маленький» синтаксис больше.

Есть способы достижения расширяемого синтаксиса в Haskell, например стиль "Наконец без тегов" [1] или два уровня уровня Шеарда и Пасалика [2].

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

[1] http://www.cs.rutgers.edu/~ccshan/tagless/jfp.pdf

[2] http://homepage.mac.com/pasalic/p2/papers/JfpPearl.pdf

2 голосов
/ 28 апреля 2011

преобразует экземпляр класса супертипа в один из классов подтипа

Классы типов Haskell не работают так.

Они не предоставляютпринуждения или подтипы.Ваша функция, возвращающая Atom, может иметь только возвращаемый тип Atom, поскольку она возвращает явный конструктор, который создает Atom значений.

Для таких языков моделирования, как этот, алгебраические типы данных (или иногда обобщенные алгебраические типы данных ) являются наиболее предпочтительным вариантом:

data Proposition
    = LITERAL Bool
    | ALL (Set Proposition)
    | ANY (Set Proposition)
    | NOT Proposition

, который можно сделать произвольно выразительным с помощью параметризованных типов или GADT в зависимости от вашего приложения.

1 голос
/ 28 апреля 2011

Есть много вещей, которые могут происходить здесь, я сомневаюсь, что что-либо включает введение классов типов.(Необычная вещь, которая может появиться здесь, - это ГАДТ.) Следующее очень простое;он просто предназначен для того, чтобы заставить вас говорить то, что вы хотите, более четко ...

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

data Formula a = Atom a 
               | Negation (Formula a)    
               | Conjunction (Formula a) (Formula a) deriving (Show, Eq, Ord)

Вот функция, которая извлекает все подформулы:

subformulas (Atom a) = [Atom a]
subformulas (Negation p) = Negation p : subformulas p
subformulas (Conjunction p q) = Conjunction p q : (subformulas p ++ subformulas q)

Вот тип, который следует использовать, если вы нене размышляю над многими атомными утверждениями:

data Atoms = P | Q | R | S | T | U | V deriving (Show, Eq, Ord)

Вот несколько случайных помощников:

k p q = Conjunction p q
n p  = Negation p
p = Atom P
q = Atom Q
r = Atom R
s = Atom S

x --> y = n $ k x (n y)  -- note lame syntax highlighting

-- Main>  ((p --> q) --> q)
-- Negation (Conjunction (Negation (Conjunction (Atom P) (Negation (Atom Q)))) (Negation (Atom Q)))
-- Main> subformulas ((p --> q) --> q)
-- [Negation (Conjunction (Negation (Conjunction (Atom P) (Negation (Atom Q)))) (Negation (Atom Q))),
--     Conjunction (Negation (Conjunction (Atom P) (Negation (Atom Q)))) (Negation (Atom Q)),
--     Negation (Conjunction (Atom P) (Negation (Atom Q))),
--     Conjunction (Atom P) (Negation (Atom Q)),Atom P,
--     Negation (Atom Q),Atom Q,Negation (Atom Q),Atom Q]

Позволяет создавать булевы атомы !:

t = Atom True
f = Atom False

-- Main> t --> f
-- Main> subformulas ( t --> f)
-- [Negation (Conjunction (Atom True) (Negation (Atom False))),
--           Conjunction (Atom True) (Negation (Atom False)),      
--            Atom True,Negation (Atom False),Atom False]

Почему бы непростая функция оценки?

 eval :: Formula Bool -> Bool
 eval (Atom p) = p
 eval (Negation p) = not (eval p)
 eval (Conjunction p q) = eval p && eval q

несколько случайных результатов:

 -- Main> eval (t --> f )
 -- False
 -- Main> map eval $ subformulas (t --> f)
 -- [False,True,True,True,False]

Добавлено позже: обратите внимание, что Formula - это Functor с очевидным примером, который может быть выведенGHC, если вы добавите Functor к производному предложению и языковой прагме {-#LANGUAGE DeriveFunctor#-}.Тогда вы можете использовать любую функцию f :: a -> Bool в качестве присваивания значений истинности:

-- *Main> let f p = p == P || p == R
-- *Main>  fmap f (p --> q)
-- Negation (Conjunction (Atom True) (Negation (Atom False)))
-- *Main> eval it
-- False
-- *Main>  fmap f ((p --> q) --> r)
-- Negation (Conjunction (Negation (Conjunction (Atom True) (Negation (Atom False)))) (Negation (Atom True)))
-- *Main> eval it
-- True
1 голос
/ 28 апреля 2011

Проблема с вашим кодом в том, что в formulaToSubFormula _ = Atom выходные данные создаются с помощью конструктора Atom, поэтому он всегда имеет тип Atom, тогда как сигнатура типа объявляет его любым типом с * 1004. * пример. Один из вариантов - добавить функцию в класс SubFormula:

class SubFormula a where
  atom :: a

instance SubFormula Atom where
  atom = Atom

formulaToSubFormula :: (Formula a, SubFormula b) => a -> b
formulaToSubFormula _ = atom

Конечно, если у вас будет только один экземпляр подтипа, вы можете полностью отказаться от класса:

formulaToSubFormula2 :: Formula a => a -> Atom

Также обратите внимание, что

data (Formula a) => Negation a = Negation a

, вероятно, не делает то, что вы хотите. Предполагается, что только типы Formula a могут быть отменены и всегда будут иметь доступный контекст Formula, но вместо этого это означает, что каждый раз, когда вы используете Negation a, вам нужно будет предоставить контекст Formula a, даже если это не используется. Вы можете получить желаемый результат, написав его с синтаксисом GADT :

data Negation a where
  Negation :: Formula a => a -> Negation a
0 голосов
/ 08 мая 2011

Единственный способ представить ограничения вложенности в типах данных - это какая-то система правил с помощью классов типов, таких как:

data Formula t val = Formula val deriving Show

-- formulae of type t allow negation of values of type a

class Negatable t a
instance Negatable Fancy a
instance Negatable Normal a
instance Negatable NNF Atom
instance Negatable CNF Atom
instance Negatable DNF Atom

class Conjunctable t a
instance Conjunctable Fancy a
instance Conjunctable Normal a
instance Conjunctable NNF a
instance Conjunctable CNF a
instance Conjunctable DNF Atom
instance Conjunctable DNF (Negation a)
instance Conjunctable DNF (Conjunction a b)

---

negate :: (Negatable t a) => Formula t a -> Formula t (Negation a)
negate (Formula x) = Formula $ Negation x

conjunct :: (Conjunctable t a, Conjunctable t b)
         => Formula t a -> Formula t b -> Formula t (Conjunction a b)
conjunct (Formula x) (Formula y) = Formula $ Conjunction x y

Статьи, которые вы упомянули, особенно Типы данных в виде корзины , были действительно полезными.

...