Списки типов с ограничениями

Question

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

Мой базовый код:

data Foo z q = Foo1 (z q)
             | Foo2 (z q)

class Qux q -- where ...
class Baz z -- where ...

class Bar a where             -- a has kind *->*
  type BCtx a q :: Constraint -- using ConstraintKinds to allow constraints on the concrete type
  f :: (BCtx a q) => a q -> a q -> a q
  g :: (BCtx a q, BCtx a q') => a q -> a q'

instance (Baz z) => Bar (Foo z) where
  type BCtx (Foo z) q = (Num (z q), Qux q) -- for example
  f (Foo1 x) (Foo1 y) = Foo1 $ x+y -- these functions need access to the type q to do arithmetic mod q
  f (Foo1 x) (Foo2 y) = Foo2 $ x-y
  -- ...

Вы можете думать о qвыше, представляющий основные полномочия. Я также хотел бы представлять составные числа, используя список типов qis. Я представляю что-то вроде:

data QList qi qs = QCons qi qs
                 | QNil

с данными

data FList c q = FNil 
               | FCons (c (Head q)) (FList c (Tail q))

где (Head q) должен соответствовать qi а также (Tail q) должен соответствовать qs, Обратите внимание, что q параметр для FList НЕ (обязательно) (Qux q), это список (Qux qi), (Я не хочу более подробно рассказывать об этом списке, так как это одна из проблем дизайна, которую я представляю). Я хотел бы работать "по модулю" на FList:

instance (Bar c) => Bar (FList c) where
   type BCtx (FList c) q = () -- Anything I put here is not enough
   f (FCons x xs) (FCons y ys) = FCons (f x y) (f xs ys)
   -- the left call to `f` calls a concrete instance, the right call to `f` is a recursive call on the rest of the list
   -- ...

Компилирование этих фрагментов кодов вместе в GHC приводит к (по модулю транскрипции, абстракции и ошибкам ввода):

Could not deduce (BCtx c (Head q), BCtx c (Tail q))

а потом

Could not deduce (BCtx c (Head (Tail q)), BCtx c (Tail (Tail q)))

и т.п.

Я понимаю, почему я получаю эту ошибку, но не как ее исправить.

Конкретно я ожидаю FList c q типа где c~Foo z а также q~QCons q1 (QCons q2 QNil)и, конечно же, мой список будет удовлетворять всем ограничениям BCtx на каждом уровне.

Я не уверен, что исправление этих конкретных ошибок приведет к компиляции кода, но это только начало. Весь класс Bar в основном фиксированный (требуется тип Constraint, а экземпляры Bar должны иметь вид * -> *). Я не верю, что могу использовать экзистенциальные типы для создания списка универсальных объектов, потому что мне нужен доступ к qi параметр. Я готов изменить тип FList а также QList чтобы позволить мне работать по модулю над коллекцией баров.

Спасибо за ваше время!

Answer 1

Для обработки списков типов необходимо отличать пустые списки от непустых и обрабатывать их отдельно. Ошибки "Не удалось вывести" в вашем коде происходят из-за того, что ваш экземпляр принимает непустой список, хотя на самом деле список может быть или не быть пустым. Вот решение с использованием расширений TypeFamilies, TypeOperators, DataKinds, а также GADTs,

С DataKinds, списки типов предварительно определены. У них есть вид [*], но они будут использоваться в контексте, где вид * ожидается, поэтому оператор должен их привести:

data InjList (qs :: [*])

Используя списки типов, FList определяется как

data FList c q where
  FNil :: FList c (InjList '[])
  FCons :: c h -> FList c (InjList t) -> FList c (InjList (h ': t))

Он определяется как GADT, чтобы выразить, как можно только построить FListс над типом InjList q' для некоторого списка типов q', Например, термин FCons [True] FNil имеет тип FList [] (InjList (Bool ': '[])), С другой стороны, так как Bool не в форме InjList q', нет терминов (кроме ⊥) типа FList [] Bool, Путем сопоставления с образцом на FList, функция может проверить, что ей был передан не-аргумент, и дополнительно определить, был ли ей передан пустой список типов.

Экземпляр Bar за FLists должен обрабатывать ноль списков и списков минусов отдельно. Нулевой список имеет пустой контекст. У списка минусов есть компоненты для головы и хвоста списка. Это выражается сопоставлением с образцом в списке типов в связанном экземпляре типа BCtx, Функция f проверяет его аргумент, чтобы убедиться, что это не ⊥, и решить, является ли он пустым списком.

instance (Bar c) => Bar (FList c) where
  -- Empty context for '[]
  type BCtx (FList c) (InjList '[]) = ()
  -- Context includes components for head and tail of list
  type BCtx (FList c) (InjList (h ': t)) = (BCtx c h, BCtx (FList c) (InjList t))

  f FNil FNil = FNil
  f (FCons x xs) (FCons y ys) = FCons (f x y) (f xs ys)

Мы можем загрузить код в GHCi, чтобы убедиться, что он работает:

instance Bar [] where
  type BCtx [] q = Num q
  f xs ys = zipWith (+) xs ys

instance Show (FList c (InjList '[])) where
  show FNil = "FNil"

instance (Show (c h), Show (FList c (InjList t))) => Show (FList c (InjList (h ': t))) where
  show (FCons h t) = "FCons (" ++ show h ++ ") (" ++ show t ++ ")"

$ ghci

> :load Test
> f (FCons [1,2] FNil) (FCons [3,4] FNil)
FCons ([4,6]) (FNil)