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.

data Nat

A mere approximation of the natural numbers. And their image as lifted by -XDataKinds corresponds to the actual natural numbers.

Constructors

Z

S !Nat

Instances

SingI 'Z

Defined in Morley.Util.Peano

Methods

sing :: Sing 'Z

RecSubset (Rec :: (k -> Type) -> [k] -> Type) ('[] :: [k]) (ss :: [k]) ('[] :: [Nat])

Defined in Data.Vinyl.Lens

Associated Types

type RecSubsetFCtx Rec f

Methods

rsubsetC :: forall g (f :: k0 -> Type). (Functor g, RecSubsetFCtx Rec f) => (Rec f '[] -> g (Rec f '[])) -> Rec f ss -> g (Rec f ss)

rcastC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f ss -> Rec f '[]

rreplaceC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f '[] -> Rec f ss -> Rec f ss

(RElem r ss i, RSubset rs ss is) => RecSubset (Rec :: (k -> Type) -> [k] -> Type) (r ': rs :: [k]) (ss :: [k]) (i ': is)

Defined in Data.Vinyl.Lens

Associated Types

type RecSubsetFCtx Rec f

Methods

rsubsetC :: forall g (f :: k0 -> Type). (Functor g, RecSubsetFCtx Rec f) => (Rec f (r ': rs) -> g (Rec f (r ': rs))) -> Rec f ss -> g (Rec f ss)

rcastC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f ss -> Rec f (r ': rs)

rreplaceC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f (r ': rs) -> Rec f ss -> Rec f ss

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

Defined in Morley.Util.Peano

Methods

sing :: Sing ('S n)

IndexWitnesses ('[] :: [Nat])

Defined in Data.Vinyl.TypeLevel

Methods

indexWitnesses :: [Int]

(IndexWitnesses is, NatToInt i) => IndexWitnesses (i ': is)

Defined in Data.Vinyl.TypeLevel

Methods

indexWitnesses :: [Int]

type Sing

Defined in Morley.Util.Peano

type Sing = SingNat

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 (n :: Nat) where

Constructors

SZ :: SingNat 'Z

SS :: !(SingNat n) -> SingNat ('S n)

Instances

Eq (SingNat n)

Defined in Morley.Util.Peano

Methods

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

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

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 -> ()

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

Equations

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

Decrement ('S n) = n

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

Equations

'Z > _ = 'False

('S _) > 'Z = 'True

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

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

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

>>> peanoSing @2
SS (SS SZ)

Peano Arithmetic

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

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

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 Take (n :: Peano) (s :: [k]) :: [k] where ...

Equations

Take 'Z _ = '[]

Take _ '[] = '[]

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

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

MockableConstraint (RequireLongerThan l a)

Defined in Morley.Util.Peano

Methods

unsafeProvideConstraint :: Dict (RequireLongerThan l a)

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

MockableConstraint (RequireLongerOrSameLength l a)

Defined in Morley.Util.Peano

Methods

unsafeProvideConstraint :: Dict (RequireLongerOrSameLength l a)

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))

Orphan instances

SingI 'Z

Methods

sing :: Sing 'Z

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

Methods

sing :: Sing ('S n)