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.

type family ToPeano (n :: Nat) :: Nat where ...

Equations

ToPeano 0 = Z

ToPeano a = S (ToPeano (a - 1))

type family Length l where ...

Equations

Length l = RLength l

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

peanoVal' :: forall n. KnownPeano n => 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

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 :: Nat). 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
• 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)

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

Morley-specific utils

type family IsLongerThan (l :: [k]) (a :: Nat) :: 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.

type family RequireLongerThan (l :: [k]) (a :: Nat) :: Constraint where ...

Comparison of type-level naturals, raises human-readable compile error when does not hold.

This is for in eDSL use only, GHC cannot reason about such constraint.

Equations

RequireLongerThan l a = If (IsLongerThan l a) (() :: Constraint) (TypeError ((((Text "Stack element #" :<>: ShowType (FromPeano a)) :<>: Text " is not accessible") :$$: ((Text "Current stack has size of only " :<>: ShowType (LengthWithTail l)) :<>: Text ":")) :$$: ShowType l))

requiredLongerThan :: forall l a r. RequireLongerThan l a => (LongerThan l a => r) -> r

Derive LongerThan from RequireLongerThan.

Orphan instances

SingI Z

Methods

sing :: Sing Z

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

Methods

sing :: Sing (S n)

Eq (Sing n)

Methods

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

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