Ослабление ограничения RecAll винила через привязку
В виниловой библиотеке есть RecAll семейство типов, которое позволяет нам задавать вопрос о том, что частично примененное ограничение верно для каждого типа в списке уровня типа. Например, мы можем написать это:
myShowFunc :: RecAll f rs Show => Rec f rs -> String
И это все прекрасно. Теперь, если у нас есть ограничение RecAll f rs c где c неизвестно, и мы знаем c x влечет за собой d x (заимствовать язык из пакета контрактов Экметта), как мы можем получить RecAll f rs d?
Причина, по которой я спрашиваю, заключается в том, что я работаю с записями в некоторых функциях, которые требуют выполнения нескольких ограничений класса типов. Для этого я использую :&: комбинатор из модуля Control.Constraints.Combine в существующем пакете. (Примечание: пакет не будет собран, если у вас установлены другие компоненты, потому что это зависит от супер-старой версии contravariant, Вы можете просто скопировать один модуль, который я упомянул.) С этим я могу получить некоторые действительно красивые ограничения при минимизации таблички типов. Например:
RecAll f rs (TypeableKey :&: FromJSON :&: TypeableVal) => Rec f rs -> Value
Но внутри тела этой функции я вызываю другую функцию, которая требует более слабого ограничения. Это может выглядеть так:
RecAll f rs (TypeableKey :&: TypeableVal) => Rec f rs -> Value
GHC не видит, что второе утверждение следует из первого. Я предположил, что это будет так. Чего я не вижу, так это как доказать это, чтобы утвердить это и помочь GHC. Пока у меня есть это:
import Data.Constraint
weakenAnd1 :: ((a :&: b) c) :- a c
weakenAnd1 = Sub Dict -- not the Dict from vinyl. ekmett's Dict.
weakenAnd2 :: ((a :&: b) c) :- b c
weakenAnd2 = Sub Dict
Они работают нормально. Но вот где я застрял:
-- The two Proxy args are to stop GHC from complaining about AmbiguousTypes
weakenRecAll :: Proxy f -> Proxy rs -> (a c :- b c) -> (RecAll f rs a :- RecAll f rs b)
weakenRecAll _ _ (Sub Dict) = Sub Dict
Это не компилируется. Кто-нибудь знает способ получить эффект, который я ищу. Вот ошибки, если они полезны. Также у меня есть Dict как квалифицированный импорт в моем реальном коде, поэтому он упоминает Constraint.Dict:
Table.hs:76:23:
Could not deduce (a c) arising from a pattern
Relevant bindings include
weakenRecAll :: Proxy f
-> Proxy rs -> (a c :- b c) -> RecAll f rs a :- RecAll f rs b
(bound at Table.hs:76:1)
In the pattern: Constraint.Dict
In the pattern: Sub Constraint.Dict
In an equation for ‘weakenRecAll’:
weakenRecAll _ _ (Sub Constraint.Dict) = Sub Constraint.Dict
Table.hs:76:46:
Could not deduce (RecAll f rs b)
arising from a use of ‘Constraint.Dict’
from the context (b c)
bound by a pattern with constructor
Constraint.Dict :: forall (a :: Constraint).
(a) =>
Constraint.Dict a,
in an equation for ‘weakenRecAll’
at Table.hs:76:23-37
or from (RecAll f rs a)
bound by a type expected by the context:
(RecAll f rs a) => Constraint.Dict (RecAll f rs b)
at Table.hs:76:42-60
Relevant bindings include
weakenRecAll :: Proxy f
-> Proxy rs -> (a c :- b c) -> RecAll f rs a :- RecAll f rs b
(bound at Table.hs:76:1)
In the first argument of ‘Sub’, namely ‘Constraint.Dict’
In the expression: Sub Constraint.Dict
In an equation for ‘weakenRecAll’:
weakenRecAll _ _ (Sub Constraint.Dict) = Sub Constraint.Dict
1 ответ
Давайте начнем с рассмотрения того, как Dict а также (:-) предназначены для использования.
ordToEq :: Dict (Ord a) -> Dict (Eq a)
ordToEq Dict = Dict
Сопоставление с образцом по значению Dict типа Dict (Ord a) приносит ограничение Ord a в область, из которой Eq a можно вывести (потому что Eq это суперкласс Ord), так Dict :: Dict (Eq a) хорошо напечатан.
ordEntailsEq :: Ord a :- Eq a
ordEntailsEq = Sub Dict
Так же, Sub вводит входное ограничение в область действия аргумента, позволяя Dict :: Dict (Eq a) быть хорошо напечатанным.
Однако, в то время как сопоставление с образцом на Dict вводит ограничение в область видимости Sub Dict не вводит в сферу применения какое-то новое правило преобразования ограничений. На самом деле, если входное ограничение уже находится в области видимости, вы не можете сопоставить шаблон с Sub Dict совсем.
-- Could not deduce (Ord a) arising from a pattern
constZero :: Ord a :- Eq a -> Int
constZero (Sub Dict) = 0
-- okay
constZero' :: Ord a => Ord a :- Eq a -> Int
constZero' (Sub Dict) = 0
Так что это объясняет вашу первую ошибку типа, "Could not deduce (a c) arising from a pattern": вы пытались сопоставить с шаблоном Sub Dict, но входное ограничение a c не было уже в объеме.
Другая ошибка типа, конечно, говорит о том, что ограничения, которые вам удалось получить в области действия, были недостаточными для удовлетворения RecAll f rs b ограничение. Итак, какие части нужны, а какие отсутствуют? Давайте посмотрим на определение RecAll,
type family RecAll f rs c :: Constraint where
RecAll f [] c = ()
RecAll f (r : rs) c = (c (f r), RecAll f rs c)
Ага! RecAll это семейство типов, столь же недооцененное, как оно есть, с полностью абстрактным rs, ограничение RecAll f rs c является черным ящиком, который не может быть удовлетворен ни одним набором меньших частей. Как только мы специализируемся rs в [] или же (r : rs), становится ясно, какие части нам нужны:
recAllNil :: Dict (RecAll f '[] c)
recAllNil = Dict
recAllCons :: p rs
-> Dict (c (f r))
-> Dict (RecAll f rs c)
-> Dict (RecAll f (r ': rs) c)
recAllCons _ Dict Dict = Dict
я использую p rs вместо Proxy rs потому что это более гибкий: если бы у меня был Rec f rsНапример, я мог бы использовать это в качестве моего прокси с p ~ Rec f,
Далее, давайте реализуем версию выше с (:-) вместо Dict:
weakenNil :: RecAll f '[] c1 :- RecAll f '[] c2
weakenNil = Sub Dict
weakenCons :: p rs
-> c1 (f r) :- c2 (f r)
-> RecAll f rs c1 :- RecAll f rs c2
-> RecAll f (r ': rs) c1 :- RecAll f (r ': rs) c2
weakenCons _ entailsF entailsR = Sub $ case (entailsF, entailsR) of
(Sub Dict, Sub Dict) -> Dict
Sub приносит свои входные ограничения RecAll f (r ': rs) c1 в область действия на время его аргумента, который мы организовали, чтобы включить остальную часть тела функции. Уравнение для семейства типов RecAll f (r ': rs) c1 расширяется до (c1 (f r), RecAll f rs c1)которые, таким образом, оба также включены в сферу применения. Тот факт, что они находятся в области видимости, позволяет нам сопоставить по образцу Sub Dictи эти два Dict ввести их соответствующие ограничения в сферу: c2 (f r), а также RecAll f rs c2, Эти два являются именно тем, что является целевым ограничением RecAll f (r ': rs) c2 расширяется, поэтому наш Dict правая сторона хорошо напечатана.
Для завершения нашей реализации weakenAllRecнам нужно будет сопоставить шаблон по rs чтобы определить, следует ли делегировать работу weakenNil или же weakenCons, Но с тех пор rs находится на уровне типа, мы не можем напрямую сопоставить его с шаблоном. В статье о хасохизме объясняется, как сопоставить с образцом на уровне типа Natнам нужно создать тип данных-обёртки Natty, Путь который Natty работает то, что каждый из его конструкторов индексируется соответствующим Nat конструктор, поэтому, когда мы сопоставляем шаблон на Natty конструктор на уровне значения, соответствующий конструктор также подразумевается на уровне типа. Мы могли бы определить такую оболочку для списков уровня типа, таких как rs, но так получилось, что Rec f rs уже есть конструкторы, соответствующие [] а также (:)и абоненты weakenAllRec скорее всего, есть один валяется в любом случае.
weakenRecAll :: Rec f rs
-> (forall a. c1 a :- c2 a)
-> RecAll f rs c1 :- RecAll f rs c2
weakenRecAll RNil entails = weakenNil
weakenRecAll (fx :& rs) entails = weakenCons rs entails
$ weakenRecAll rs entails
Обратите внимание, что тип entails должно быть forall a. c1 a :- c2 aне просто c1 a :- c2 aпотому что мы не хотим утверждать, что weakenRecAll будет работать для любого a выбора вызывающего абонента, но мы хотим, чтобы вызывающий абонент доказал, что c1 a влечет за собой c2 a для каждого a,