Структура значений ограниченных моноидных типов

У меня есть тип данных, который является экземпляром Monoid, поэтому я могу получить красивую композицию значений:

data R a = R String (Maybe (String → a))

instance Monoid (R a) where
  mempty = R "" Nothing
  R s f `mappend` R t g = R (s ++ t) (case g of Just _ → g; Nothing → f)

Далее, я не хочу комбинировать все значения R a друг с другом, это не имеет смысла в моем домене. Поэтому я представляю phantom тип t:

{-# LANGUAGE DataKinds, KindSignatures #-}

data K = T1 | T2
data R (t ∷ K) a = R String (Maybe (String → a))

instance Monoid (R t a) where …

Итак, у меня есть "ограниченные" значения:

v1 ∷ R T1 Int
v2 ∷ R T2 Int
-- v1 <> v2 => type error

и "неограниченный":

v ∷ R t Int
-- v <> v1 => ok
-- v <> v2 => ok

Но теперь у меня проблема. Когда дело доходит до v30, например:

  • У меня было бы огромное объявление типа data​​strike > (data K = T1 | … | T30). Я мог бы решить, используя naturals типа уровня, чтобы получить бесконечный источник типов phantom (лечение хуже, чем болезнь, не так ли?).
  • Я должен помнить, какой тип phantom для какого значения использовать при написании сигнатур типов в зависимом коде (это действительно раздражает)

Существует ли более простой подход к ограничению состава?

Ответы

Ответ 1

Поиск ограничения.

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

Вот идея:

class ConstrainedMonoid m where
  type Compatible m (t1 :: k) (t2 :: k) :: Constraint
  type TAppend m (t1 :: k) (t2 :: k) :: k
  type TZero m :: k

  memptyC :: m (TZero m)
  mappendC :: (Compatible m t t') => m t -> m t' -> m (TAppend m t t')

Хорошо, есть тривиальный экземпляр, который на самом деле не добавляет ничего нового (я заменил аргументы типа R):

data K = T0 | T1 | T2 | T3 | T4
data R a (t :: K) = R String (Maybe (String -> a))

instance ConstrainedMonoid (R a) where
  type Compatible (R a) T1 T1 = ()
  type Compatible (R a) T2 T2 = ()
  type Compatible (R a) T3 T3 = ()
  type Compatible (R a) T4 T4 = ()
  type Compatible (R a) T0 y = ()
  type Compatible (R a) x T0 = ()

  type TAppend (R a) T0 y = y 
  type TAppend (R a) x T0 = x
  type TAppend (R a) T1 T1 = T1
  type TAppend (R a) T2 T2 = T2
  type TAppend (R a) T3 T3 = T3
  type TAppend (R a) T4 T4 = T4
  type TZero (R a) = T0

  memptyC = R "" Nothing
  R s f `mappendC` R t g = R (s ++ t) (g `mplus` f)

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

Однако он не закрыт. Это больше похоже на набор различных моноидов, индексированных K. Если этого вы хотите, этого должно быть достаточно.

Если вы хотите больше

Посмотрим на другой вариант:

data B (t :: K) = B String deriving Show

instance ConstrainedMonoid B where
  type Compatible B T1 T1 = ()
  type Compatible B T2 T2 = ()
  type Compatible B T3 T3 = ()
  type Compatible B T4 T4 = ()

  type TAppend B x y = T1
  type TZero B = T3 

  memptyC = B ""
  (B x) `mappendC` (B y) = B (x ++ y)

Это может быть случай, который имеет смысл в вашем домене, однако он больше не является моноидом. И если вы попытаетесь сделать один из них, он будет таким же, как и выше, только с разными TZero. Я на самом деле просто размышляю здесь, но моя интуиция говорит мне, что единственными действительными экземплярами моноидов являются именно те, что для R a; только с разными значениями единиц.

В противном случае вы получите что-то не обязательно ассоциативное (и, вероятно, с терминальным объектом), которое не закрыто по композиции. И если вы хотите ограничить состав равным K s, вы потеряете значение единицы.

Лучший способ (IMHO)

Вот как я на самом деле решил свою проблему (я даже не думал о моноидах тогда, так как они так и не поняли). Решение существенно удаляет все, кроме Compatible "производителя ограничений", который остается как предикат двух типов:

type family Matching (t1 :: K) (t2 :: K) :: Constraint
type instance Matching T1 T1 = ()
type instance Matching T2 T1 = ()
type instance Matching T1 T2 = ()
type instance Matching T4 T4 = ()

используется как

foo :: (Matching a b) => B a -> B b -> B Int

Это дает вам полный контроль над вашим определением совместимости и какой состав (не обязательно моноидальный) вы хотите, и он более общий. Он также может быть расширен до бесконечных видов:

-- pseudo code, but you get what I mean
type instance NatMatching m n = (IsEven m, m > n)

Отвечая на две последние точки:

  • Да, вам нужно определить достаточно много типов в вашем роде. Но я думаю, что они все равно должны объяснять себя. Вы также можете разбить их на группы или определить рекурсивный тип.

  • В основном вы должны напомнить значение типа индекса в двух местах: определение ограничения и, возможно, для методов factory (mkB1 :: String -> B T1). Но я думаю, что это не должно быть проблемой, если типы названы хорошо. (Это может быть очень избыточным, хотя - я еще не нашел способа избежать этого. Возможно, это сработает.)

Может ли это быть проще?

Мне бы хотелось написать следующее:

type family Matching (t1 :: K) (t2 :: K) :: Constraint
type instance Matching T1 y = ()
type instance Matching x T1 = ()
type instance Matching x y = (x ~ y)

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

EDIT: В настоящее время мы имеем закрытые типы семейств, которые делают именно это.