Утверждение, что класс типов верен для всех результатов применения семейства типов

У меня есть семейство типов, определенное следующим образом:

type family Vec a (n :: Nat) where
  Vec a Z = a
  Vec a (S n) = (a, Vec a n)

Я хотел бы заявить, что результат применения этого семейства типов всегда соответствует ограничению класса SymVal из пакета SBV:

forall a . (SymVal a) => SymVal (Vec a n)

Есть SymVal экземпляры a,bтак что всякий раз, когда SymVal a держит, то SymVal (Vec a n) следует держать, для любого значения n, Как я могу убедиться, что GHC видит это SymVal всегда реализуется для результата приложения семейства типов?

Однако я не знаю, как это выразить. Я пишу экземпляр? Производное предложение? Я не создаю новый тип, просто сопоставляю числа с существующими.

Или я на неправильном пути? Должен ли я использовать семейство данных или функциональные зависимости?

Источник

2 ответа

Решение

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

foo :: forall (a :: Type) (n :: Nat). SymVal (Vec a n) => ...

когда foo называется с конкретным n, решатель ограничений сократит приложение семейства типов и будет использовать экземпляры

instance ( SymVal p, SymVal q ) => SymVal (p,q)

В конце этого процесса решатель ограничений будет нуждаться в экземпляре для SymVal a, Таким образом, вы сможете позвонить foo:

  • если вы укажете заданное значение для n, позволяя приложениям семейства типов полностью сокращать и использовать тип a который имеет экземпляр для SymVal:
bar :: forall (a :: Type). SymVal a => ...
bar = ... foo @a @(S (S (S Z))) ...

baz :: ...
baz = ... foo @Float @(S Z) ... -- Float has a SymVal instance
  • отложить поиск экземпляра, предоставив тот же контекст:
quux :: forall (a :: Type) (n :: Nat). SymVal (Vec a n) => ...
quux = ... foo @a @n ...

GHC не может автоматически вывести SymVal (Vec a n) из SymVal aпотому что без дальнейшего контекста он не может уменьшить приложение семейства типов и, следовательно, не знает, какой экземпляр выбрать. Если вы хотите, чтобы GHC мог выполнить этот вывод, вам нужно будет пройти n явно в качестве аргумента. Это можно эмулировать с помощью синглетонов:

deduceSymVal :: forall (a :: Type) (n :: Nat). Sing n -> Dict (SymVal a) -> Dict (SymVal (Vec a n))
deduceSymVal sz@SZ Dict =
  case sz of
    ( _ :: Sing Z )
      -> Dict
deduceSymVal ( ss@(SS sm) ) Dict
  = case ss of
      ( _ :: Sing (S m) ) ->
        case deduceSymVal @a @m sm Dict of
          Dict -> Dict

(Обратите внимание, что эти отвратительные операторы case будут исключены при использовании приложений типов в шаблонах, mais c'est la vie.)

Затем вы можете использовать эту функцию, чтобы GHC мог вывести SymVal (Vec a n) ограничение от SymVal a ограничение, если вы можете предоставить синглтон для n (что составляет прохождение n явно, а не параметрически над ним):

flob :: forall (a :: Type) (n :: Nat). (SymVal a, SingI n) => ...
flob = case deduceSymVal @a (sing @n) Dict of
  Dict -- matching on 'Dict' provides a `SymVal (Vec a n)` instance
    -> ... foo @a @n ...
Источник

Не может быть сделано Вы просто должны поставить ограничение везде. Это настоящий облом.

Источник
Другие вопросы по тегам