Safe Haskell | None |
---|---|
Language | Haskell2010 |
Module, providing singleton boilerplate for
T
data types.
Some functions from Data.Singletons are provided alternative version here.
Some instances which are usually generated with TH are manually implemented
as they require some specific constraints, namely Typeable
and/or
Converge
, not provided in instances generated by TH.
Synopsis
- data SingT z where
- 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)
- STNever :: SingT ('TNever :: T)
- 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)
- eqP :: forall (a :: T) (b :: T). (SingI a, SingI b) => Proxy a -> Proxy b -> Maybe (a :~: b)
- 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)
Documentation
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) | |
STNever :: SingT ('TNever :: T) |
Instances
SDecide T => TestCoercion SingT Source # | |
Defined in Michelson.Typed.Sing | |
SDecide T => TestEquality SingT Source # | |
Defined in Michelson.Typed.Sing |
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) Source #
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) Source #
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) Source #
Monadic version of eqI
.
Throws an error using the given function if the two types are not equal.