Могу ли я запретить один конкретный конструктор данных внутри другого, в то время как оба дают один и тот же тип?

Я хотел бы создать тип T в Haskell, который позволяет

[Leaf 1, Rooted (Leaf 2), Branch (Leaf 3) (Branch (Leaf 4) (Leaf 5))]

но нет

[Leaf 1, Rooted (Leaf 2), Branch (Rooted (Leaf 3)) (Branch (Leaf 4) (Leaf 5))]

т.е. все конструкторы T, кроме Rooted, могут появляться в первом или втором аргументах Branch (полный код имеет еще несколько конструкторов).

Я пробовал такие вещи, как

{-# LANGUAGE GADTs #-}
data T (x::Bool) where
  Leaf :: Int -> T True
  Rooted :: T True -> T False
  Branch :: T True -> T True -> T True

что гарантирует, что мы не можем сделать Branch (Rooted …) …, но также означает, что мы не можем сделать [Rooted …, One …], так как это будет список различных типов ([T True, T False]).

Я изучил DataKinds, надеясь, что смогу сделать

{-# LANGUAGE GADTs, DataKinds, KindSignatures #-}
data T where
  Leaf :: Int -> T
  Rooted :: T -> T
  Branch :: UnRooted a => a -> a -> T
class UnRooted a
instance UnRooted Leaf
instance UnRooted Branch

но тогда ghc (7.10.3) дает Data constructor ‘Leaf’ comes from an un-promotable type ‘T’.

Есть ли способ сделать это в Haskell?


types haskell gadt data-kinds
person unhammer    schedule 27.11.2017    source источник
comment
Если вы хотите поместить их в один и тот же (однородный) список, вы должны указать один и тот же тип для root и non-root. Но если они имеют один и тот же тип, вы можете заменить один на другой в поддеревьях. Это невозможно, как говорится. Возможно, было бы нормально обернуть вашу первую попытку в экзистенциальную обертку, чтобы удалить логическое значение в типе? Или используя тип суммы? Или без GADT сделать root собственным типом (и по-прежнему использовать сумму или оболочку)?   -  person chi    schedule 27.11.2017
comment
Можешь объяснить, зачем тебе это? То есть, для чего для должен быть конструктор Rooted?   -  person MathematicalOrchid    schedule 27.11.2017
comment
Это сопоставление с образцом. Я хотел бы иметь возможность писать выражения в виде простых списков с довольно компактным синтаксисом. Branch на самом деле представляет собой набор операторов для объединения двух выражений. Rooted - это (набор) оберток, чтобы сказать, что такие вещи, как этот шаблон, не обязательно должны появляться рядом с предыдущим/следующим. Но кажется сложным определить такой тип простым и понятным способом, поэтому я думаю, что мне следует найти другой подход.   -  person unhammer    schedule 27.11.2017

Ответы (1)


arrow_upward
3
arrow_downward

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

{-# LANGUAGE GADTs, DataKinds, KindSignatures, RankNTypes #-}
data T (x::Bool) where
  Leaf :: Int -> T True
  Rooted :: T True -> T False
  Branch :: T True -> T True -> T True

data TWrap = forall (x :: Bool). TWrap (T x)

[TWrap $ Leaf 1, TWrap $ Rooted (Leaf 2), TWrap $ Branch (Leaf 3) (Branch (Leaf 4) (Leaf 5))]

Однако, если нам все равно придется обернуть тип, вероятно, лучше просто выбрать более простое решение разделения типа:

data T = Leaf Int | Branch T T
data TWrap = Unrooted T | Rooted T

[Unrooted $ Leaf 1, Rooted $ Leaf 2, Unrooted $ Branch (Leaf 3) (Branch (Leaf 4) (Leaf 5))]

Вы запрашиваете в основном зависимые типы, которых нет в Haskell (пока).

person Hjulle    schedule 27.11.2017
comment
Пожалуйста, поправьте меня, если мой комментарий о зависимых типах был неточным. В Haskell есть некоторая поддержка зависимых типов (например, через GADT), но я считаю, что для удовлетворения описания, данного в вопросе, потребуется дополнительная поддержка. - person Hjulle; 27.11.2017