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

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

6 голосов
/ 04 июля 2019

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

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 ]

5 голосов
/ 04 июля 2019

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

4 голосов
/ 04 июля 2019

Я не знаю точного контекста, в котором вам требуются эти 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 ...
...