| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
PlutusCore.Builtin.KnownTypeAst
Synopsis
- data TyNameRep (kind ∷ Type) = TyNameRep Symbol Nat
- data family TyVarRep (name ∷ TyNameRep kind) ∷ kind
- data family TyAppRep (fun ∷ dom → cod) (arg ∷ dom) ∷ cod
- data family TyForallRep (name ∷ TyNameRep kind) (a ∷ Type) ∷ Type
- data Hole
- data family RepHole x
- data family TypeHole a
- type family RunHole hole where ...
- type HasTermLevel uni = Includes uni
- type HasTypeLevel uni x = KnownTypeAst Void uni (ElaborateBuiltin uni x)
- type HasTypeAndTermLevel uni x = (uni `HasTypeLevel` x, uni `HasTermLevel` x)
- mkTyBuiltin ∷ ∀ a (x ∷ a) uni ann tyname. uni `HasTypeLevel` x ⇒ ann → Type tyname uni ann
- type KnownBuiltinTypeAst tyname uni x = AllBuiltinArgs uni (KnownTypeAst tyname uni) x
- class KnownTypeAst tyname uni x where
- toTypeAst ∷ ∀ a tyname uni (x ∷ a) proxy. KnownTypeAst tyname uni x ⇒ proxy x → Type tyname uni ()
- type family Insert x xs where ...
- type family Delete x xs where ...
Documentation
data TyNameRep (kind ∷ Type) Source #
Representation of a type variable: its name and unique and an implicit kind.
Instances
data family TyVarRep (name ∷ TyNameRep kind) ∷ kind Source #
Representation of an intrinsically-kinded type variable: a name.
Instances
| (tyname ~ TyName, name ~ ('TyNameRep text uniq ∷ TyNameRep a), KnownSymbol text, KnownNat uniq) ⇒ KnownTypeAst tyname uni (TyVarRep name ∷ a) Source # | |
| (TypeError NoStandalonePolymorphicDataErrMsg ∷ Constraint) ⇒ Contains uni (TyVarRep ∷ TyNameRep kind → kind) Source # | |
| type ToBinds uni acc (TyVarRep name ∷ a) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst | |
| type ToHoles uni _1 (TyVarRep name ∷ a) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst | |
| type IsBuiltin uni (TyVarRep name ∷ a) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst | |
data family TyAppRep (fun ∷ dom → cod) (arg ∷ dom) ∷ cod Source #
Representation of an intrinsically-kinded type application: a function and an argument.
Instances
| (KnownTypeAst tyname uni fun, KnownTypeAst tyname uni arg) ⇒ KnownTypeAst tyname uni (TyAppRep fun arg ∷ a) Source # | |
| type ToBinds uni acc (TyAppRep fun arg ∷ a) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst | |
| type ToHoles uni _1 (TyAppRep fun arg ∷ a) Source # | |
| type IsBuiltin uni (TyAppRep fun arg ∷ a) Source # | |
data family TyForallRep (name ∷ TyNameRep kind) (a ∷ Type) ∷ Type Source #
Representation of of an intrinsically-kinded universal quantifier: a bound name and a body.
Instances
| (tyname ~ TyName, name ~ ('TyNameRep text uniq ∷ TyNameRep kind), KnownSymbol text, KnownNat uniq, KnownKind kind, KnownTypeAst tyname uni a) ⇒ KnownTypeAst tyname uni (TyForallRep name a ∷ Type) Source # | |
| type ToBinds uni acc (TyForallRep name a ∷ Type) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst | |
| type ToHoles uni _1 (TyForallRep name a ∷ Type) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst | |
| type IsBuiltin uni (TyForallRep name a ∷ Type) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst | |
type family RunHole hole where ... Source #
Turn a hole in the GHC.Type -> GHC.Type form into one of the Hole form. This only changes
the kind of the given argument. This is a way of encoding forall a. a -> Hole at the kind
level, which we don't attempt to use, because GHC apparently hates polymorphism at the kind
level and chokes upon encountering it.
type HasTermLevel uni = Includes uni Source #
Specifies that the given type is a built-in one and its values can be embedded into a Term.
type HasTypeLevel uni x = KnownTypeAst Void uni (ElaborateBuiltin uni x) Source #
Specifies that the given type is a built-in one and can be embedded into a Kind.
type HasTypeAndTermLevel uni x = (uni `HasTypeLevel` x, uni `HasTermLevel` x) Source #
The product of HasTypeLevel and HasTermLevel.
mkTyBuiltin ∷ ∀ a (x ∷ a) uni ann tyname. uni `HasTypeLevel` x ⇒ ann → Type tyname uni ann Source #
Convert a Haskell representation of a possibly 0-ary application of a built-in type to
arbitrary types implementing KnownTypeAst.
type KnownBuiltinTypeAst tyname uni x = AllBuiltinArgs uni (KnownTypeAst tyname uni) x Source #
A constraint for "a is a KnownTypeAst by means of being included in uni".
class KnownTypeAst tyname uni x where Source #
This class allows one to convert the type-level Haskell representation of a Plutus type into the corresponding Plutus type. Associated type families are needed to help elaboration.
Depending on the universe converting a Haskell type to a Plutus team can give different results
(e.g. Int can be a built-in type instead of being encoded via built-in Integer), hence this
class takes a uni argument. Plus, elaboration is universe-specific too.
Minimal complete definition
Nothing
Associated Types
type IsBuiltin uni x ∷ Bool Source #
Whether x is a built-in type.
type IsBuiltin uni x = IsBuiltin uni (ElaborateBuiltin uni x)
type ToHoles uni (hole ∷ Type → Type) x ∷ [Hole] Source #
Return every part of the type that can be a to-be-instantiated type variable.
For example, in Integer there's no such types and in (a, b) it's the two arguments
(a and b) and the same applies to a -> b (to mention a type that is not built-in).
Takes a hole in the GHC.Type -> GHC.Type form (a convention originally adopted in the
elaborator, perhaps not a very helpful one), which can be turned into an actual Hole via
RunHole.
type ToHoles uni hole x = ToHoles uni hole (ElaborateBuiltin uni x)
type ToBinds uni (acc ∷ [Some TyNameRep]) x ∷ [Some TyNameRep] Source #
Collect all unique variables (a variable consists of a textual name, a unique and a kind) in an accumulator and return the accumulator once a leaf is reached.
type ToBinds uni acc x = ToBinds uni acc (ElaborateBuiltin uni x)
Methods
typeAst ∷ Type tyname uni () Source #
The Plutus counterpart of the x type.
default typeAst ∷ KnownTypeAst tyname uni (ElaborateBuiltin uni x) ⇒ Type tyname uni () Source #
Instances
toTypeAst ∷ ∀ a tyname uni (x ∷ a) proxy. KnownTypeAst tyname uni x ⇒ proxy x → Type tyname uni () Source #
Return the Plutus counterpart of the x type.