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 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 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, KnownPeano n) => SingI ('S n :: Nat)

Defined in 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 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

class KnownPeano (n :: Peano) where

Methods

peanoVal :: proxy n -> Natural

Instances

KnownPeano 'Z

Defined in Util.Peano

Methods

peanoVal :: proxy 'Z -> Natural

KnownPeano a => MockableConstraint (KnownPeano a)

Defined in Util.Peano

Methods

provideConstraintUnsafe :: Dict (KnownPeano a)

KnownPeano a => KnownPeano ('S a)

Defined in Util.Peano

Methods

peanoVal :: proxy ('S a) -> Natural

data SingNat (n :: Nat) where

Constructors

SZ :: SingNat 'Z

SS :: (SingI n, KnownPeano n) => SingNat n -> SingNat ('S n)

Instances

Eq (SingNat n)

Defined in Util.Peano

Methods

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

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

Show (SingNat n)

Defined in Util.Peano

Methods

showsPrec :: Int -> SingNat n -> ShowS

show :: SingNat n -> String

showList :: [SingNat n] -> ShowS

NFData (SingNat n)

Defined in Util.Peano

Methods

rnf :: SingNat n -> ()

peanoVal' :: forall n. KnownPeano n => Natural

peanoValSing :: forall n. KnownPeano n => Sing n -> Natural

Get runtime value from singleton.

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 try to access to 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 Util.Peano

MockableConstraint (RequireLongerThan l a)

Defined in Util.Peano

Methods

provideConstraintUnsafe :: 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 Util.Peano

MockableConstraint (RequireLongerOrSameLength l a)

Defined in Util.Peano

Methods

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

Orphan instances

SingI 'Z

Methods

sing :: Sing 'Z

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

Methods

sing :: Sing ('S n)