This module provides the ability to refine given
KnownNat
instances using
GHC.TypeLits's comparison API, and also the
ability to prove inequalities and upper/lower limits.
If a library function requires
1 <= n constraint,
but only
KnownNat n is available:
foo :: (KnownNat n, 1 <= n) => Proxy n -> Int
bar :: KnownNat n => Proxy n -> Int
bar n = case (Proxy :: Proxy 1) %<=? n of
LE Refl -> foo n
NLE _ -> 0
foo requires that
1 <= n, but
bar has to
handle all cases of
n.
%<=? lets you compare the
KnownNats in two
Proxys and returns a
:<=?,
which has two constructors,
LE and
NLE.
If you pattern match on the result, in the
LE branch, the
constraint
1 <= n will be satisfied according to GHC, so
bar can safely call
foo, and GHC will recognize that
1 <= n.
In the
NLE branch, the constraint that
1 > n is
satisfied, so any functions that require that constraint would be
callable.
For convenience,
isLE and
isNLE are also offered:
bar :: KnownNat n => Proxy n -> Int
bar n = case isLE (Proxy :: Proxy 1) n of
Just Refl -> foo n
Nothing -> 0
Similarly, if a library function requires something involving
CmpNat, you can use
cmpNat and the
SCmpNat type:
foo1 :: (KnownNat n, CmpNat 5 n ~ LT) => Proxy n -> Int
foo2 :: (KnownNat n, CmpNat 5 n ~ GT) => Proxy n -> Int
bar :: KnownNat n => Proxy n -> Int
bar n = case cmpNat (Proxy :: Proxy 5) n of
CLT Refl -> foo1 n
CEQ Refl -> 0
CGT Refl -> foo2 n
You can use the
Refl that
cmpNat gives you with
flipCmpNat and
cmpNatLE to "flip" the inequality or turn
it into something compatible with
<=? (useful for when you
have to work with libraries that mix the two methods) or
cmpNatEq and
eqCmpNat to get to/from witnesses for
equality of the two
Nats.
This module is useful for helping bridge between libraries that use
different
Nat-based comparison systems in their type
constraints.