GHC.TypeLits.Compare

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.

<= and <=?

data (:<=?) :: Nat -> Nat -> Type where

Two possible ordered relationships between two natural numbers.

Constructors

LE :: ((m <=? n) :~: 'True) -> m :<=? n

NLE :: ((m <=? n) :~: 'False) -> ((n <=? m) :~: 'True) -> m :<=? n

(%<=?) :: (KnownNat m, KnownNat n) => p m -> q n -> m :<=? n

Compare m and n, classifying their relationship into some constructor of :<=?.

Convenience functions

isLE :: (KnownNat m, KnownNat n) => p m -> q n -> Maybe ((m <=? n) :~: 'True)

Simplified version of %<=?: check if m is less than or equal to to n. If it is, match on Just Refl to get GHC to believe it, within the body of the pattern match.

isNLE :: (KnownNat m, KnownNat n) => p m -> q n -> Maybe ((m <=? n) :~: 'False)

Simplified version of %<=?: check if m is not less than or equal to to n. If it is, match on Just Refl to get GHC to believe it, within the body of the pattern match.

CmpNat

data SCmpNat :: Nat -> Nat -> Type where

Three possible ordered relationships between two natural numbers.

Constructors

CLT :: (CmpNat m n :~: 'LT) -> SCmpNat m n

CEQ :: (CmpNat m n :~: 'EQ) -> (m :~: n) -> SCmpNat m n

CGT :: (CmpNat m n :~: 'GT) -> SCmpNat m n

cmpNat :: (KnownNat m, KnownNat n) => p m -> q n -> SCmpNat m n

Compare m and n, classifying their relationship into some constructor of SCmpNat.

Manipulating witnesses

flipCmpNat :: SCmpNat m n -> SCmpNat n m

Flip an inequality.

cmpNatEq :: (CmpNat m n :~: 'EQ) -> m :~: n

CmpNat m n being EQ implies that m is equal to n.

eqCmpNat :: (m :~: n) -> CmpNat m n :~: 'EQ

A witness of equality implies that CmpNat m n is Eq.

reflCmpNat :: (m :~: n) -> SCmpNat m n

Inject a witness of equality into an SCmpNat at CEQ.

cmpNatLE :: SCmpNat m n -> m :<=? n

Convert to :<=?

cmpNatGOrdering :: SCmpNat n m -> GOrdering n m

Convert to GOrdering

Since: 0.4.0.0