Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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 #
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 # | |
RenderDoc (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.