Избегайте ограничения класса на уровне naturals

Question

Я использую Nat типа из модуля GHC.TypeLits, который, по общему признанию, должен быть определен в отдельной библиотеке. В любом случае GHC.TypeLits имеет класс KnownNat с функцией класса natVal, которая преобразует время компиляции Nat во время выполнения Integer. Существует также функция типа (+), которая добавляет время компиляции Nat s.

Проблема в том, что данный (KnownNat n1, KnownNat n2), GHC не может получить это KnownNat (n1 + n2).

Это приводит к взрыву ограничений, которые необходимо добавить, когда я добавляю naturals уровня.

Одним из вариантов было бы определить натуральные числа себя так:

data Nat = Zero | Succ Nat 

Или, возможно, использовать библиотеку как type-natural. Но, кажется, глупо не использовать Nats, которые встроены в GHC, которые также позволяют хорошо использовать буквенные числа типов (т.е. 0, 1) вместо того, чтобы определить:

N0 = Zero 
N1 = Succ N0 
etc... 

Есть в любом случае вокруг этого вопрос с GHC KnownNat ограничений, требуемых повсюду? Или я должен просто игнорировать модуль GHC.TypeLits для моей проблемы?

Answer 1

Этого GHC типа проверка плагин делает именно это (производный «сложное» KnownNat ограничение из тех, что уже имеется): https://hackage.haskell.org/package/ghc-typelits-knownnat

Если «типа проверка плагин» звучит немного пугающий (он сделал для меня в первую очередь), это на самом деле очень просто в использовании. Просто добавьте его в качестве зависимости в файле пакета (или междусобойчик установить его), как и любой другой пакет, то либо добавить:

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} 

к началу исходных файлов (так же, как в LANGUAGE прагме), или добавить его как вариант в глобальном масштабе в вашем файле пакета.

Существует также другой плагин того же автора, который очень полезен для работы с typelit Nats: https://hackage.haskell.org/package/ghc-typelits-natnormalise. Этот способ позволяет вывести равенство выражений типа Nat, которые GHC само по себе отказывается: такие вещи, как n + (m + 1) ~ (n + 1) + m, которые появляются все время, когда GHC пытается доказать соответствие «ожидаемых» и «фактических» типов.