Morley.Michelson.Typed.Sing

Module, providing singleton boilerplate for T data types.

Some functions from Data.Singletons are provided alternative version here.

Documentation

data SingT :: T -> Type where

Constructors

STKey :: SingT ('TKey :: T)

STUnit :: SingT ('TUnit :: T)

STSignature :: SingT ('TSignature :: T)

STChainId :: SingT ('TChainId :: T)

STOption :: forall (n :: T). (Sing n) -> SingT ('TOption n :: T)

STList :: forall (n :: T). (Sing n) -> SingT ('TList n :: T)

STSet :: forall (n :: T). (Sing n) -> SingT ('TSet n :: T)

STOperation :: SingT ('TOperation :: T)

STContract :: forall (n :: T). (Sing n) -> SingT ('TContract n :: T)

STTicket :: forall (n :: T). (Sing n) -> SingT ('TTicket n :: T)

STPair :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TPair n n :: T)

STOr :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TOr n n :: T)

STLambda :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TLambda n n :: T)

STMap :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TMap n n :: T)

STBigMap :: forall (n :: T) (n :: T). (Sing n) -> (Sing n) -> SingT ('TBigMap n n :: T)

STInt :: SingT ('TInt :: T)

STNat :: SingT ('TNat :: T)

STString :: SingT ('TString :: T)

STBytes :: SingT ('TBytes :: T)

STMutez :: SingT ('TMutez :: T)

STBool :: SingT ('TBool :: T)

STKeyHash :: SingT ('TKeyHash :: T)

STBls12381Fr :: SingT ('TBls12381Fr :: T)

STBls12381G1 :: SingT ('TBls12381G1 :: T)

STBls12381G2 :: SingT ('TBls12381G2 :: T)

STTimestamp :: SingT ('TTimestamp :: T)

STAddress :: SingT ('TAddress :: T)

STChest :: SingT ('TChest :: T)

STChestKey :: SingT ('TChestKey :: T)

STSaplingState :: forall (n :: Nat). (Sing n) -> SingT ('TSaplingState n :: T)

STSaplingTransaction :: forall (n :: Nat). (Sing n) -> SingT ('TSaplingTransaction n :: T)

STNever :: SingT ('TNever :: T)

Instances

(SDecide T, SDecide Peano) => TestCoercion SingT

Defined in Morley.Michelson.Typed.Sing

Methods

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

(SDecide T, SDecide Peano) => TestEquality SingT

Defined in Morley.Michelson.Typed.Sing

Methods

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

Show (SingT x)

Defined in Morley.Michelson.Typed.Sing

Methods

showsPrec :: Int -> SingT x -> ShowS

show :: SingT x -> String

showList :: [SingT x] -> ShowS

NFData (SingT a)

Defined in Morley.Michelson.Typed.Sing

Methods

rnf :: SingT a -> ()

Eq (SingT x)

Defined in Morley.Michelson.Typed.Sing

Methods

(==) :: SingT x -> SingT x -> Bool

(/=) :: SingT x -> SingT x -> Bool

Buildable (SingT t)

Defined in Morley.Michelson.Typed.Sing

Methods

build :: SingT t -> Doc

buildList :: [SingT t] -> Doc

castSingE :: forall (a :: T) (b :: T) t. (SingI a, SingI b) => t a -> Either Text (t b)

Previously, we were using SingI constraints in SingT constructors. That was not so optimal because we have been spending too much space at runtime. Instead of that, we process values of SingT using the function withSingI in those places where the SingI constraint is required. withSingI allows one to create the SingI context for a given Sing.

castM :: forall (a :: T) (b :: T) t m. (SingI a, SingI b, Monad m) => t a -> (forall x. MismatchError T -> m x) -> m (t b)

Monadic version of castSing. Throws an error using the given function if the cast fails.

eqP :: forall (a :: T) (b :: T). (SingI a, SingI b) => Proxy a -> Proxy b -> Maybe (a :~: b)

Version of eqI that uses Proxy

requireEq :: forall (a :: T) (b :: T) m. (SingI a, SingI b, Monad m) => (forall x. MismatchError T -> m x) -> m (a :~: b)

Monadic version of eqI. Throws an error using the given function if the two types are not equal.

Orphan instances

SingKind T

Associated Types

type Demote T = (r :: Type)

Methods

fromSing :: forall (a :: T). Sing a -> Demote T

toSing :: Demote T -> SomeSing T

(SDecide T, SDecide Peano) => SDecide T

Methods

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

SingI 'TAddress

Methods

sing :: Sing 'TAddress

SingI 'TBls12381Fr

Methods

sing :: Sing 'TBls12381Fr

SingI 'TBls12381G1

Methods

sing :: Sing 'TBls12381G1

SingI 'TBls12381G2

Methods

sing :: Sing 'TBls12381G2

SingI 'TBool

Methods

sing :: Sing 'TBool

SingI 'TBytes

Methods

sing :: Sing 'TBytes

SingI 'TChainId

Methods

sing :: Sing 'TChainId

SingI 'TChest

Methods

sing :: Sing 'TChest

SingI 'TChestKey

Methods

sing :: Sing 'TChestKey

SingI 'TInt

Methods

sing :: Sing 'TInt

SingI 'TKey

Methods

sing :: Sing 'TKey

SingI 'TKeyHash

Methods

sing :: Sing 'TKeyHash

SingI 'TMutez

Methods

sing :: Sing 'TMutez

SingI 'TNat

Methods

sing :: Sing 'TNat

SingI 'TNever

Methods

sing :: Sing 'TNever

SingI 'TOperation

Methods

sing :: Sing 'TOperation

SingI 'TSignature

Methods

sing :: Sing 'TSignature

SingI 'TString

Methods

sing :: Sing 'TString

SingI 'TTimestamp

Methods

sing :: Sing 'TTimestamp

SingI 'TUnit

Methods

sing :: Sing 'TUnit

SingI1 'TContract

Methods

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

SingI1 'TList

Methods

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

SingI1 'TOption

Methods

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

SingI1 'TSet

Methods

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

SingI1 'TTicket

Methods

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

SingI1 'TSaplingState

Methods

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

SingI1 'TSaplingTransaction

Methods

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

SingI2 'TBigMap

Methods

liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing ('TBigMap x y)

SingI2 'TLambda

Methods

liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing ('TLambda x y)

SingI2 'TMap

Methods

liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing ('TMap x y)

SingI2 'TOr

Methods

liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing ('TOr x y)

SingI2 'TPair

Methods

liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing ('TPair x y)

SingI n => SingI1 ('TBigMap n :: T -> T)

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ('TBigMap n x)

SingI n => SingI1 ('TLambda n :: T -> T)

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ('TLambda n x)

SingI n => SingI1 ('TMap n :: T -> T)

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ('TMap n x)

SingI n => SingI1 ('TOr n :: T -> T)

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ('TOr n x)

SingI n => SingI1 ('TPair n :: T -> T)

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ('TPair n x)

SingI n => SingI ('TContract n :: T)

Methods

sing :: Sing ('TContract n)

SingI n => SingI ('TList n :: T)

Methods

sing :: Sing ('TList n)

SingI n => SingI ('TOption n :: T)

Methods

sing :: Sing ('TOption n)

SingI n => SingI ('TSaplingState n :: T)

Methods

sing :: Sing ('TSaplingState n)

SingI n => SingI ('TSaplingTransaction n :: T)

Methods

sing :: Sing ('TSaplingTransaction n)

SingI n => SingI ('TSet n :: T)

Methods

sing :: Sing ('TSet n)

SingI n => SingI ('TTicket n :: T)

Methods

sing :: Sing ('TTicket n)

(SingI n, SingI n) => SingI ('TBigMap n n :: T)

Methods

sing :: Sing ('TBigMap n0 n)

(SingI n, SingI n) => SingI ('TLambda n n :: T)

Methods

sing :: Sing ('TLambda n0 n)

(SingI n, SingI n) => SingI ('TMap n n :: T)

Methods

sing :: Sing ('TMap n0 n)

(SingI n, SingI n) => SingI ('TOr n n :: T)

Methods

sing :: Sing ('TOr n0 n)

(SingI n, SingI n) => SingI ('TPair n n :: T)

Methods

sing :: Sing ('TPair n0 n)