| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Universe
Synopsis
- data Esc a
- data Some (tag :: k -> Type) where
- data SomeTypeIn uni = forall k (a :: k). SomeTypeIn !(uni (Esc a))
- data Kinded uni ta where
- data ValueOf uni a = ValueOf !(uni (Esc a)) !a
- class Contains uni a where
- type Includes uni = Permits (Contains uni)
- knownUniOf :: uni `Contains` a => proxy a -> uni (Esc a)
- someType :: forall k (a :: k) uni. uni `Contains` a => SomeTypeIn uni
- someValueOf :: forall a uni. uni (Esc a) -> a -> Some (ValueOf uni)
- someValue :: forall a uni. uni `Contains` a => a -> Some (ValueOf uni)
- someValueType :: Some (ValueOf uni) -> SomeTypeIn uni
- newtype DecodeUniM a = DecodeUniM {
- unDecodeUniM :: StateT [Int] Maybe a
- class Closed uni where
- type Everywhere uni (constr :: Type -> Constraint) :: Constraint
- encodeUni :: uni a -> [Int]
- withDecodedUni :: (forall k (a :: k). Typeable k => uni (Esc a) -> DecodeUniM r) -> DecodeUniM r
- bring :: uni `Everywhere` constr => proxy constr -> uni (Esc a) -> (constr a => r) -> r
- decodeKindedUni :: Closed uni => [Int] -> Maybe (SomeTypeIn (Kinded uni))
- peelUniTag :: DecodeUniM Int
- type family Permits constr
- type family EverywhereAll uni constrs where ...
- type (<:) uni1 uni2 = uni1 `Everywhere` Includes uni2
- class HasUniApply (uni :: Type -> Type) where
- checkStar :: forall uni a (x :: a). Typeable a => uni (Esc x) -> Maybe (a :~: Type)
- withApplicable :: forall (a :: Type) (ab :: Type) f x uni m r. (Typeable ab, Typeable a, MonadPlus m) => uni (Esc (f :: ab)) -> uni (Esc (x :: a)) -> (forall (b :: Type). (Typeable b, ab ~ (a -> b)) => m r) -> m r
- tryUniApply :: (MonadPlus m, HasUniApply uni) => SomeTypeIn (Kinded uni) -> SomeTypeIn (Kinded uni) -> m (SomeTypeIn (Kinded uni))
- class GShow (t :: k -> Type) where
- gshowsPrec :: forall (a :: k). Int -> t a -> ShowS
- gshow :: forall {k} t (a :: k). GShow t => t a -> String
- class GEq (f :: k -> Type) where
- defaultEq :: forall {k} f (a :: k) (b :: k). GEq f => f a -> f b -> Bool
- data (a :: k) :~: (b :: k) where
- data DSum (tag :: k -> Type) (f :: k -> Type) = !(tag a) :=> (f a)
Documentation
data Some (tag :: k -> Type) where #
Instances
| (Closed uni, Everywhere uni PrettyConst) => PrettyBy ConstConfig (Some (ValueOf uni)) Source # | |
Defined in PlutusCore.Pretty.PrettyConst Methods prettyBy :: ConstConfig -> Some (ValueOf uni) -> Doc ann # prettyListBy :: ConstConfig -> [Some (ValueOf uni)] -> Doc ann # | |
| Applicative m => Monoid (Some m) | |
| Applicative m => Semigroup (Some m) | |
| GRead f => Read (Some f) | |
| GShow tag => Show (Some tag) | |
| GNFData tag => NFData (Some tag) | |
Defined in Data.Some.Newtype | |
| (Closed uni, Everywhere uni Flat) => Flat (Some (ValueOf uni)) | |
| GEq tag => Eq (Some tag) | |
| GCompare tag => Ord (Some tag) | |
Defined in Data.Some.Newtype | |
| (Closed uni, GEq uni, Everywhere uni Eq, Everywhere uni Hashable) => Hashable (Some (ValueOf uni)) Source # | |
Defined in Universe.Core | |
| (Closed uni, Everywhere uni ExMemoryUsage) => ExMemoryUsage (Some (ValueOf uni)) Source # | |
Defined in PlutusCore.Evaluation.Machine.ExMemoryUsage | |
| (Closed uni, Everywhere uni PrettyConst) => Pretty (Some (ValueOf uni)) Source # | |
data SomeTypeIn uni Source #
A particular type from a universe.
Constructors
| forall k (a :: k). SomeTypeIn !(uni (Esc a)) |
Instances
data Kinded uni ta where Source #
Instances
| GShow uni => GShow (Kinded uni :: Type -> Type) Source # | |
Defined in Universe.Core Methods gshowsPrec :: forall (a :: k). Int -> Kinded uni a -> ShowS # | |
| (Typeable k, Contains uni a) => Contains (Kinded uni) (a :: k) Source # | A |
| Pretty (SomeTypeIn uni) => Pretty (SomeTypeIn (Kinded uni)) Source # | |
Defined in PlutusCore.Pretty.PrettyConst Methods pretty :: SomeTypeIn (Kinded uni) -> Doc ann # prettyList :: [SomeTypeIn (Kinded uni)] -> Doc ann # | |
| GShow uni => Show (Kinded uni ta) Source # | |
A value of a particular type from a universe.
Instances
class Contains uni a where Source #
A class for enumerating types and fully instantiated type formers that uni contains.
For example, a particular ExampleUni may have monomorphic types in it:
instance ExampleUni Contains Integer where ...
instance ExampleUni Contains Bool where ...
as well as polymorphic ones:
instance ExampleUni Contains [] where ...
instance ExampleUni Contains (,) where ...
as well as their instantiations:
instance ExampleUni Contains a => ExampleUni Contains [a] where ...
instance (ExampleUni Contains a, ExampleUni Contains b) => ExampleUni Contains (a, b) where ...
(a universe can have any subset of the mentioned sorts of types, for example it's fine to have instantiated polymorphic types and not have uninstantiated ones and vice versa)
Note that when used as a constraint of a function Contains does not allow you to directly
express things like "uni has the Integer, Bool and [] types and type formers",
because [] is not fully instantiated. So you can only say "uni has Integer, Bool,
[Integer], [Bool], [[Integer]], [[Bool]] etc" and such manual enumeration is annoying,
so we'd really like to be able to say that uni has lists of arbitrary built-in types
(including lists of lists etc). Contains does not allow that, but Includes does.
For example, in the body of the following definition:
foo :: (uni Includes Integer, uni Includes Bool, uni Includes []) => ...
foo = ...
you can make use of the fact that uni has lists of arbitrary included types (integers,
booleans and lists).
Hence most of the time opt for using the more flexible Includes.
Includes is defined in terms of Contains, so you only need to provide a Contains instance
per type from the universe and you'll get Includes for free.
Instances
knownUniOf :: uni `Contains` a => proxy a -> uni (Esc a) Source #
Same as knownUni, but receives a proxy.
someType :: forall k (a :: k) uni. uni `Contains` a => SomeTypeIn uni Source #
Wrap a type into SomeTypeIn, provided it's in the universe.
someValueOf :: forall a uni. uni (Esc a) -> a -> Some (ValueOf uni) Source #
Wrap a value into Some (ValueOf uni), given its explicit type tag.
someValue :: forall a uni. uni `Contains` a => a -> Some (ValueOf uni) Source #
Wrap a value into Some (ValueOf uni), provided its type is in the universe.
someValueType :: Some (ValueOf uni) -> SomeTypeIn uni Source #
newtype DecodeUniM a Source #
A monad to decode types from a universe in.
We use a monad for decoding, because parsing arguments of polymorphic built-in types can peel off
an arbitrary amount of type tags from the input list of tags and so we have state, which is
convenient to handle with, well, StateT.
Constructors
| DecodeUniM | |
Fields
| |
Instances
class Closed uni where Source #
A universe is Closed, if it's known how to constrain every type from the universe and
every type can be encoded to / decoded from a sequence of integer tags.
The universe doesn't have to be finite and providing support for infinite universes is the
reason why we encode a type as a sequence of integer tags as opposed to a single integer tag.
For example, given
data U a where
UList :: !(U a) -> U [a]
UInt :: U IntUList (UList UInt) can be encoded to [0,0,1] where 0 and 1 are the integer tags of the
UList and UInt constructors, respectively.
Associated Types
type Everywhere uni (constr :: Type -> Constraint) :: Constraint Source #
A constrant for "constr a holds for any a from uni".
Methods
encodeUni :: uni a -> [Int] Source #
Encode a type as a sequence of Int tags.
The opposite of decodeUni.
withDecodedUni :: (forall k (a :: k). Typeable k => uni (Esc a) -> DecodeUniM r) -> DecodeUniM r Source #
Decode a type and feed it to the continuation.
bring :: uni `Everywhere` constr => proxy constr -> uni (Esc a) -> (constr a => r) -> r Source #
Bring a constr a instance in scope, provided a is a type from the universe and
constr holds for any type from the universe.
Instances
| Closed DefaultUni Source # | |
Defined in PlutusCore.Default.Universe Associated Types type Everywhere DefaultUni constr Source # Methods encodeUni :: DefaultUni a -> [Int] Source # withDecodedUni :: (forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r) -> DecodeUniM r Source # bring :: Everywhere DefaultUni constr => proxy constr -> DefaultUni (Esc a) -> (constr a => r) -> r Source # | |
decodeKindedUni :: Closed uni => [Int] -> Maybe (SomeTypeIn (Kinded uni)) Source #
peelUniTag :: DecodeUniM Int Source #
Peel off a tag from the input list of type tags.
type family Permits constr Source #
constr elaborates to one of
-
constr f
forall a. constr a => constr (f a)
forall a b. (constr a, constr b) => constr (f a b)
forall a b c. (constr a, constr b, constr c) => constr (f a b c)Permits f
depending on the kind of f. This allows us to say things like
( constr Permits Integer
, constr Permits []
, constr Permits (,)
)
and thus constraint every type from the universe (including polymorphic ones) to satisfy
constr, which is how we provide an implementation of Everywhere for universes with
polymorphic types.
Permits is an open type family, so you can provide type instances for fs expecting
more type arguments than 3 if you need that.
Note that, say, constr elaborates toPermits []
forall a. constr a => constr [a]
and for certain type classes that does not make sense (e.g. the Generic instance of []
does not require the type of elements to be Generic), however it's not a problem because
we use Permit to constrain the whole universe and so we know that arguments of polymorphic
built-in types are builtins themselves are hence do satisfy the constraint and the fact that
these constraints on arguments do not get used in the polymorphic case only means that they
get ignored.
Instances
| type Permits constr Source # | |
Defined in Universe.Core type Permits constr | |
| type Permits constr Source # | |
Defined in Universe.Core type Permits constr | |
| type Permits constr Source # | |
Defined in Universe.Core type Permits constr | |
| type Permits constr Source # | |
Defined in Universe.Core type Permits constr | |
type family EverywhereAll uni constrs where ... Source #
Equations
| EverywhereAll uni '[] = () | |
| EverywhereAll uni (constr ': constrs) = (uni `Everywhere` constr, uni `EverywhereAll` constrs) |
type (<:) uni1 uni2 = uni1 `Everywhere` Includes uni2 Source #
A constraint for "uni1 is a subuniverse of uni2".
class HasUniApply (uni :: Type -> Type) where Source #
A class for "uni has general type application".
Methods
uniApply :: forall k l (f :: k -> l) a. uni (Esc f) -> uni (Esc a) -> uni (Esc (f a)) Source #
Apply a type constructor to an argument.
Arguments
| :: uni tb | The type. |
| -> r | What to return if the type is not an application. |
| -> (forall k l (f :: k -> l) a. tb ~ Esc (f a) => uni (Esc f) -> uni (Esc a) -> r) | The continuation taking a function and an argument. |
| -> r |
Deconstruct a type application into the function and the argument and feed them to the continuation. If the type is not an application, then return the default value.
Instances
| HasUniApply DefaultUni Source # | |
Defined in PlutusCore.Default.Universe Methods uniApply :: forall k l (f :: k -> l) (a :: k). DefaultUni (Esc f) -> DefaultUni (Esc a) -> DefaultUni (Esc (f a)) Source # matchUniApply :: DefaultUni tb -> r -> (forall k l (f :: k -> l) (a :: k). tb ~ Esc (f a) => DefaultUni (Esc f) -> DefaultUni (Esc a) -> r) -> r Source # | |
checkStar :: forall uni a (x :: a). Typeable a => uni (Esc x) -> Maybe (a :~: Type) Source #
Check if the kind of the given type from the universe is Type.
withApplicable :: forall (a :: Type) (ab :: Type) f x uni m r. (Typeable ab, Typeable a, MonadPlus m) => uni (Esc (f :: ab)) -> uni (Esc (x :: a)) -> (forall (b :: Type). (Typeable b, ab ~ (a -> b)) => m r) -> m r Source #
Check if one type from the universe can be applied to another (i.e. check that the expected
kind of the argument matches the actual one) and call the continuation in the refined context.
Fail with mzero otherwise.
tryUniApply :: (MonadPlus m, HasUniApply uni) => SomeTypeIn (Kinded uni) -> SomeTypeIn (Kinded uni) -> m (SomeTypeIn (Kinded uni)) Source #
Apply a type constructor to an argument, provided kinds match.
class GShow (t :: k -> Type) where #
Methods
gshowsPrec :: forall (a :: k). Int -> t a -> ShowS #
Instances
| GShow SNat | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a :: k). Int -> SNat a -> ShowS # | |
| GShow SChar | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a :: k). Int -> SChar a -> ShowS # | |
| GShow SSymbol | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a :: k). Int -> SSymbol a -> ShowS # | |
| GShow DefaultUni Source # | |
Defined in PlutusCore.Default.Universe Methods gshowsPrec :: forall (a :: k). Int -> DefaultUni a -> ShowS # | |
| GShow uni => GShow (Kinded uni :: Type -> Type) Source # | |
Defined in Universe.Core Methods gshowsPrec :: forall (a :: k). Int -> Kinded uni a -> ShowS # | |
| (GShow uni, Closed uni, Everywhere uni Show) => GShow (ValueOf uni :: Type -> Type) Source # | |
Defined in Universe.Core Methods gshowsPrec :: forall (a :: k). Int -> ValueOf uni a -> ShowS # | |
| GShow (TypeRep :: k -> Type) | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a :: k0). Int -> TypeRep a -> ShowS # | |
| GShow ((:~:) a :: k -> Type) | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k0). Int -> (a :~: a0) -> ShowS # | |
| GShow (GOrdering a :: k -> Type) | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k0). Int -> GOrdering a a0 -> ShowS # | |
| (GShow a, GShow b) => GShow (Product a b :: k -> Type) | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k0). Int -> Product a b a0 -> ShowS # | |
| (GShow a, GShow b) => GShow (Sum a b :: k -> Type) | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k0). Int -> Sum a b a0 -> ShowS # | |
| GShow ((:~~:) a :: k -> Type) | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k0). Int -> (a :~~: a0) -> ShowS # | |
| (GShow a, GShow b) => GShow (a :*: b :: k -> Type) | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k0). Int -> (a :*: b) a0 -> ShowS # | |
| (GShow a, GShow b) => GShow (a :+: b :: k -> Type) | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k0). Int -> (a :+: b) a0 -> ShowS # | |
class GEq (f :: k -> Type) where #
Instances
| GEq SNat | |
| GEq SChar | |
| GEq SSymbol | |
| GEq DefaultUni Source # | |
Defined in PlutusCore.Default.Universe Methods geq :: forall (a :: k) (b :: k). DefaultUni a -> DefaultUni b -> Maybe (a :~: b) # | |
| (GEq uni, Closed uni, Everywhere uni Eq) => GEq (ValueOf uni :: Type -> Type) Source # | |
| GEq (TypeRep :: k -> Type) | |
| GEq ((:~:) a :: k -> Type) | |
| (GEq a, GEq b) => GEq (Product a b :: k -> Type) | |
| (GEq a, GEq b) => GEq (Sum a b :: k -> Type) | |
| GEq ((:~~:) a :: k -> Type) | |
| (GEq a, GEq b) => GEq (a :*: b :: k -> Type) | |
| (GEq f, GEq g) => GEq (f :+: g :: k -> Type) | |
data (a :: k) :~: (b :: k) where infix 4 Source #
Propositional equality. If a :~: b is inhabited by some terminating
value, then the type a is the same as the type b. To use this equality
in practice, pattern-match on the a :~: b to get out the Refl constructor;
in the body of the pattern-match, the compiler knows that a ~ b.
Since: base-4.7.0.0
Instances
| Category ((:~:) :: k -> k -> Type) | Since: base-4.7.0.0 |
| TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
| GNFData ((:~:) a :: k -> Type) | |
Defined in Data.GADT.DeepSeq | |
| GCompare ((:~:) a :: k -> Type) | |
Defined in Data.GADT.Internal | |
| GEq ((:~:) a :: k -> Type) | |
| GRead ((:~:) a :: k -> Type) | |
Defined in Data.GADT.Internal Methods greadsPrec :: Int -> GReadS ((:~:) a) | |
| GShow ((:~:) a :: k -> Type) | |
Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k0). Int -> (a :~: a0) -> ShowS # | |
| NFData2 ((:~:) :: Type -> Type -> Type) | Since: deepseq-1.4.3.0 |
Defined in Control.DeepSeq | |
| NFData1 ((:~:) a) | Since: deepseq-1.4.3.0 |
Defined in Control.DeepSeq | |
| (a ~ b, Data a) => Data (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Data Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~: b) -> c (a :~: b) Source # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b) Source # toConstr :: (a :~: b) -> Constr Source # dataTypeOf :: (a :~: b) -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b)) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b)) Source # gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r Source # gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source # | |
| a ~ b => Bounded (a :~: b) | Since: base-4.7.0.0 |
| a ~ b => Enum (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality Methods succ :: (a :~: b) -> a :~: b Source # pred :: (a :~: b) -> a :~: b Source # toEnum :: Int -> a :~: b Source # fromEnum :: (a :~: b) -> Int Source # enumFrom :: (a :~: b) -> [a :~: b] Source # enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b] Source # enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b] Source # enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b] Source # | |
| a ~ b => Read (a :~: b) | Since: base-4.7.0.0 |
| Show (a :~: b) | Since: base-4.7.0.0 |
| NFData (a :~: b) | Since: deepseq-1.4.3.0 |
Defined in Control.DeepSeq | |
| Eq (a :~: b) | Since: base-4.7.0.0 |
| Ord (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
data DSum (tag :: k -> Type) (f :: k -> Type) #
Constructors
| !(tag a) :=> (f a) |
Instances
| (GRead tag, Has' Read tag f) => Read (DSum tag f) | |
| (GShow tag, Has' Show tag f) => Show (DSum tag f) | |
| (GEq tag, Has' Eq tag f) => Eq (DSum tag f) | |
| (GCompare tag, Has' Eq tag f, Has' Ord tag f) => Ord (DSum tag f) | |
Defined in Data.Dependent.Sum Methods compare :: DSum tag f -> DSum tag f -> Ordering Source # (<) :: DSum tag f -> DSum tag f -> Bool Source # (<=) :: DSum tag f -> DSum tag f -> Bool Source # (>) :: DSum tag f -> DSum tag f -> Bool Source # (>=) :: DSum tag f -> DSum tag f -> Bool Source # | |