covenant
Copyright(C) MLabs 2025
LicenseApache 2.0
Maintainerkoz@mlabs.city, sean@mlabs.city
Safe HaskellNone
LanguageHaskell2010

Covenant.Type

Description

Covenant's type system and various ways to construct types.

Since: 1.0.0

Synopsis

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', S Z to 'one scope outside our immediate enclosing scope', etc. This can mean different things depending on what these scope(s) are.

Since: 1.0.0

Constructors

BoundAt DeBruijn (Index "tyvar") 

Instances

Instances details
Show AbstractTy Source #

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Type

Eq AbstractTy Source #

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Type

Ord AbstractTy Source #

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Type

data Renamed Source #

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 Rigid; third is the positional index within its scope. We must have unique identifiers for wildcard scopes, as wildcards unify with everything except other wildcards in the same scope, and child scopes aren't unique.

Instances

Instances details
Show Renamed Source #

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Type

Eq Renamed Source #

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Type

Methods

(==) :: Renamed -> Renamed -> Bool #

(/=) :: Renamed -> Renamed -> Bool #

Ord Renamed Source #

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Type

Pretty (CompT Renamed) Source #

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Type

Methods

pretty :: CompT Renamed -> Doc ann #

prettyList :: [CompT Renamed] -> Doc ann #

Pretty (DataDeclaration Renamed) Source #

Since: 1.1.0

Instance details

Defined in Covenant.Internal.Type

Pretty (ValT Renamed) Source #

Do not use this instance to write other Pretty instances. It exists to ensure readable tests without having to expose a lot of internals.

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Type

Methods

pretty :: ValT Renamed -> Doc ann #

prettyList :: [ValT Renamed] -> Doc ann #

Computation types

data CompT a where Source #

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 forall a . ... -> ...). Use this like a data constructor.

Since: 1.0.0

pattern Comp2 :: CompTBody a -> CompT a

A computation type that binds two type variables (that is, something whose type is forall a b . ... -> ...). Use this like a data constructor.

Since: 1.0.0

pattern Comp3 :: CompTBody a -> CompT a

A computation type that binds three type variables (that is, something whose type is forall a b c . ... -> ...). Use this like a data constructor.

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 Comp patterns, CompN is exhaustive if matched on.

Since: 1.0.0

Instances

Instances details
Eq1 CompT Source #

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Type

Methods

liftEq :: (a -> b -> Bool) -> CompT a -> CompT b -> Bool #

Show a => Show (CompT a) Source #

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Type

Methods

showsPrec :: Int -> CompT a -> ShowS #

show :: CompT a -> String #

showList :: [CompT a] -> ShowS #

Eq a => Eq (CompT a) Source #

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Type

Methods

(==) :: CompT a -> CompT a -> Bool #

(/=) :: CompT a -> CompT a -> Bool #

Ord a => Ord (CompT a) Source #

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Type

Methods

compare :: CompT a -> CompT a -> Ordering #

(<) :: CompT a -> CompT a -> Bool #

(<=) :: CompT a -> CompT a -> Bool #

(>) :: CompT a -> CompT a -> Bool #

(>=) :: CompT a -> CompT a -> Bool #

max :: CompT a -> CompT a -> CompT a #

min :: CompT a -> CompT a -> CompT a #

Pretty (CompT Renamed) Source #

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Type

Methods

pretty :: CompT Renamed -> Doc ann #

prettyList :: [CompT Renamed] -> Doc ann #

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.

Example

Since: 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.

Note

Together with ReturnT, these two patterns provide an exhaustive pattern match.

Example

Since: 1.0.0

pattern ArgsAndResult :: Vector (ValT a) -> ValT a -> CompTBody a

A view of a computation type as a Vector of its argument types, together with its result type. Can be used as a data constructor, and is an exhaustive match.

Example

Since: 1.0.0

Instances

Instances details
Eq1 CompTBody Source #

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Type

Methods

liftEq :: (a -> b -> Bool) -> CompTBody a -> CompTBody b -> Bool #

Show a => Show (CompTBody a) Source #

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Type

Eq a => Eq (CompTBody a) Source #

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Type

Methods

(==) :: CompTBody a -> CompTBody a -> Bool #

(/=) :: CompTBody a -> CompTBody a -> Bool #

Ord a => Ord (CompTBody a) Source #

Since: 1.0.0

Instance details

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

data ValT a Source #

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

Instances details
Eq1 ValT Source #

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Type

Methods

liftEq :: (a -> b -> Bool) -> ValT a -> ValT b -> Bool #

Show a => Show (ValT a) Source #

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Type

Methods

showsPrec :: Int -> ValT a -> ShowS #

show :: ValT a -> String #

showList :: [ValT a] -> ShowS #

Eq a => Eq (ValT a) Source #

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Type

Methods

(==) :: ValT a -> ValT a -> Bool #

(/=) :: ValT a -> ValT a -> Bool #

Ord a => Ord (ValT a) Source #

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Type

Methods

compare :: ValT a -> ValT a -> Ordering #

(<) :: ValT a -> ValT a -> Bool #

(<=) :: ValT a -> ValT a -> Bool #

(>) :: ValT a -> ValT a -> Bool #

(>=) :: ValT a -> ValT a -> Bool #

max :: ValT a -> ValT a -> ValT a #

min :: ValT a -> ValT a -> ValT a #

Pretty (ValT Renamed) Source #

Do not use this instance to write other Pretty instances. It exists to ensure readable tests without having to expose a lot of internals.

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Type

Methods

pretty :: ValT Renamed -> Doc ann #

prettyList :: [ValT Renamed] -> Doc ann #

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

byteStringT :: ValT a Source #

Helper for defining the value type of builtin bytestrings.

Since: 1.0.0

integerT :: ValT a Source #

Helper for defining the value type of builtin integers.

Since: 1.0.0

stringT :: ValT a Source #

Helper for defining the value type of builtin strings.

Since: 1.0.0

tyvar :: DeBruijn -> Index "tyvar" -> ValT AbstractTy Source #

Helper for defining type variables.

Since: 1.0.0

boolT :: ValT a Source #

Helper for defining the value type of builtin booleans.

Since: 1.0.0

g1T :: ValT a Source #

Helper for defining the value type of BLS12-381 G1 curve points.

Since: 1.0.0

g2T :: ValT a Source #

Helper for defining the value type of BLS12-381 G2 curve points.

Since: 1.0.0

mlResultT :: ValT a Source #

Helper for defining the value type of BLS12-381 multiplication results.

Since: 1.0.0

unitT :: ValT a Source #

Helper for defining the value type of the builtin unit type.

Since: 1.0.0

Data declarations

newtype TyName Source #

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

Constructors

TyName Text 

Instances

Instances details
IsString TyName Source #

Since: 1.1.0

Instance details

Defined in Covenant.Internal.Type

Methods

fromString :: String -> TyName #

Show TyName Source #

Since: 1.1.0

Instance details

Defined in Covenant.Internal.Type

Eq TyName Source #

Since: 1.1.0

Instance details

Defined in Covenant.Internal.Type

Methods

(==) :: TyName -> TyName -> Bool #

(/=) :: TyName -> TyName -> Bool #

Ord TyName Source #

Since: 1.1.0

Instance details

Defined in Covenant.Internal.Type

data Constructor a Source #

A single constructor of a data type, with its fields.

Since: 1.1.0

Instances

Instances details
Eq1 Constructor Source #

Since: 1.1.0

Instance details

Defined in Covenant.Internal.Type

Methods

liftEq :: (a -> b -> Bool) -> Constructor a -> Constructor b -> Bool #

(k ~ A_Lens, a ~ Vector (ValT c), b ~ Vector (ValT c)) => LabelOptic "constructorArgs" k (Constructor c) (Constructor c) a b Source #

Since: 1.1.0

Instance details

Defined in Covenant.Internal.Type

Methods

labelOptic :: Optic k NoIx (Constructor c) (Constructor c) a b #

(k ~ A_Lens, a ~ ConstructorName, b ~ ConstructorName) => LabelOptic "constructorName" k (Constructor c) (Constructor c) a b Source #

Since: 1.1.0

Instance details

Defined in Covenant.Internal.Type

Methods

labelOptic :: Optic k NoIx (Constructor c) (Constructor c) a b #

Show a => Show (Constructor a) Source #

Since: 1.1.0

Instance details

Defined in Covenant.Internal.Type

Eq a => Eq (Constructor a) Source #

Since: 1.1.0

Instance details

Defined in Covenant.Internal.Type

data PlutusDataStrategy Source #

Specifics of how a Data-encoded datatype is represented.

Since: 1.1.0

Constructors

EnumData

The type is encoded as an Integer, corresponding to which 'arm' of the datatype we want.

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 Constr.

Since: 1.1.0

NewtypeData

The type 'borrows' the encoding of whatever it wraps.

Since: 1.1.0

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 Data, using the specified strategy to determine specifics.

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

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 Data we can use to build and tear it down.

Since: 1.1.0

Instances

Instances details
(k ~ A_Fold, a ~ Count "tyvar", b ~ Count "tyvar") => LabelOptic "datatypeBinders" k (DataDeclaration c) (DataDeclaration c) a b Source #

Since: 1.1.0

Instance details

Defined in Covenant.Internal.Type

(k ~ A_Fold, a ~ Vector (Constructor c), b ~ Vector (Constructor c)) => LabelOptic "datatypeConstructors" k (DataDeclaration c) (DataDeclaration c) a b Source #

Since: 1.1.0

Instance details

Defined in Covenant.Internal.Type

(k ~ A_Lens, a ~ DataEncoding, b ~ DataEncoding) => LabelOptic "datatypeEncoding" k (DataDeclaration c) (DataDeclaration c) a b Source #

Since: 1.1.0

Instance details

Defined in Covenant.Internal.Type

(k ~ A_Lens, a ~ TyName, b ~ TyName) => LabelOptic "datatypeName" k (DataDeclaration c) (DataDeclaration c) a b Source #

Since: 1.1.0

Instance details

Defined in Covenant.Internal.Type

Show a => Show (DataDeclaration a) Source #

Since: 1.1.0

Instance details

Defined in Covenant.Internal.Type

Eq a => Eq (DataDeclaration a) Source #

Since: 1.1.0

Instance details

Defined in Covenant.Internal.Type

Pretty (DataDeclaration Renamed) Source #

Since: 1.1.0

Instance details

Defined in Covenant.Internal.Type