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 :: Constraint

Methods

rsubsetC :: (Functor g, RecSubsetFCtx Rec f) => (Rec f [] -> g (Rec f [])) -> Rec f ss -> g (Rec f ss)

rcastC :: RecSubsetFCtx Rec f => Rec f ss -> Rec f []

rreplaceC :: 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 :: Constraint

Methods

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

rcastC :: RecSubsetFCtx Rec f => Rec f ss -> Rec f (r ': rs)

rreplaceC :: 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]

Eq (Sing n)

Defined in Util.Peano

Methods

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

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

Show (Sing n)

Defined in Util.Peano

Methods

showsPrec :: Int -> Sing n -> ShowS

show :: Sing n -> String

showList :: [Sing n] -> ShowS

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

Defined in Data.Vinyl.TypeLevel

Methods

indexWitnesses :: [Int]

data Sing (_ :: Nat)

Defined in Util.Peano

data Sing (_ :: Nat) where

• SZ :: forall (_ :: Nat). Sing Z
• SS :: forall (_ :: Nat) (n :: Peano). (SingI n, KnownPeano n) => Sing n -> Sing (S n)

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 => KnownPeano (S a)

Defined in Util.Peano

Methods

peanoVal :: proxy (S a) -> Natural

data family Sing (a :: k) :: Type

The singleton kind-indexed data family.

Instances

Eq (Sing n)

Defined in Util.Peano

Methods

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

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

Show (Sing n)

Defined in Util.Peano

Methods

showsPrec :: Int -> Sing n -> ShowS

show :: Sing n -> String

showList :: [Sing n] -> ShowS

data Sing (a :: Bool)

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Bool) where

• SFalse :: forall (a :: Bool). Sing False
• STrue :: forall (a :: Bool). Sing True

data Sing (a :: Ordering)

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Ordering) where

• SLT :: forall (a :: Ordering). Sing LT
• SEQ :: forall (a :: Ordering). Sing EQ
• SGT :: forall (a :: Ordering). Sing GT

data Sing (n :: Nat)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where

• SNat :: forall (n :: Nat). KnownNat n => Sing n

data Sing (n :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where

• SSym :: forall (n :: Symbol). KnownSymbol n => Sing n

data Sing (a :: ())

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: ()) where

• STuple0 :: forall (a :: ()). Sing ()

data Sing (a :: Void)

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Void)

data Sing (a :: All)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: All) where

• SAll :: forall (a :: All) (n :: Bool). {..} -> Sing (All n)

data Sing (a :: Any)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: Any) where

• SAny :: forall (a :: Any) (n :: Bool). {..} -> Sing (Any n)

data Sing (_ :: Nat)

Defined in Util.Peano

data Sing (_ :: Nat) where

• SZ :: forall (_ :: Nat). Sing Z
• SS :: forall (_ :: Nat) (n :: Peano). (SingI n, KnownPeano n) => Sing n -> Sing (S n)

data Sing (a :: CT)

Instance of data family Sing for CT.

Defined in Michelson.Typed.Sing

data Sing (a :: CT) where

• SCInt :: forall (a :: CT). Sing CInt
• SCNat :: forall (a :: CT). Sing CNat
• SCString :: forall (a :: CT). Sing CString
• SCBytes :: forall (a :: CT). Sing CBytes
• SCMutez :: forall (a :: CT). Sing CMutez
• SCBool :: forall (a :: CT). Sing CBool
• SCKeyHash :: forall (a :: CT). Sing CKeyHash
• SCTimestamp :: forall (a :: CT). Sing CTimestamp
• SCAddress :: forall (a :: CT). Sing CAddress

data Sing (a :: T)

Instance of data family Sing for T. Custom instance is implemented in order to inject Typeable constraint for some of constructors.

Defined in Michelson.Typed.Sing

data Sing (a :: T) where

• STc :: forall (a :: T) (a :: CT). (SingI a, Typeable a) => Sing a -> Sing (Tc a)
• STKey :: forall (a :: T). Sing TKey
• STUnit :: forall (a :: T). Sing TUnit
• STSignature :: forall (a :: T). Sing TSignature
• STChainId :: forall (a :: T). Sing TChainId
• STOption :: forall (a :: T) (a :: T). (SingI a, Typeable a) => Sing a -> Sing (TOption a)
• STList :: forall (a :: T) (a :: T). (SingI a, Typeable a) => Sing a -> Sing (TList a)
• STSet :: forall (a :: T) (a :: CT). (SingI a, Typeable a) => Sing a -> Sing (TSet a)
• STOperation :: forall (a :: T). Sing TOperation
• STContract :: forall (a :: T) (a :: T). (SingI a, Typeable a) => Sing a -> Sing (TContract a)
• STPair :: forall (a :: T) (a :: T) (b :: T). (SingI a, SingI b, Typeable a, Typeable b) => Sing a -> Sing b -> Sing (TPair a b)
• STOr :: forall (a :: T) (a :: T) (b :: T). (SingI a, SingI b, Typeable a, Typeable b) => Sing a -> Sing b -> Sing (TOr a b)
• STLambda :: forall (a :: T) (a :: T) (b :: T). (SingI a, SingI b, Typeable a, Typeable b) => Sing a -> Sing b -> Sing (TLambda a b)
• STMap :: forall (a :: T) (a :: CT) (b :: T). (SingI a, SingI b, Typeable a, Typeable b) => Sing a -> Sing b -> Sing (TMap a b)
• STBigMap :: forall (a :: T) (a :: CT) (b :: T). (SingI a, SingI b, Typeable a, Typeable b) => Sing a -> Sing b -> Sing (TBigMap a b)

data Sing (b :: [a])

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: [a]) where

• SNil :: forall a (b :: [a]). Sing ([] :: [a])
• SCons :: forall a (b :: [a]) (n1 :: a) (n2 :: [a]). Sing n1 -> Sing n2 -> Sing (n1 ': n2)

data Sing (b :: Maybe a)

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Maybe a) where

• SNothing :: forall a (b :: Maybe a). Sing (Nothing :: Maybe a)
• SJust :: forall a (b :: Maybe a) (n :: a). Sing n -> Sing (Just n)

data Sing (b :: Min a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Min a) where

• SMin :: forall a (b :: Min a) (n :: a). {..} -> Sing (Min n)

data Sing (b :: Max a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Max a) where

• SMax :: forall a (b :: Max a) (n :: a). {..} -> Sing (Max n)

data Sing (b :: First a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: First a) where

• SFirst :: forall a (b :: First a) (n :: a). {..} -> Sing (First n)

data Sing (b :: Last a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Last a) where

• SLast :: forall a (b :: Last a) (n :: a). {..} -> Sing (Last n)

data Sing (a :: WrappedMonoid m)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: WrappedMonoid m) where

• SWrapMonoid :: forall m (a :: WrappedMonoid m) (n :: m). {..} -> Sing (WrapMonoid n)

data Sing (b :: Option a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Option a) where

• SOption :: forall a (b :: Option a) (n :: Maybe a). {..} -> Sing (Option n)

data Sing (b :: Identity a)

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Identity a) where

• SIdentity :: forall a (b :: Identity a) (n :: a). {..} -> Sing (Identity n)

data Sing (b :: First a)

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: First a) where

• SFirst :: forall a (b :: First a) (n :: Maybe a). {..} -> Sing (First n)

data Sing (b :: Last a)

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: Last a) where

• SLast :: forall a (b :: Last a) (n :: Maybe a). {..} -> Sing (Last n)

data Sing (b :: Dual a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Dual a) where

• SDual :: forall a (b :: Dual a) (n :: a). {..} -> Sing (Dual n)

data Sing (b :: Sum a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Sum a) where

• SSum :: forall a (b :: Sum a) (n :: a). {..} -> Sing (Sum n)

data Sing (b :: Product a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Product a) where

• SProduct :: forall a (b :: Product a) (n :: a). {..} -> Sing (Product n)

data Sing (b :: Down a)

Defined in Data.Singletons.Prelude.Ord

data Sing (b :: Down a) where

• SDown :: forall a (b :: Down a) (n :: a). Sing n -> Sing (Down n)

data Sing (b :: NonEmpty a)

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: NonEmpty a) where

• (:%|) :: forall a (b :: NonEmpty a) (n1 :: a) (n2 :: [a]). Sing n1 -> Sing n2 -> Sing (n1 :| n2)

data Sing (b :: Endo a)

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: Endo a) where

• SEndo :: forall a (b :: Endo a) (x :: a ~> a). Sing x -> Sing (Endo x)

data Sing (b :: MaxInternal a)

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: MaxInternal a) where

• SMaxInternal :: forall a (b :: MaxInternal a) (x :: Maybe a). Sing x -> Sing (MaxInternal x)

data Sing (b :: MinInternal a)

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: MinInternal a) where

• SMinInternal :: forall a (b :: MinInternal a) (x :: Maybe a). Sing x -> Sing (MinInternal x)

data Sing (c :: Either a b)

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: Either a b) where

• SLeft :: forall a b (c :: Either a b) (n :: a). Sing n -> Sing (Left n :: Either a b)
• SRight :: forall a b (c :: Either a b) (n :: b). Sing n -> Sing (Right n :: Either a b)

data Sing (c :: (a, b))

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: (a, b)) where

• STuple2 :: forall a b (c :: (a, b)) (n1 :: a) (n2 :: b). Sing n1 -> Sing n2 -> Sing ((,) n1 n2)

data Sing (c :: Arg a b)

Defined in Data.Singletons.Prelude.Semigroup

data Sing (c :: Arg a b) where

• SArg :: forall a b (c :: Arg a b) (n1 :: a) (n2 :: b). Sing n1 -> Sing n2 -> Sing (Arg n1 n2)

newtype Sing (f :: k1 ~> k2)

Defined in Data.Singletons.Internal

newtype Sing (f :: k1 ~> k2) = SLambda {

• applySing :: forall (t :: k1). Sing t -> Sing (f @@ t)

}

data Sing (b :: StateL s a)

Defined in Data.Singletons.Prelude.Traversable

data Sing (b :: StateL s a) where

• SStateL :: forall s a (b :: StateL s a) (x :: s ~> (s, a)). Sing x -> Sing (StateL x)

data Sing (b :: StateR s a)

Defined in Data.Singletons.Prelude.Traversable

data Sing (b :: StateR s a) where

• SStateR :: forall s a (b :: StateR s a) (x :: s ~> (s, a)). Sing x -> Sing (StateR x)

data Sing (d :: (a, b, c))

Defined in Data.Singletons.Prelude.Instances

data Sing (d :: (a, b, c)) where

• STuple3 :: forall a b c (d :: (a, b, c)) (n1 :: a) (n2 :: b) (n3 :: c). Sing n1 -> Sing n2 -> Sing n3 -> Sing ((,,) n1 n2 n3)

data Sing (c :: Const a b)

Defined in Data.Singletons.Prelude.Const

data Sing (c :: Const a b) where

• SConst :: forall k a (b :: k) (c :: Const a b) (a1 :: a). {..} -> Sing (Const a1 :: Const a b)

data Sing (e :: (a, b, c, d))

Defined in Data.Singletons.Prelude.Instances

data Sing (e :: (a, b, c, d)) where

• STuple4 :: forall a b c d (e :: (a, b, c, d)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing ((,,,) n1 n2 n3 n4)

data Sing (f :: (a, b, c, d, e))

Defined in Data.Singletons.Prelude.Instances

data Sing (f :: (a, b, c, d, e)) where

• STuple5 :: forall a b c d e (f :: (a, b, c, d, e)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing ((,,,,) n1 n2 n3 n4 n5)

data Sing (g :: (a, b, c, d, e, f))

Defined in Data.Singletons.Prelude.Instances

data Sing (g :: (a, b, c, d, e, f)) where

• STuple6 :: forall a b c d e f (g :: (a, b, c, d, e, f)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e) (n6 :: f). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing n6 -> Sing ((,,,,,) n1 n2 n3 n4 n5 n6)

data Sing (h :: (a, b, c, d, e, f, g))

Defined in Data.Singletons.Prelude.Instances

data Sing (h :: (a, b, c, d, e, f, g)) where

• STuple7 :: forall a b c d e f g (h :: (a, b, c, d, e, f, g)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e) (n6 :: f) (n7 :: g). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing n6 -> Sing n7 -> Sing ((,,,,,,) n1 n2 n3 n4 n5 n6 n7)

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

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

Orphan instances

SingI Z

Methods

sing :: Sing Z

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

Methods

sing :: Sing (S n)

Eq (Sing n)

Methods

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

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

Show (Sing n)

Methods

showsPrec :: Int -> Sing n -> ShowS

show :: Sing n -> String

showList :: [Sing n] -> ShowS