Morley.Util.Peano

Type-nat utilities.

We take Peano numbers as base for operations because they make it much easer to prove things to compiler. Their performance does not seem to introduce a problem, because we use nats primarily along with stack which is a linked list with similar performance characteristics.

Many of things we introduce here are covered in type-natural package, but unfortunatelly it does not work with GHC 8.6 at the moment of writing this module. We use Data.Vinyl as source of Peano Nat for now.

General

type Peano = Nat

A convenient alias.

We are going to use Peano numbers for type-dependent logic and normal Nats in user API, need to distinguish them somehow.

pattern S :: !Nat -> Nat

pattern Z :: Nat

type family ToPeano (n :: Nat) :: Peano where ...

Equations

ToPeano 0 = 'Z

ToPeano a = 'S (ToPeano (a - 1))

type family FromPeano (n :: Peano) :: Nat where ...

Equations

FromPeano 'Z = 0

FromPeano ('S a) = 1 + FromPeano a

data SingNat :: Nat -> Type where

Constructors

SZ :: SingNat ('Z :: Nat)

SS :: forall (n :: Nat). !(Sing n) -> SingNat ('S n :: Nat)

Instances

SDecide Nat => TestCoercion SingNat

Defined in Morley.Util.Peano

Methods

testCoercion :: forall (a :: k) (b :: k). SingNat a -> SingNat b -> Maybe (Coercion a b)

SDecide Nat => TestEquality SingNat

Defined in Morley.Util.Peano

Methods

testEquality :: forall (a :: k) (b :: k). SingNat a -> SingNat b -> Maybe (a :~: b)

Lift (SingNat n :: Type)

Defined in Morley.Util.Peano

Methods

lift :: Quote m => SingNat n -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => SingNat n -> Code m (SingNat n)

Show (SingNat n)

Defined in Morley.Util.Peano

Methods

showsPrec :: Int -> SingNat n -> ShowS

show :: SingNat n -> String

showList :: [SingNat n] -> ShowS

NFData (SingNat n)

Defined in Morley.Util.Peano

Methods

rnf :: SingNat n -> ()

Eq (SingNat n)

Defined in Morley.Util.Peano

Methods

(==) :: SingNat n -> SingNat n -> Bool

(/=) :: SingNat n -> SingNat n -> Bool

peanoSing :: forall (n :: Nat). SingIPeano n => SingNat (ToPeano n)

Get the peano singleton for a given type-level nat literal.

>>> peanoSing @2
SS (SS SZ)

peanoSing' :: forall (n :: Nat). KnownNat n => SingNat (ToPeano n)

Same as peanoSing, but only requires KnownNat instance.

Witnesses half the equivalence between KnownNat n and SingI (ToPeano n)

withPeanoSingI :: forall (n :: Nat) r. KnownNat n => (SingIPeano n => r) -> r

Run a computation requiring SingI (ToPeano n) in a context which only has KnownNat n. Mostly useful when used with SomeNat

withSomePeano :: Natural -> (forall n. (KnownNat n, SingIPeano n) => Proxy n -> r) -> r

Lift a given term-level Natural to the type level for a given computation. The computation is expected to accept a Proxy for the sake of convenience: it's easier to get at the type-level natural with ScopedTypeVariables when pattern-matching on the proxy, e.g.

(x :: Natural) `withSomePeano` \(_ :: Proxy n) -> doSomeNatComputation @n

Utility type synonyms

type IsoNatPeano (n :: Nat) (p :: Peano) = (n ~ FromPeano p, ToPeano n ~ p)

A constraint asserting that GHC's Nat n and Peano p are the same (up to an isomorphism)

type SingIPeano (n :: Nat) = SingI (ToPeano n)

A synonym for SingI (ToPeano n). Essentially requires that we can construct a Peano singleton for a given Nat

Peano Arithmetic

type family (x :: Peano) > (y :: Peano) :: Bool where ...

Peano naturals comparisson

Equations

'Z > _ = 'False

('S _) > 'Z = 'True

('S x) > ('S y) = x > y

type family (x :: Peano) >= (y :: Peano) :: Bool where ...

Peano naturals comparisson

Equations

_ >= 'Z = 'True

'Z >= _ = 'False

('S x) >= ('S y) = x >= y

peanoSingDecrement :: Sing n -> Maybe (Sing (Decrement n))

Utility to Decrement a Peano Singleton.

Useful when dealing with the constraint

peanoSingAdd :: SingNat n -> SingNat m -> SingNat (AddPeano n m)

Singleton addition

type family Decrement (a :: Peano) :: Peano where ...

Equations

Decrement 'Z = TypeError ('Text "Expected n > 0")

Decrement ('S n) = n

type family AddPeano (n :: Peano) (m :: Peano) :: Peano where ...

Peano naturals addition

Equations

AddPeano 'Z x = x

AddPeano ('S x) y = 'S (AddPeano x y)

type family SubPeano (n :: Peano) (m :: Peano) :: Peano where ...

Peano naturals subtraction

Equations

SubPeano 'Z ('S m) = TypeError (('Text "Subtracting " ':<>: 'ShowType (FromPeano ('S m))) ':<>: 'Text " from zero")

SubPeano n 'Z = n

SubPeano ('S n) ('S m) = SubPeano n m

type family MinPeano (n :: Peano) (m :: Peano) :: Peano where ...

Out of two Peano naturals, return the smaller one

Equations

MinPeano _ 'Z = 'Z

MinPeano 'Z _ = 'Z

MinPeano ('S n) ('S m) = 'S (MinPeano n m)

type family MaxPeano (n :: Peano) (m :: Peano) :: Peano where ...

Out of two Peano naturals, return the larger one

Equations

MaxPeano n 'Z = n

MaxPeano 'Z m = m

MaxPeano ('S n) ('S m) = 'S (MaxPeano n m)

Lists

type family Length l :: Peano where ...

Equations

Length l = RLength l

type family At (n :: Peano) s where ...

Equations

At 'Z (x ': _) = x

At ('S n) (_ ': xs) = At n xs

At a '[] = TypeError ('Text "You tried to access a non-existing element of the stack, n = " ':<>: 'ShowType (FromPeano a))

type family Drop (n :: Peano) (s :: [k]) :: [k] where ...

Equations

Drop 'Z s = s

Drop ('S _) '[] = '[]

Drop ('S n) (_ ': s) = Drop n s

type family LazyTake n xs where ...

A "lazier" version of Take. LazyTake n xs will always produce a list of exactly n elements. If xs has less than n elements, then some of the elements of the result will be stuck. Similarly, if some tail of xs is stuck or ambiguous, then elements of the result past that point will be stuck.

LazyTake (ToPeano 4) '[1,2,3,4,5] ~ '[1,2,3,4]
LazyTake (ToPeano 4) (1 ': 2 ': 3 ': 4 ': Any) ~ '[1,2,3,4]
LazyTake (ToPeano 4) '[1,2] ~
  '[1, 2, Head '[], Head (Tail '[])]

LazyTake is often better than Take for driving type inference. For example, given the constraint

xs ~ Take (ToPeano 3) xs ++ q ': Drop (ToPeano 4) xs

GHC can't infer anything about the shape of xs. However, the constraint

xs ~ LazyTake (ToPeano 3) xs ++ q ': Drop (ToPeano 4) xs

will allow GHC to infer

xs ~ x1 ': x2 ': x3 ': q ': Drop (ToPeano 4) xs

Equations

LazyTake 'Z _ = '[]

LazyTake ('S n) xs = Head xs ': LazyTake n (Tail xs)

type family Take (n :: Peano) (s :: [k]) :: [k] where ...

A type-level version of take. Note that in many cases, using LazyTake instead will improve type inference.

Equations

Take 'Z _ = '[]

Take _ '[] = '[]

Take ('S n) (a ': s) = a ': Take n s

type family Head (xs :: [k]) :: k where ...

Equations

Head (x ': _1 :: [k]) = x

type family Tail (xs :: [a]) :: [a] where ...

Equations

Tail (_1 ': xs :: [a]) = xs

Morley-specific utils

type family IsLongerThan (l :: [k]) (a :: Peano) :: Bool where ...

Comparison of type-level naturals, as a function.

It is as lazy on the list argument as possible - there is no need to know the whole list if the natural argument is small enough. This property is important if we want to be able to extract reusable parts of code which are aware only of relevant part of stack.

Equations

IsLongerThan (_ ': _) 'Z = 'True

IsLongerThan (_ ': xs) ('S a) = IsLongerThan xs a

IsLongerThan '[] _ = 'False

type LongerThan l a = IsLongerThan l a ~ 'True

Comparison of type-level naturals, as a constraint.

class (RequireLongerThan' l a, LongerThan l a) => RequireLongerThan (l :: [k]) (a :: Peano)

Instances

(RequireLongerThan' l a, LongerThan l a) => RequireLongerThan (l :: [k]) a

Defined in Morley.Util.Peano

type family IsLongerOrSameLength (l :: [k]) (a :: Peano) :: Bool where ...

Similar to IsLongerThan, but returns True when list length equals to the passed number.

Equations

IsLongerOrSameLength _ 'Z = 'True

IsLongerOrSameLength (_ ': xs) ('S a) = IsLongerOrSameLength xs a

IsLongerOrSameLength '[] ('S _) = 'False

type LongerOrSameLength l a = IsLongerOrSameLength l a ~ 'True

IsLongerOrSameLength in form of constraint that gives most information to GHC.

class (RequireLongerOrSameLength' l a, LongerOrSameLength l a) => RequireLongerOrSameLength (l :: [k]) (a :: Peano)

We can have `RequireLongerOrSameLength = (RequireLongerOrSameLength' l a, LongerOrSameLength l a)`, but apparently the printed error message can be caused by LongerOrSameLength rather than RequireLongerOrSameLength'. We do not know for sure how it all works, but we think that if we require constraint X before Y (using multiple `=>`s) then X will always be evaluated first.

Instances

(RequireLongerOrSameLength' l a, LongerOrSameLength l a) => RequireLongerOrSameLength (l :: [k]) a

Defined in Morley.Util.Peano

Length constraints Dictionaries

requireLongerThan :: Rec any stk -> Sing n -> Maybe (Dict (RequireLongerThan stk n))

requireLongerOrSameLength :: Rec any stk -> Sing n -> Maybe (Dict (RequireLongerOrSameLength stk n))

Length constraints Dictionaries

isGreaterThan :: Sing a -> Sing b -> Maybe (Dict ((a > b) ~ 'True))

isGreaterEqualThan :: Sing a -> Sing b -> Maybe (Dict ((a >= b) ~ 'True))

Inductive proofs

additivity :: forall k m n. AddPeano k ('S m) ~ n => SingNat k -> (n > k) :~: 'True

Proof that for naturals, k + (m + 1) = n entails n > k

associativity :: forall y x. SingNat x -> AddPeano x ('S y) :~: 'S (AddPeano x y)

Proof that for naturals, x + (y + 1) = (x + y) + 1

minIdempotency :: SingNat n -> MinPeano n n :~: n

Proof that for naturals, min(n, n) = n

commutativity :: SingNat x -> SingNat y -> AddPeano x y :~: AddPeano y x

Proof that x + y = y + x

transitivity :: ((x >= y) ~ 'True, (y > z) ~ 'True) => SingNat x -> SingNat y -> SingNat z -> (x > z) :~: 'True

Proof that for naturals, x >= y > z implies x > z

Helpers

toNatural :: Peano -> Natural

someSingNat :: Natural -> SomeSing Peano

Orphan instances

Data Nat

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Nat -> c Nat

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Nat

toConstr :: Nat -> Constr

dataTypeOf :: Nat -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Nat)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Nat)

gmapT :: (forall b. Data b => b -> b) -> Nat -> Nat

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r

gmapQ :: (forall d. Data d => d -> u) -> Nat -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Nat -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Nat -> m Nat

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Nat -> m Nat

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Nat -> m Nat

Generic Nat

Associated Types

type Rep Nat :: Type -> Type

Methods

from :: Nat -> Rep Nat x

to :: Rep Nat x -> Nat

Show Nat

Methods

showsPrec :: Int -> Nat -> ShowS

show :: Nat -> String

showList :: [Nat] -> ShowS

NFData Nat

Methods

rnf :: Nat -> ()

Eq Nat

Methods

(==) :: Nat -> Nat -> Bool

(/=) :: Nat -> Nat -> Bool

SingKind Nat

Associated Types

type Demote Nat = (r :: Type)

Methods

fromSing :: forall (a :: Nat). Sing a -> Demote Nat

toSing :: Demote Nat -> SomeSing Nat

SDecide Nat => SDecide Nat

Methods

(%~) :: forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Decision (a :~: b)

SingI 'Z

Methods

sing :: Sing 'Z

SingI1 'S

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ('S x)

SingI n => SingI ('S n :: Nat)

Methods

sing :: Sing ('S n)