| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Morley.Michelson.Typed.Sing
Contents
Description
Module, providing singleton boilerplate for
T data types.
Some functions from Data.Singletons are provided alternative version here.
Synopsis
- data SingT :: T -> Type 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)
- 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)
- 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. MismatchError T -> 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. MismatchError T -> m x) -> m (a :~: b)
Documentation
data SingT :: T -> Type where Source #
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 Source # | |
Defined in Morley.Michelson.Typed.Sing | |
| (SDecide T, SDecide Peano) => TestEquality SingT Source # | |
Defined in Morley.Michelson.Typed.Sing | |
| Show (SingT x) Source # | |
| NFData (SingT a) Source # | |
Defined in Morley.Michelson.Typed.Sing | |
| Eq (SingT x) Source # | |
| Buildable (SingT t) Source # | |
Defined in Morley.Michelson.Typed.Sing | |
castSingE :: forall (a :: T) (b :: T) t. (SingI a, SingI b) => t a -> Either Text (t b) Source #
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) 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. MismatchError T -> m x) -> m (a :~: b) Source #
Monadic version of eqI.
Throws an error using the given function if the two types are not equal.