Как я могу сказать GHC удовлетворить ограничение уровня типа <=, если я знаю, что это правда во время выполнения?
У меня есть тип, параметризованный натуральным числом n
:
data MyType (n :: Nat) = MyType
Операции с этим типом имеют смысл только тогда n > 0
, когда , поэтому я указал это как ограничение:
myFunction :: (KnownNat n, 1 <= n) => MyType n -> MyType n
myFunction = id
(Обратите внимание, что реальные версии этих функций действительно используются n
, превращая его в значение с natVal
.)
Я хочу создать экзистенциальный тип ( SomeMyType
), который позволяет нам выбирать n
во время выполнения:
data SomeMyType where
SomeMyType :: forall n. (KnownNat n, 1 <= n) => MyType n -> SomeMyType
Для получения значений SomeMyType
я пишу someMyTypeVal
функцию, которая работает следующим образом someNatVal
:
someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n
| n > 0 = case someNatVal n of
Just (SomeNat (_ :: p n)) -> Just (SomeMyType (MyType @n))
Nothing -> Nothing
| otherwise = Nothing
Это отлично сработало бы без 1 <= n
ограничения, но с ограничением я получаю следующую ошибку типа:
• Couldn't match type ‘1 <=? n’ with ‘'True’
arising from a use of ‘SomeMyType’
Как я могу обойти это ограничение? Поскольку я проверил это n > 0
во время выполнения, я не возражал бы использовать операцию, подобную этой, unsafeCoerce
чтобы убедить GHC, что 1 <= n
это правда, но я не могу просто использовать, unsafeCoerce
потому что это потеряло бы значение уровня типа n
.
Как лучше всего с этим справиться?
Ответы
Поковырявшись еще немного, я нашел ответ Джастина Л. на аналогичный вопрос . Он завернул свое решение в typelits-witnessesпакет, который я смог использовать для довольно чистого решения этой проблемы:
someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n = someNatVal n >>= check
where check :: SomeNat -> Maybe SomeMyType
check (SomeNat (_ :: p n)) = case (SNat @1) %<=? (SNat @n) of
LE Refl -> Just (SomeMyType (MyType @n))
NLE _ _ -> Nothing
a %<=? b
позволяет нам сравнивать два натуральных числа на уровне типа и дает нам представление о том a
, меньше ли это b
( LE
) или нет ( NLE
). Это дает нам дополнительное ограничение в LE
случае возврата a SomeMyType
, но попытка сделать это в NLE
случае все равно даст нам ошибку «не удается сопоставить '1 <=? N' с '' True '».
Обратите внимание на явную сигнатуру типа для - check
без нее тип check
выводится как, check :: SomeNat -> Maybe a
и я бы получил следующую ошибку типа:
• Couldn't match type ‘a’ with ‘SomeMyType’
‘a’ is untouchable
inside the constraints: 'True ~ (1 <=? n)
С явной подписью типа все работает, и код даже (в разумных пределах) читается.
В качестве более прямого ответа ограничение 1 <= n
- это просто псевдоним типа для 1 <=? n ~ 'True
. Вы можете небезопасно создать такое ограничение равенства типов с помощью:
{-# LANGUAGE DataKinds, TypeOperators #-}
import Data.Type.Equality
import GHC.TypeLits
import Unsafe.Coerce
unsafeDeclarePositive :: p n -> (1 <=? n) :~: 'True
unsafeDeclarePositive _ = unsafeCoerce Refl
что более или менее то, что typelits-witnesses
делается под капотом.
При наличии этого определения необходимо выполнить проверку типа:
someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n
| n > 0 = case someNatVal n of
Just (SomeNat (pxy :: p n)) ->
case unsafeDeclarePositive pxy of
Refl -> Just (SomeMyType (MyType @n))
Nothing -> Nothing
| otherwise = Nothing