Как создать класс рекурсивного типа, который ведет себя как другой класс рекурсивного типа, но имеет меньше экземпляров, чем родительский класс?
Вот пример:
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
Поэтому мне нужен инструмент для представления этой иерархии.
removeImplicationвы удаляете только самый внешний конструкторImplication.removeImplication (Negation (Implication x y))будет(Negation (Implication x y)). Простое решение состоит в том, чтобы просто иметь два типаFormulaи, скажем,NormalFormи функциюtoNormalForm, которая проходит через сложные формулы и рекурсивно преобразует Импликации в соответствующую NormalForm, не так ли? Я думаю, нам все еще нужно знать больше о том, куда вы идете с этим. - person applicative schedule 28.04.2011removeImplicationнужна только для того, чтобы показать, что я имею в виду. Дело в том, чтоNormalFormявляется подмножествомFormula, и поэтому я ищу способ разделить это подмножество между обоими типами. - person Till Theis schedule 28.04.2011stephen tetley. Определение типа данных, особенно рекурсивное, похоже на язык в миниатюре. Вы рассматриваете несколько маленьких языков и их взаимоотношения; почему эти отношения не должны быть выражены функциями между типами? ЕслиL1иL2являются типами, то типыL1 -> L2иL2 -> L1являются типами отношений между ними, грубо говоря. - person applicative schedule 29.04.2011data CNFElemиdata CNFвам нужно обернуть первый «конструктор». В его нынешнем виде каждый из них является уже определенным типом,AtomиCNFElemсоответственно, и не может быть конструктором типа, который вы определяете. Итак, вам нужныdata CNFElem = CNFAtom Atom | ...иdata CNF = CNFElt CNFElem. Это относится и к большинству определений типов ранее в запросе. - person applicative schedule 29.04.2011CNF-Formulaявляется допустимымFormula(хотя не каждыйFormulaявляется допустимымCNF-Formula). Поэтому я попытался визуализировать это «наследство» через систему типов. - person Till Theis schedule 29.04.2011isFormulaиisCNFFormulaкак предикатStrings, или же использоватьisCNFFormulaкак предикатFormulas. Он латентно отвергает представление обоих как типов, то есть как нечто, предполагаемое представлением его обитателей. Все B являются C предполагает, что существует общий тип, скажем, A, и мы можем утверждать или отрицать, что B является B и является C для A, или что B является базовым типом, а предикат C определяется по отношению к Это. - person applicative schedule 30.04.2011stephen tetleyстатье [Типы данных на выбор] (www.cs.nott.ac.uk/~wss/Publications/DataTypesALaCarte.pdf). Вот модуль, содержащий некоторые материалы hpaste.org/46175/data_types_a_la_carte. Я не могу вспомнить, где я нашел это. - person applicative schedule 30.04.2011Valсоответствует вашему типуAtom, егоAddиMulсоответствуют вашимDisjunctionиImplication(здесь нам нужно отрицание).(:+:)добавляет один ингредиент к другому. Итак, сначала у нас естьdata Val e = Val Int(обратите внимание на неиспользуемый параметр); затемdata Add e = Add e e, своего рода диагонализатор, тоже функтор. Вместе они дают намVal :+: Add, еще один функтор. Затем мы добавляемdata Mul e = Mul e eи можем рассматривать(Val :+: Add) :+: Mul, новый экземпляр Functor. - person applicative schedule 30.04.2011Exprпринимает фиксированную точку любого из них, таким образом, Expr (Val :+: Add), один тип, имеет суммы и суммы сумм и т. д. (ЛистьяInts из-за определенияVal)Expr ((Val :+: Add) :+: Mul)представляет суммы, произведения, суммы произведений и т. д. Наконец, класс многопараметрического типа(:<:)имеет вид отношения «подтип», но обратите внимание, что он связывает функторы в системе типов. Я не изучал его какое-то время; это сложно, но очень интересно и сравнительно легко читается. - person applicative schedule 30.04.2011type CNF = Expr (Conjunction :+: Disjunction :+: Atom :+: Negation), но это позволило бы произвольное вложениеConjunctionиDisjunctions, хотяDisjunctionне может содержатьConjunction(то же самое дляNegation). - person Till Theis schedule 02.05.2011isCNFFormula, то я мог бы в первую очередь использовать простой рекурсивный тип данных, поскольку я не мог бы определить структуруFormulaпо его типу (в этом весь смысл, не так ли?) . Что мне не хватает? И кстати: спасибо за вашу помощь - я уже кое-что узнал из статьи и поэкспериментировал с описанной в ней концепцией. - person Till Theis schedule 02.05.2011