morley-1.20.0: Developer tools for the Michelson Language
Safe HaskellSafe-Inferred
LanguageHaskell2010

Morley.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 Data.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.

pattern S :: !Nat -> Nat #

pattern Z :: Nat #

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 

data SingNat :: Nat -> Type where Source #

Constructors

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

Instances

Instances details
SDecide Nat => TestCoercion SingNat Source # 
Instance details

Defined in Morley.Util.Peano

Methods

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

SDecide Nat => TestEquality SingNat Source # 
Instance details

Defined in Morley.Util.Peano

Methods

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

Lift (SingNat n :: Type) Source # 
Instance details

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

Defined in Morley.Util.Peano

Methods

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

show :: SingNat n -> String #

showList :: [SingNat n] -> ShowS #

NFData (SingNat n) Source # 
Instance details

Defined in Morley.Util.Peano

Methods

rnf :: SingNat n -> () #

Eq (SingNat n) Source # 
Instance details

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

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

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

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

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

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

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

Peano naturals comparisson

Equations

'Z > _ = 'False 
('S _) > 'Z = 'True 
('S x) > ('S y) = x > y 

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

Peano naturals comparisson

Equations

_ >= 'Z = 'True 
'Z >= _ = 'False 
('S x) >= ('S y) = x >= y 

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

Utility to Decrement a Peano Singleton.

Useful when dealing with the constraint

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

Singleton addition

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

Equations

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

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

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

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

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

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 ... 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 tried to access a 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 LazyTake n xs where ... Source #

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

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 ... 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 Morley.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 Morley.Util.Peano

Length constraints Dictionaries

Length constraints Dictionaries

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

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

Inductive proofs

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

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

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

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

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

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

Proof that x + y = y + x

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

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

Helpers

Orphan instances

Data Nat Source # 
Instance details

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

Associated Types

type Rep Nat :: Type -> Type #

Methods

from :: Nat -> Rep Nat x #

to :: Rep Nat x -> Nat #

Show Nat Source # 
Instance details

Methods

showsPrec :: Int -> Nat -> ShowS #

show :: Nat -> String #

showList :: [Nat] -> ShowS #

NFData Nat Source # 
Instance details

Methods

rnf :: Nat -> () #

Eq Nat Source # 
Instance details

Methods

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

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

SingKind Nat Source # 
Instance details

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

Methods

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

SingI 'Z Source # 
Instance details

Methods

sing :: Sing 'Z #

SingI1 'S Source # 
Instance details

Methods

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

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

Methods

sing :: Sing ('S n) #