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

STNever :: SingT ('TNever :: T)

Instances

SDecide T => 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 => TestEquality SingT

Defined in Morley.Michelson.Typed.Sing

Methods

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

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

castM :: forall (a :: T) (b :: T) t m. (SingI a, SingI b, Monad m) => t a -> (forall x. Demote (KindOf a) -> Demote (KindOf b) -> 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. Demote (KindOf a) -> Demote (KindOf b) -> 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

SDecide T => SDecide T

Methods

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

SingKind T

Associated Types

type Demote T = (r :: Type)

Methods

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

toSing :: Demote T -> SomeSing T

SingI 'TKey

Methods

sing :: Sing 'TKey

SingI 'TUnit

Methods

sing :: Sing 'TUnit

SingI 'TSignature

Methods

sing :: Sing 'TSignature

SingI 'TChainId

Methods

sing :: Sing 'TChainId

SingI 'TOperation

Methods

sing :: Sing 'TOperation

SingI 'TInt

Methods

sing :: Sing 'TInt

SingI 'TNat

Methods

sing :: Sing 'TNat

SingI 'TString

Methods

sing :: Sing 'TString

SingI 'TBytes

Methods

sing :: Sing 'TBytes

SingI 'TMutez

Methods

sing :: Sing 'TMutez

SingI 'TBool

Methods

sing :: Sing 'TBool

SingI 'TKeyHash

Methods

sing :: Sing 'TKeyHash

SingI 'TBls12381Fr

Methods

sing :: Sing 'TBls12381Fr

SingI 'TBls12381G1

Methods

sing :: Sing 'TBls12381G1

SingI 'TBls12381G2

Methods

sing :: Sing 'TBls12381G2

SingI 'TTimestamp

Methods

sing :: Sing 'TTimestamp

SingI 'TAddress

Methods

sing :: Sing 'TAddress

SingI 'TChest

Methods

sing :: Sing 'TChest

SingI 'TChestKey

Methods

sing :: Sing 'TChestKey

SingI 'TNever

Methods

sing :: Sing 'TNever

SingI1 'TList

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.

Methods

withSingI1 :: forall (x :: k) r. SingI x => (SingI ('TList x) => r) -> r

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

Methods

withSingI1 :: forall (x :: k0) r. SingI x => (SingI ('TMap k x) => r) -> r

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

Methods

sing :: Sing ('TOption n)

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

Methods

sing :: Sing ('TList n)

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

Methods

sing :: Sing ('TSet n)

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

Methods

sing :: Sing ('TContract n)

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

Methods

sing :: Sing ('TTicket n)

(SingI n1, SingI n2) => SingI ('TPair n1 n2 :: T)

Methods

sing :: Sing ('TPair n1 n2)

(SingI n1, SingI n2) => SingI ('TOr n1 n2 :: T)

Methods

sing :: Sing ('TOr n1 n2)

(SingI n1, SingI n2) => SingI ('TLambda n1 n2 :: T)

Methods

sing :: Sing ('TLambda n1 n2)

(SingI n1, SingI n2) => SingI ('TMap n1 n2 :: T)

Methods

sing :: Sing ('TMap n1 n2)

(SingI n1, SingI n2) => SingI ('TBigMap n1 n2 :: T)

Methods

sing :: Sing ('TBigMap n1 n2)