| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
PlutusCore.Builtin.Polymorphism
Synopsis
- newtype Opaque val (rep ∷ Type) = Opaque {
- unOpaque ∷ val
- newtype SomeConstant uni (rep ∷ Type) = SomeConstant {
- unSomeConstant ∷ Some (ValueOf uni)
- 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 family BuiltinHead x
- type family ElaborateBuiltin uni x
- type family AllElaboratedArgs constr x where ...
- class AllElaboratedArgs constr (ElaborateBuiltin uni x) ⇒ AllBuiltinArgs uni constr x
Documentation
newtype Opaque val (rep ∷ Type) Source #
The AST of a value with a Plutus type attached to it. The type is for the Plutus type checker
to look at. Opaque can appear in the type of the denotation of a builtin.
Instances
newtype SomeConstant uni (rep ∷ Type) Source #
For unlifting from the Constant constructor when the stored value is of a monomorphic
built-in type
The rep parameter specifies how the type looks on the PLC side (i.e. just like with
Opaque val rep).
Constructors
| SomeConstant | |
Fields
| |
Instances
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 IsBuiltin uni (TyVarRep name ∷ a) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst | |
| type ToHoles 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 IsBuiltin uni (TyAppRep fun arg ∷ a) Source # | |
| type ToHoles 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 IsBuiltin uni (TyForallRep name a ∷ Type) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst | |
| type ToHoles uni (TyForallRep name a ∷ Type) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst | |
data family BuiltinHead x Source #
For annotating an uninstantiated built-in type, so that it gets handled by the right instance or type family.
Instances
| Contains uni f ⇒ KnownTypeAst tyname uni (BuiltinHead f ∷ a) Source # | |
| type ToBinds uni acc (BuiltinHead f ∷ a) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst | |
| type IsBuiltin uni (BuiltinHead f ∷ a) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst | |
| type ToHoles uni (BuiltinHead f ∷ a) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst | |
type family ElaborateBuiltin uni x Source #
Take an iterated application of a built-in type and elaborate every function application
inside of it to TyAppRep and annotate the head with BuiltinHead.
The idea is that we don't need to process built-in types manually if we simply add some
annotations for instance resolution to look for. Think what we'd have to do manually for, say,
ToHoles: traverse the spine of the application and collect all the holes into a list, which is
troubling, because type applications are left-nested and lists are right-nested, so we'd have to
use accumulators or an explicit Reverse type family. And then we also have KnownTypeAst and
ToBinds, so handling built-in types in a special way for each of those would be a hassle,
especially given the fact that type-level Haskell is not exactly good at computing things.
With the ElaborateBuiltin approach we get KnownTypeAst, ToHoles and ToBinds for free.
We make this an open type family, so that elaboration is customizable for each universe.
Instances
| type ElaborateBuiltin DefaultUni (x ∷ a) Source # | |
Defined in PlutusCore.Default.Universe | |
type family AllElaboratedArgs constr x where ... Source #
Take a constraint and use it to constrain every argument of a possibly 0-ary elaborated application of a built-in type.
Equations
| AllElaboratedArgs constr (f `TyAppRep` x) = (constr x, AllElaboratedArgs constr f) | |
| AllElaboratedArgs _ (BuiltinHead _) = () |
class AllElaboratedArgs constr (ElaborateBuiltin uni x) ⇒ AllBuiltinArgs uni constr x Source #
Take a constraint and use it to constrain every argument of a possibly 0-ary application of a built-in type.
Instances
| AllElaboratedArgs constr (ElaborateBuiltin uni x) ⇒ AllBuiltinArgs uni constr (x ∷ a) Source # | |
Defined in PlutusCore.Builtin.Polymorphism | |