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

Вот пример:

 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
  

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

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

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

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

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

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

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

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

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

В Haskell есть способы добиться расширяемого синтаксиса, например, стиля «Окончательно без тегов» [1] или двухуровневых типов Sheard и Pasalic [2].

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

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

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

Проблема с вашим кодом заключается в том, что в formulaToSubFormula _ = Atom вывод создается с помощью Atom конструктора, поэтому он всегда имеет тип Atom , тогда как сигнатура типа объявляет его любым типом с SubFormula экземпляром. Одним из вариантов является добавление функции в 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
  

Здесь может происходить много чего, я сомневаюсь, что что-либо связано с введением классов типов. (Самая необычная вещь, которая может появиться в ближайшее время, — это GADT.) Следующее очень простое; оно просто предназначено для того, чтобы заставить вас более четко сказать, что вы хотите….

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

 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 amp;amp; eval q
  

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

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

Добавлено позже: обратите внимание, что Formula это Functor с очевидным экземпляром, который может быть выведен GHC, если вы добавите функтор к производящему предложению и языковой прагме {-#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
  

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

 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
  

Упомянутые вами статьи, особенно типы данных a la cart, были действительно полезны.