Не знаете, что такое GADT и распространяемые ограничения.

Об этом можно подумать OutsideIn (X) ... с местными допущениями. Дело не в неопределенности или ленивых оценках. Сопоставление с образцом в конструкторе GADT находится снаружи, правая часть уравнения находится внутри. Ограничения из конструктора доступны только локально - только внутри.

baz (MkGADTBag x) (Just y) = x == y

Имеет явный конструктор данных MkGADTBag снаружи, предоставляющий Eq a. x == y вызывает запрос Eq a локально / внутри, который выводится из сопоставления с образцом. OTOH

baz2           x        y  = unGADTBag x == fromJust y

Не имеет явного конструктора данных снаружи, поэтому контекст не предоставляется. unGADTBag имеет Eq a, но он глубже внутри l.h. аргумент ==; вывод типа не заглядывает глубже. Это просто не так. Тогда в действующем определении для unGADTBag

unGADTBag (MkGADTBag x) = x

есть Eq a, доступный извне, но он не может уйти из RHS в среду типов на сайте использования для unGADTBag. Это просто не так. Грустный!

Лучшее, что я могу найти для объяснения, - это ближе к концу статьи OutsideIn, раздел 9.7 Обоснован ли акцент на основных типах? (риторический вопрос, но мой ответ хотел бы я: конечно, мы должны подчеркнуть основные типы; вывод типов может стать более принципиальным при некоторых обстоятельствах.) В последнем разделе рассматривается этот пример.

    data R a where
      RInt :: Int -> R Int
      RBool :: Bool -> R Bool
      RChar :: Char -> R Char

    flop1 (RInt x) = x

есть третий тип, который, возможно, более желателен [для flop1], и это тип R Int -> Int.

Определение flop1 имеет ту же форму, что и unGADTBag, с ограничением a равным Int.

    flop2 (RInt x) = x
    flop2 (RBool x) = x

К сожалению, обычные полиморфные типы слишком слабы, чтобы выразить это ограничение [что a должно быть только Int или Bool], и мы можем получить только Ɐa.R a -> a для flop2, что не исключает применения flop2 к значениям типа R Char.

Итак, на этом этапе работа, похоже, перестает пытаться уточнить основные типы:

В заключение, отказ от некоторых естественных основных типов в пользу более специализированных типов, которые устраняют больше ошибок сопоставления с образцом во время выполнения, является привлекательным, но не совсем работает, если мы не рассматриваем более выразительный синтаксис типов. Более того, далеко не очевидно, как указать эти типы в декларативной спецификации высокого уровня.

привлекательно. Это просто не так.

Я вижу, что общее решение сложно / невозможно. Но для случаев использования ограниченных пакетов / списков / наборов спецификация:

• Все конструкторы данных имеют одинаковые ограничения на параметры типа данных.
• Все конструкторы выдают один и тот же тип (... -> T a, ... -> T [a], ... -> T Int и т. Д.).
• Типы данных с одним конструктором тривиально этому удовлетворяют.

Чтобы удовлетворить первый пункт, для типа Set, использующего двоичное сбалансированное дерево, должно быть неочевидное определение конструктора Nil:

data OrdSet a  where
  SNode :: Ord a => OrdSet a -> a -> OrdSet a -> OrdSet a
  SNil  :: Ord a => OrdSet a                     -- seemingly redundant Ord constraint

Даже в этом случае повторение ограничения для каждого узла и каждого терминала кажется расточительным: это одно и то же ограничение на всем пути вниз (в отличие от GADT для абстрактных синтаксических деревьев EDSL); предположительно каждый узел содержит копию точно такого же словаря.

Лучший способ обеспечить одинаковые ограничения для каждого конструктора - это просто добавить ограничение к типу данных:

data Ord a => OrdSet a  where ...

И, возможно, ограничение могло бы пойти «OutsideOut» в среду, которая обращается к дереву.

Другой возможный подход - использовать PatternSynonym с явная подпись, дающая Обязательное ограничение.

pattern EqGADTBag :: Eq a => [a] -> GADTBag a              -- that Eq a is the *Required*
pattern EqGADTBag{ unEqGADTBag } = MkGADTBag unEqGADTBag   -- without sig infers Eq a only as *Provided*

То есть без этой явной сигнатуры:

*> :i EqGADTBag
pattern EqGADTBag :: () => Eq a => [a] -> GADTBag a

() => Eq a => ... показывает Eq a Предоставлено, возникающее из конструктора GADT.

Теперь мы получаем оба предполагаемых baz, baz2 :: Eq a => GADTBag a -> Maybe [a] -> Bool:

baz (EqGADTBag x) (Just y) = x == y

baz2           x        y  = unEqGADTBag x == fromJust y

Из любопытства: можно дать эти уравнения для baz, baz2, а также уравнения в O.P., используя имена из GADT decl. GHC предупреждает о наложении шаблонов [правильно]; и выводит ограниченный знак для baz.

Интересно, есть ли здесь шаблон дизайна? Не накладывайте ограничений на конструктор данных - то есть не делайте его GADT. Вместо этого объявите «тень» PatternSynonym с обязательными / предоставленными ограничениями.