| Safe Haskell | None |
|---|---|
| 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
- someValueOf :: forall a uni. uni ( Esc a) -> a -> Some ( ValueOf uni)
- someValue :: forall a uni. uni `Includes` a => a -> Some ( ValueOf uni)
- someValueType :: Some ( ValueOf uni) -> SomeTypeIn uni
- class Contains uni a where
- type Includes uni = Permits ( Contains 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
- type family EverywhereAll uni constrs where ...
- type (<:) uni1 uni2 = uni1 `Everywhere` Includes uni2
-
class
HasUniApply
(uni ::
Type
->
Type
)
where
- matchUniApply :: uni tb -> r -> ( forall k l (f :: k -> l) a. tb ~ Esc (f a) => uni ( Esc f) -> uni ( Esc a) -> r) -> r
- 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
- knownUniOf :: uni `Contains` a => proxy a -> uni ( Esc a)
-
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
- deriveGEq :: DeriveGEQ t => t -> Q [ Dec ]
- deriveGCompare :: DeriveGCompare t => t -> Q [ Dec ]
- data (a :: k) :~: (b :: k) where
Documentation
data Some (tag :: k -> Type ) where Source #
Existential. This is type is useful to hide GADTs' parameters.
>>>data Tag :: * -> * where TagInt :: Tag Int; TagBool :: Tag Bool>>>instance GShow Tag where gshowsPrec _ TagInt = showString "TagInt"; gshowsPrec _ TagBool = showString "TagBool">>>classify s = case s of "TagInt" -> [mkGReadResult TagInt]; "TagBool" -> [mkGReadResult TagBool]; _ -> []>>>instance GRead Tag where greadsPrec _ s = [ (r, rest) | (con, rest) <- lex s, r <- classify con ]
You can either use
PatternSynonyms
(available with GHC >= 8.0)
>>>let x = Some TagInt>>>xSome TagInt
>>>case x of { Some TagInt -> "I"; Some TagBool -> "B" } :: String"I"
or you can use functions
>>>let y = mkSome TagBool>>>ySome TagBool
>>>withSome y $ \y' -> case y' of { TagInt -> "I"; TagBool -> "B" } :: String"B"
The implementation of
mapSome
is
safe
.
>>>let f :: Tag a -> Tag a; f TagInt = TagInt; f TagBool = TagBool>>>mapSome f ySome TagBool
but you can also use:
>>>withSome y (mkSome . f)Some TagBool
>>>read "Some TagBool" :: Some TagSome TagBool
>>>read "mkSome TagInt" :: Some TagSome TagInt
Instances
| GEq tag => Eq ( Some tag) | |
| GCompare tag => Ord ( Some tag) | |
|
Defined in Data.Some.Newtype |
|
| GRead f => Read ( Some f) | |
| GShow tag => Show ( Some tag) | |
| Applicative m => Semigroup ( Some m) | |
| Applicative m => Monoid ( Some m) | |
| GNFData tag => NFData ( Some tag) | |
|
Defined in Data.Some.Newtype |
|
| ( Closed uni, Everywhere uni Flat ) => Flat ( Some ( ValueOf uni)) Source # | |
| ( Closed uni, Everywhere uni PrettyConst ) => Pretty ( Some ( ValueOf uni)) Source # | |
| ( Closed uni, Everywhere uni ExMemoryUsage ) => ExMemoryUsage ( Some ( ValueOf uni)) Source # | |
|
Defined in PlutusCore.Evaluation.Machine.ExMemory |
|
data SomeTypeIn uni Source #
A particular type from a universe.
Constructors
| forall k (a :: k). SomeTypeIn !(uni ( Esc a)) |
Instances
A value of a particular type from a universe.
Instances
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 `Includes` 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 #
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
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 Int
UList (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.
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
f
s expecting
more type arguments than 3 if you need that.
Note that, say,
constr
elaborates to
Permits
[]
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 Source # | |
|
Defined in Universe.Core
type
Permits
|
|
| type Permits Source # | |
|
Defined in Universe.Core
type
Permits
|
|
| type Permits Source # | |
|
Defined in Universe.Core
type
Permits
|
|
| type Permits Source # | |
|
Defined in Universe.Core
type
Permits
|
|
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
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 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.
knownUniOf :: uni `Contains` a => proxy a -> uni ( Esc a) Source #
Same as
knownUni
, but receives a
proxy
.
class GShow (t :: k -> Type ) where Source #
Show
-like class for 1-type-parameter GADTs.
GShow t => ...
is equivalent to something
like
(forall a. Show (t a)) => ...
. The easiest way to create instances would probably be
to write (or derive) an
instance Show (T a)
, and then simply say:
instance GShow t where gshowsPrec = showsPrec
Methods
gshowsPrec :: forall (a :: k). Int -> t a -> ShowS Source #
Instances
| GShow DefaultUni Source # | |
|
Defined in PlutusCore.Default.Universe Methods gshowsPrec :: forall (a :: k). Int -> DefaultUni a -> ShowS Source # |
|
| ( GShow uni, Closed uni, Everywhere uni Show ) => GShow ( ValueOf uni :: Type -> Type ) Source # | |
|
Defined in Universe.Core |
|
| GShow uni => GShow ( Kinded uni :: Type -> Type ) Source # | |
|
Defined in Universe.Core |
|
| GShow ( TypeRep :: k -> Type ) | |
|
Defined in Data.GADT.Internal |
|
| GShow ( GOrdering a :: k -> Type ) | |
|
Defined in Data.GADT.Internal |
|
| GShow ( (:~:) a :: k -> Type ) | |
|
Defined in Data.GADT.Internal |
|
| ( GShow a, GShow b) => GShow ( Sum a b :: k -> Type ) |
|
|
Defined in Data.GADT.Internal |
|
| ( GShow a, GShow b) => GShow ( Product a b :: k -> Type ) |
|
|
Defined in Data.GADT.Internal |
|
class GEq (f :: k -> Type ) where Source #
A class for type-contexts which contain enough information to (at least in some cases) decide the equality of types occurring within them.
Methods
geq :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b) Source #
Produce a witness of type-equality, if one exists.
A handy idiom for using this would be to pattern-bind in the Maybe monad, eg.:
extract :: GEq tag => tag a -> DSum tag -> Maybe a
extract t1 (t2 :=> x) = do
Refl <- geq t1 t2
return x
Or in a list comprehension:
extractMany :: GEq tag => tag a -> [DSum tag] -> [a] extractMany t1 things = [ x | (t2 :=> x) <- things, Refl <- maybeToList (geq t1 t2)]
(Making use of the
DSum
type from
Data.Dependent.Sum
in both examples)
Instances
| GEq DefaultUni Source # | |
|
Defined in PlutusCore.Default.Universe Methods geq :: forall (a :: k) (b :: k). DefaultUni a -> DefaultUni b -> Maybe (a :~: b) Source # |
|
| ( 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 ( Sum a b :: k -> Type ) | |
| ( GEq a, GEq b) => GEq ( Product a b :: k -> Type ) | |
deriveGCompare :: DeriveGCompare t => t -> Q [ Dec ] Source #
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 |
| Semigroupoid ( (:~:) :: k -> k -> Type ) | |
| TestEquality ( (:~:) a :: k -> Type ) |
Since: base-4.7.0.0 |
|
Defined in Data.Type.Equality |
|
| GShow ( (:~:) a :: k -> Type ) | |
|
Defined in Data.GADT.Internal |
|
| GRead ( (:~:) a :: k -> Type ) | |
|
Defined in Data.GADT.Internal |
|
| GEq ( (:~:) a :: k -> Type ) | |
| GCompare ( (:~:) a :: k -> Type ) | |
| 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 => 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 # |
|
| Eq (a :~: b) |
Since: base-4.7.0.0 |
| (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 # |
|
| Ord (a :~: b) |
Since: base-4.7.0.0 |
|
Defined in Data.Type.Equality Methods compare :: (a :~: b) -> (a :~: b) -> Ordering Source # (<) :: (a :~: b) -> (a :~: b) -> Bool Source # (<=) :: (a :~: b) -> (a :~: b) -> Bool Source # (>) :: (a :~: b) -> (a :~: b) -> Bool Source # (>=) :: (a :~: b) -> (a :~: b) -> Bool 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 |
|