morley-1.12.0: Developer tools for the Michelson Language
Safe HaskellNone
LanguageHaskell2010

Util.Peano

Description

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.

Synopsis

General

type Peano = Nat Source #

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

Instances details
SingI 'Z Source # 
Instance details

Defined in Util.Peano

Methods

sing :: Sing 'Z #

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

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

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) Source # 
Instance details

Defined in Util.Peano

Methods

sing :: Sing ('S n) #

IndexWitnesses ('[] :: [Nat]) 
Instance details

Defined in Data.Vinyl.TypeLevel

Methods

indexWitnesses :: [Int] #

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

Defined in Data.Vinyl.TypeLevel

Methods

indexWitnesses :: [Int] #

type Sing Source # 
Instance details

Defined in Util.Peano

type Sing = SingNat

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

Equations

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

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

Equations

FromPeano 'Z = 0 
FromPeano ('S a) = 1 + FromPeano a 

class KnownPeano (n :: Peano) where Source #

Methods

peanoVal :: proxy n -> Natural Source #

Instances

Instances details
KnownPeano 'Z Source # 
Instance details

Defined in Util.Peano

Methods

peanoVal :: proxy 'Z -> Natural Source #

KnownPeano a => MockableConstraint (KnownPeano a) Source # 
Instance details

Defined in Util.Peano

KnownPeano a => KnownPeano ('S a) Source # 
Instance details

Defined in Util.Peano

Methods

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

data SingNat (n :: Nat) where Source #

Constructors

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

Instances

Instances details
Eq (SingNat n) Source # 
Instance details

Defined in Util.Peano

Methods

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

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

Show (SingNat n) Source # 
Instance details

Defined in Util.Peano

Methods

showsPrec :: Int -> SingNat n -> ShowS #

show :: SingNat n -> String #

showList :: [SingNat n] -> ShowS #

NFData (SingNat n) Source # 
Instance details

Defined in Util.Peano

Methods

rnf :: SingNat n -> () #

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

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

Get runtime value from singleton.

Lists

type family Length l :: Peano where ... Source #

Equations

Length l = RLength l 

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

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 ... Source #

Equations

Drop 'Z s = s 
Drop ('S _) '[] = '[] 
Drop ('S n) (_ ': s) = Drop n s 

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

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 ... Source #

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 Source #

Comparison of type-level naturals, as a constraint.

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

Instances

Instances details
(RequireLongerThan' l a, LongerThan l a) => RequireLongerThan (l :: [k]) a Source # 
Instance details

Defined in Util.Peano

MockableConstraint (RequireLongerThan l a) Source # 
Instance details

Defined in Util.Peano

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

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

type LongerOrSameLength l a = IsLongerOrSameLength l a ~ 'True Source #

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

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

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

Instances details
(RequireLongerOrSameLength' l a, LongerOrSameLength l a) => RequireLongerOrSameLength (l :: [k]) a Source # 
Instance details

Defined in Util.Peano

MockableConstraint (RequireLongerOrSameLength l a) Source # 
Instance details

Defined in Util.Peano

Length constraints Dictionaries

Orphan instances

SingI 'Z Source # 
Instance details

Methods

sing :: Sing 'Z #

(SingI n, KnownPeano n) => SingI ('S n :: Nat) Source # 
Instance details

Methods

sing :: Sing ('S n) #