Safe Haskell	Safe-Inferred
Language	Haskell2010

PlutusCore.Builtin.KnownKind

Synopsis

data SingKind k where
- SingType ∷ SingKind Type
- SingKindArrow ∷ SingKind k → SingKind l → SingKind (k → l)
withSingKind ∷ Kind ann → (∀ k. SingKind k → r) → r
class KnownKind k where
- knownKind ∷ SingKind k
bringKnownKind ∷ SingKind k → (KnownKind k ⇒ r) → r
withKnownKind ∷ Kind ann → (∀ k. KnownKind k ⇒ Proxy k → r) → r
class ToKind (uni ∷ Type → Type) where
- toSingKind ∷ uni (Esc (a ∷ k)) → SingKind k
demoteKind ∷ SingKind k → Kind ()
kindOfBuiltinType ∷ ToKind uni ⇒ uni (Esc a) → Kind ()

Documentation

data SingKind k where Source #

The type of singletonized Haskell kinds representing Plutus kinds. Indexing by a Haskell kind allows us to avoid an error call in the ToKind instance of DefaultUni and not worry about proxies in the type of knownKind.

Constructors

SingType ∷ SingKind Type
SingKindArrow ∷ SingKind k → SingKind l → SingKind (k → l) infixr 5

withSingKind ∷ Kind ann → (∀ k. SingKind k → r) → r Source #

Feed the SingKind version of the given Kind to the given continuation.

class KnownKind k where Source #

For reifying Haskell kinds representing Plutus kinds at the term level.

Methods

knownKind ∷ SingKind k Source #

Instances

Instances details

rep ~ LiftedRep ⇒ KnownKind (TYPE rep) Source #	Plutus only supports lifted types, hence the equality constraint.
Instance details Defined in PlutusCore.Builtin.KnownKind Methods knownKind ∷ SingKind (TYPE rep) Source #
(KnownKind dom, KnownKind cod) ⇒ KnownKind (dom → cod) Source #
Instance details Defined in PlutusCore.Builtin.KnownKind Methods knownKind ∷ SingKind (dom → cod) Source #

bringKnownKind ∷ SingKind k → (KnownKind k ⇒ r) → r Source #

Satisfy the KnownKind constraint of a continuation using the given SingKind.

withKnownKind ∷ Kind ann → (∀ k. KnownKind k ⇒ Proxy k → r) → r Source #

class ToKind (uni ∷ Type → Type) where Source #

For computing the Plutus kind of a built-in type. See kindOfBuiltinType.

Methods

toSingKind ∷ uni (Esc (a ∷ k)) → SingKind k Source #

Reify the kind of a type from the universe at the term level.

Instances

Instances details

ToKind DefaultUni Source #
Instance details Defined in PlutusCore.Default.Universe Methods toSingKind ∷ ∀ k (a ∷ k). DefaultUni (Esc a) → SingKind k Source #

demoteKind ∷ SingKind k → Kind () Source #

Convert a reified Haskell kind to a Plutus kind.

kindOfBuiltinType ∷ ToKind uni ⇒ uni (Esc a) → Kind () Source #

Compute the kind of a type from a universe.