Как написать forall ограничения, например, для некоторых семей типа F и G:Forall ограничений
forall x y. G (F x y) ~ (x, y)
это возможно с помощью Edward A. Kmett Constraints пакета? И если бы это был небольшой пример? Я полагаю, мне нужно использовать Forall.
Да, это возможно, используя constraints. Будьте осторожны, однако! Равноправие, которое вы утверждаете, вряд ли будет иметь достаточную общность для constraints, если типы семейств нетривиальны. Рассмотрим, в частности, являются ли семьи типа успешно уменьшить, когда x и y застряли семьи типа
type family X where {}
type family Y where {}
Кроме того, я вижу, что ваш частности желаемое ограничение не имеет свободных переменных вообще. Надеюсь, это просто пример. фактическое закрытое ограничение, подобное этому, вряд ли будет полезно.
Фундаментальная семейного типа в Data.Constraint.Forall является Forall. Этот конкретный пример может быть обработан немного более удобно с использованием ForallT, но наиболее важно понять, как использовать Forall.
В общем, Forall p означает forall x . p x. Это не звучит очень общее, но на самом деле это происходит, если вы наращиваете свой p шаг за шагом. Вы ищете
forall x y. G (F x y) ~ (x, y)
Начинайте с определения класса, в котором вы указываете отношения, которые ищете.
class G (F x y) ~ (x, y) => C x y
instance G (F x y) ~ (x, y) => C x y
Теперь вы можете идти шаг за шагом, определяя
class Forall (C x) => D x
instance Forall (C x) => D x
(который вы можете прочитать, как D x = forall y . C x y)
, а затем с помощью Forall D (т.е. forall x . D x), чтобы выразить свое ограничение. Вам нужно будет использовать inst, чтобы получить Dict (D x) и снова, чтобы получить Dict (C x y).
Вы ищете, что это ограничение более крупного типа или вы хотите, чтобы на самом деле это было равенство? Это может помочь предоставить больше информации о том, что вы пытаетесь сделать. –
Если вы ищете значение для представления самого равенства, будет 'равенствоVal :: G (F x y): ~: (x, y); равенствоVal = ... Refl ... 'с': ~: 'из' Data.Type.Equality' работает? Если, с другой стороны, это ограничение на более крупный тип, не можете ли вы просто иметь G (F x y) ~ (x, y) => ... '? Я полагаю, что 'Forall' из пакета ограничений имеет универсальное квантификацию по ограничениям (например,' (Forall p, pa) => a'), где 'p' может быть таким ограничением, как' Num', что, похоже, не является быть тем, что вы ищете (если я правильно понимаю). –