Как работает пакет ограничений?

Идея Data.Constraint.Forall, как я понимаю, заключается в использовании принуждения в реализации, но обеспечить безопасность с использованием типа система. У меня есть два вопроса относительно последнего.

  • Зачем нам нужны две переменные skolem - A и B? Я бы предположил, что если ограничение выполняется "неизвестным" типом, то оно является полиморфным. Как второй тип дает больше безопасности?
  • Почему эти типы называются сколемированными переменными? Я думал, что сколеминизация используется для устранения экзистенциальной квантификации, и здесь мы видим универсальную количественную оценку. Есть ли что-нибудь, что я пропустил?

Ответы

Ответ 1

Возможно с помощью MPTC и функциональной зависимости идентифицировать Skolem, когда это единственная переменная, используя ограничение, параметризованное по ограничению. Трюк, который я использовал для этого, не работает, когда есть два.

С точки зрения кода, написанного вне этого модуля, переменные Skolemized. Они фактически являются "новым" конструктором типа.

Но учитывая, что вы не можете явно ссылаться на эти типы вне модуля, так как они не экспортируются, любой экземпляр, который охватывает эти Skolems, должен быть универсально определен.

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