Copyright | (C) MLabs 2025 |
---|---|
License | Apache 2.0 |
Maintainer | koz@mlabs.city, sean@mlabs.city |
Safe Haskell | None |
Language | Haskell2010 |
Covenant.Type
Description
Covenant's type system and various ways to construct types.
Since: 1.0.0
Synopsis
- data AbstractTy = BoundAt DeBruijn (Index "tyvar")
- data Renamed
- data CompT a where
- data CompTBody a where
- arity :: CompT a -> Int
- data ValT a
- = Abstraction a
- | ThunkT (CompT a)
- | BuiltinFlat BuiltinFlatT
- | Datatype TyName (Vector (ValT a))
- dataTypeT :: TyName -> ValT a
- dataType1T :: TyName -> ValT AbstractTy -> ValT AbstractTy
- dataType2T :: TyName -> ValT AbstractTy -> ValT AbstractTy -> ValT AbstractTy
- data BuiltinFlatT
- byteStringT :: ValT a
- integerT :: ValT a
- stringT :: ValT a
- tyvar :: DeBruijn -> Index "tyvar" -> ValT AbstractTy
- boolT :: ValT a
- g1T :: ValT a
- g2T :: ValT a
- mlResultT :: ValT a
- unitT :: ValT a
- newtype TyName = TyName Text
- newtype ConstructorName = ConstructorName Text
- data Constructor a = Constructor ConstructorName (Vector (ValT a))
- data PlutusDataStrategy
- data DataEncoding
- = SOP
- | PlutusData PlutusDataStrategy
- | BuiltinStrategy InternalStrategy
- data PlutusDataConstructor
- data DataDeclaration a
- = DataDeclaration TyName (Count "tyvar") (Vector (Constructor a)) DataEncoding
- | OpaqueData TyName (Set PlutusDataConstructor)
Type abstractions
data AbstractTy Source #
A type abstraction, using a combination of a DeBruijn index (to indicate which scope it refers to) and a positional index (to indicate which bound variable in that scope it refers to).
Important note
This is a relative representation: any given AbstractTy
could refer to
different things when placed in different positions in the ASG. This stems
from how DeBruijn indices behave: Z
refers to 'our immediate enclosing
scope',
to 'one scope outside our immediate enclosing scope',
etc. This can mean different things depending on what these scope(s) are.S
Z
Since: 1.0.0
Instances
Show AbstractTy Source # | Since: 1.0.0 |
Defined in Covenant.Internal.Type Methods showsPrec :: Int -> AbstractTy -> ShowS # show :: AbstractTy -> String # showList :: [AbstractTy] -> ShowS # | |
Eq AbstractTy Source # | Since: 1.0.0 |
Defined in Covenant.Internal.Type | |
Ord AbstractTy Source # | Since: 1.0.0 |
Defined in Covenant.Internal.Type Methods compare :: AbstractTy -> AbstractTy -> Ordering # (<) :: AbstractTy -> AbstractTy -> Bool # (<=) :: AbstractTy -> AbstractTy -> Bool # (>) :: AbstractTy -> AbstractTy -> Bool # (>=) :: AbstractTy -> AbstractTy -> Bool # max :: AbstractTy -> AbstractTy -> AbstractTy # min :: AbstractTy -> AbstractTy -> AbstractTy # |
A type abstraction that has undergone renaming from a specific context.
Since: 1.0.0
Constructors
Rigid Int (Index "tyvar") | Set by an enclosing scope, and thus is essentially a concrete type, we just don't know which. First field is its 'true level', second field is the positional index in that scope. |
Unifiable (Index "tyvar") | Can be unified with something, but must be consistent: that is, only one unification for every instance. Field is this variable's positional index; we don't need to track the scope, as only one scope contains unifiable bindings. |
Wildcard Word64 Int (Index "tyvar") | Must unify with everything, except with other distinct wildcards in the
same scope. First field is a unique scope identifier; second is its
'true level' simialr to |
Instances
Show Renamed Source # | Since: 1.0.0 |
Eq Renamed Source # | Since: 1.0.0 |
Ord Renamed Source # | Since: 1.0.0 |
Defined in Covenant.Internal.Type | |
Pretty (CompT Renamed) Source # | Since: 1.0.0 |
Pretty (DataDeclaration Renamed) Source # | Since: 1.1.0 |
Defined in Covenant.Internal.Type Methods pretty :: DataDeclaration Renamed -> Doc ann # prettyList :: [DataDeclaration Renamed] -> Doc ann # | |
Pretty (ValT Renamed) Source # | Do not use this instance to write other Since: 1.0.0 |
Computation types
A computation type, with abstractions indicated by the type argument. In
pretty much any case imaginable, this would be either AbstractTy
(in the
ASG), or Renamed
(after renaming).
Since: 1.0.0
Bundled Patterns
pattern Comp0 :: CompTBody a -> CompT a | A computation type that does not bind any type variables. Use this like a data constructor. Since: 1.0.0 |
pattern Comp1 :: CompTBody a -> CompT a | A computation type that binds one type variable (that
is, something whose type is Since: 1.0.0 |
pattern Comp2 :: CompTBody a -> CompT a | A computation type that binds two type variables (that
is, something whose type is Since: 1.0.0 |
pattern Comp3 :: CompTBody a -> CompT a | A computation type that binds three type variables
(that is, something whose type is Since: 1.0.0 |
pattern CompN :: Count "tyvar" -> CompTBody AbstractTy -> CompT AbstractTy | A general way to construct and deconstruct computations which bind an
arbitrary number of type variables. Use this like a data constructor. Unlike
the other Since: 1.0.0 |
data CompTBody a where Source #
The 'body' of a computation type, consisting of the types of its arguments and the type of its result.
Since: 1.0.0
Bundled Patterns
pattern ReturnT :: ValT a -> CompTBody a | The body of a computation type that doesn't take any arguments and produces the a result of the given value type. Use this just as you would a data constructor. ExampleSince: 1.0.0 |
pattern (:--:>) :: ValT a -> CompTBody a -> CompTBody a infixr 1 | Given a type of argument, and the body of another computation type, construct a copy of the body, adding an extra argument of the argument type. Use this just as you would a data constructor. NoteTogether with Example
Since: 1.0.0 |
pattern ArgsAndResult :: Vector (ValT a) -> ValT a -> CompTBody a | A view of a computation type as a Example
Since: 1.0.0 |
Instances
Eq1 CompTBody Source # | Since: 1.0.0 |
Show a => Show (CompTBody a) Source # | Since: 1.0.0 |
Eq a => Eq (CompTBody a) Source # | Since: 1.0.0 |
Ord a => Ord (CompTBody a) Source # | Since: 1.0.0 |
Defined in Covenant.Internal.Type |
arity :: CompT a -> Int Source #
Determine the arity of a computation type: that is, how many arguments a function of this type must be given.
Since: 1.0.0
Value types
A value type, with abstractions indicated by the type argument. In pretty
much any case imaginable, this would be either AbstractTy
(in the ASG) or
Renamed
(after renaming).
Since: 1.0.0
Constructors
Abstraction a | An abstract type. |
ThunkT (CompT a) | A suspended computation. |
BuiltinFlat BuiltinFlatT | A builtin type without any nesting. |
Datatype TyName (Vector (ValT a)) | An applied type constructor for a non-'flat' data type. | @since 1.1.0 |
Instances
Eq1 ValT Source # | Since: 1.0.0 |
Show a => Show (ValT a) Source # | Since: 1.0.0 |
Eq a => Eq (ValT a) Source # | Since: 1.0.0 |
Ord a => Ord (ValT a) Source # | Since: 1.0.0 |
Pretty (ValT Renamed) Source # | Do not use this instance to write other Since: 1.0.0 |
dataTypeT :: TyName -> ValT a Source #
Helper for referring to compound data types with no type variables.
Since: 1.1.0
dataType1T :: TyName -> ValT AbstractTy -> ValT AbstractTy Source #
Helper for referring to compound data types with one type variable.
Since: 1.1.0
dataType2T :: TyName -> ValT AbstractTy -> ValT AbstractTy -> ValT AbstractTy Source #
Helper for referring to compound data types with two type variables.
Since: 1.1.0
data BuiltinFlatT Source #
All builtin types that are 'flat': that is, do not have other types 'nested inside them'.
Since: 1.0.0
Constructors
UnitT | |
BoolT | |
IntegerT | |
StringT | |
ByteStringT | |
BLS12_381_G1_ElementT | |
BLS12_381_G2_ElementT | |
BLS12_381_MlResultT |
Instances
Show BuiltinFlatT Source # | Since: 1.0.0 |
Defined in Covenant.Internal.Type Methods showsPrec :: Int -> BuiltinFlatT -> ShowS # show :: BuiltinFlatT -> String # showList :: [BuiltinFlatT] -> ShowS # | |
Eq BuiltinFlatT Source # | Since: 1.0.0 |
Defined in Covenant.Internal.Type | |
Ord BuiltinFlatT Source # | Since: 1.0.0 |
Defined in Covenant.Internal.Type Methods compare :: BuiltinFlatT -> BuiltinFlatT -> Ordering # (<) :: BuiltinFlatT -> BuiltinFlatT -> Bool # (<=) :: BuiltinFlatT -> BuiltinFlatT -> Bool # (>) :: BuiltinFlatT -> BuiltinFlatT -> Bool # (>=) :: BuiltinFlatT -> BuiltinFlatT -> Bool # max :: BuiltinFlatT -> BuiltinFlatT -> BuiltinFlatT # min :: BuiltinFlatT -> BuiltinFlatT -> BuiltinFlatT # |
byteStringT :: ValT a Source #
Helper for defining the value type of builtin bytestrings.
Since: 1.0.0
tyvar :: DeBruijn -> Index "tyvar" -> ValT AbstractTy Source #
Helper for defining type variables.
Since: 1.0.0
Helper for defining the value type of BLS12-381 multiplication results.
Since: 1.0.0
Data declarations
The name of a data type. This refers specifically to non-'flat' types either provided by the ledger, or defined by the user.
Since: 1.1.0
newtype ConstructorName Source #
The name of a data type constructor.
Since: 1.1.0
Constructors
ConstructorName Text |
Instances
IsString ConstructorName Source # | Since: 1.1.0 |
Defined in Covenant.Internal.Type Methods fromString :: String -> ConstructorName # | |
Show ConstructorName Source # | Since: 1.1.0 |
Defined in Covenant.Internal.Type Methods showsPrec :: Int -> ConstructorName -> ShowS # show :: ConstructorName -> String # showList :: [ConstructorName] -> ShowS # | |
Eq ConstructorName Source # | Since: 1.1.0 |
Defined in Covenant.Internal.Type Methods (==) :: ConstructorName -> ConstructorName -> Bool # (/=) :: ConstructorName -> ConstructorName -> Bool # | |
Ord ConstructorName Source # | Since: 1.1.0 |
Defined in Covenant.Internal.Type Methods compare :: ConstructorName -> ConstructorName -> Ordering # (<) :: ConstructorName -> ConstructorName -> Bool # (<=) :: ConstructorName -> ConstructorName -> Bool # (>) :: ConstructorName -> ConstructorName -> Bool # (>=) :: ConstructorName -> ConstructorName -> Bool # max :: ConstructorName -> ConstructorName -> ConstructorName # min :: ConstructorName -> ConstructorName -> ConstructorName # |
data Constructor a Source #
A single constructor of a data type, with its fields.
Since: 1.1.0
Constructors
Constructor ConstructorName (Vector (ValT a)) |
Instances
data PlutusDataStrategy Source #
Specifics of how a Data
-encoded datatype is represented.
Since: 1.1.0
Constructors
EnumData | The type is encoded as an Since: 1.1.0 |
ProductListData | The type is encoded as a list of its fields. Since: 1.1.0 |
ConstrData | The type is encoded using Since: 1.1.0 |
NewtypeData | The type 'borrows' the encoding of whatever it wraps. Since: 1.1.0 |
Instances
Show PlutusDataStrategy Source # | Since: 1.1.0 |
Defined in Covenant.Internal.Strategy Methods showsPrec :: Int -> PlutusDataStrategy -> ShowS # show :: PlutusDataStrategy -> String # showList :: [PlutusDataStrategy] -> ShowS # | |
Eq PlutusDataStrategy Source # | Since: 1.1.0 |
Defined in Covenant.Internal.Strategy Methods (==) :: PlutusDataStrategy -> PlutusDataStrategy -> Bool # (/=) :: PlutusDataStrategy -> PlutusDataStrategy -> Bool # | |
Ord PlutusDataStrategy Source # | Since: 1.1.0 |
Defined in Covenant.Internal.Strategy Methods compare :: PlutusDataStrategy -> PlutusDataStrategy -> Ordering # (<) :: PlutusDataStrategy -> PlutusDataStrategy -> Bool # (<=) :: PlutusDataStrategy -> PlutusDataStrategy -> Bool # (>) :: PlutusDataStrategy -> PlutusDataStrategy -> Bool # (>=) :: PlutusDataStrategy -> PlutusDataStrategy -> Bool # max :: PlutusDataStrategy -> PlutusDataStrategy -> PlutusDataStrategy # min :: PlutusDataStrategy -> PlutusDataStrategy -> PlutusDataStrategy # |
data DataEncoding Source #
Describes how a datatype is represented onchain.
Since: 1.1.0
Constructors
SOP | The datatype is represented using the SOP primitives. Since: 1.1.0 |
PlutusData PlutusDataStrategy | The datatype is represented as Since: 1.1.0 |
BuiltinStrategy InternalStrategy | The type uses one of the builtin 'special' strategies. This is used only for specific types and isn't generally available for use. Since: 1.1.0 |
Instances
Show DataEncoding Source # | Since: 1.1.0 |
Defined in Covenant.Internal.Strategy Methods showsPrec :: Int -> DataEncoding -> ShowS # show :: DataEncoding -> String # showList :: [DataEncoding] -> ShowS # | |
Eq DataEncoding Source # | Since: 1.1.0 |
Defined in Covenant.Internal.Strategy | |
Ord DataEncoding Source # | Since: 1.1.0 |
Defined in Covenant.Internal.Strategy Methods compare :: DataEncoding -> DataEncoding -> Ordering # (<) :: DataEncoding -> DataEncoding -> Bool # (<=) :: DataEncoding -> DataEncoding -> Bool # (>) :: DataEncoding -> DataEncoding -> Bool # (>=) :: DataEncoding -> DataEncoding -> Bool # max :: DataEncoding -> DataEncoding -> DataEncoding # min :: DataEncoding -> DataEncoding -> DataEncoding # |
data PlutusDataConstructor Source #
The constructors of the onchain Data
type. Needed for other definitions
here.
Since: 1.1.0
Constructors
PlutusI | |
PlutusB | |
PlutusConstr | |
PlutusList | |
PlutusMap |
Instances
data DataDeclaration a Source #
Description of a non-'flat' type, together with how it is encoded.
Since: 1.1.0
Constructors
DataDeclaration TyName (Count "tyvar") (Vector (Constructor a)) DataEncoding | A 'standard' datatype, with its constructors and encoding. Since: 1.1.0 |
OpaqueData TyName (Set PlutusDataConstructor) | An 'opaque' datatype, with the permitted constructors of
Since: 1.1.0 |