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

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

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 всегда реализуется для результата приложения семейства типов?

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

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


typeclass haskell type-level-computation type-families sbv
person jmite    schedule 04.07.2019    source источник
comment
Я не знаю многих деталей этой части Haskell, но не могли бы вы просто создать два экземпляра: instance SymVal a => SymVal (Vec a Z) и instance SymVal (Vec a n) => SymVal (Vec a (S n))?   -  person bradrn    schedule 04.07.2019

Ответы (2)


arrow_upward
4
arrow_downward

Я не знаю точного контекста, в котором вам требуются эти 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 ...
person Sam Derbyshire    schedule 04.07.2019
comment
Это круто! Что такое Dict? Это встроенная функция для явного обхода экземпляров класса типов? - person jmite; 04.07.2019
comment
@jmite Это история: data Dict con = con => Dict. - person HTNW; 04.07.2019
comment
Разве вы не можете сказать type family Pred (n :: Nat) :: Nat where Pred (S n) = n, а затем избавиться от всех этих случаев? deduceSymVal SZ Dict = Dict; deduceSymVal (SS m) Dict = case deduceSymVal @a @(Pred n) m of Dict -> Dict. Это не универсальное решение, как cases или шаблоны приложений типа (хотя спасибо за шаблон, я украду его), но в этом случае оно работает. - person HTNW; 04.07.2019
comment
Использование одиночного Nat в качестве динамического свидетеля было именно тем, что мне было нужно. Спасибо! - person jmite; 05.07.2019

arrow_upward
5
arrow_downward

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

person Daniel Wagner    schedule 04.07.2019