Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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
- data family LastArg x y
- 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
).
SomeConstant | |
|
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 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 |
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 ToHoles uni _1 (BuiltinHead f ∷ a) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst | |
type IsBuiltin uni (BuiltinHead f ∷ a) Source # | |
Defined in PlutusCore.Builtin.KnownTypeAst |
data family LastArg x y Source #
LastArg x y
is the same thing as y
in the signature of the denotation of a built-in
functions and this type is only used for referencing x
before y
, so that the elaboration
machinery generates x
before y
in the all
part of the Plutus signature of the builtin.
This is a very hacky and indirect way of specifying the ordering of type variables in a Plutus
signature, in future we'll do it explicitly by introducing a Forall
binder for use in type
signatures of denotations of builtins.
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.
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 |