Copyright	(C) MLabs 2025
License	Apache 2.0
Maintainer	koz@mlabs.city, sean@mlabs.city
Safe Haskell	None
Language	Haskell2010

Covenant.Type

Contents

Type abstractions
Computation types
Value types
Renaming
Type application

Description

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

Since: 1.0.0

Synopsis

data AbstractTy = BoundAt DeBruijn (Index "tyvar")
data Renamed
- = Rigid Int (Index "tyvar")
- | Unifiable (Index "tyvar")
- | Wildcard Word64 Int (Index "tyvar")
data CompT a where
- pattern Comp0 :: CompTBody a -> CompT a
- pattern Comp1 :: CompTBody a -> CompT a
- pattern Comp2 :: CompTBody a -> CompT a
- pattern Comp3 :: CompTBody a -> CompT a
- pattern CompN :: Count "tyvar" -> CompTBody AbstractTy -> CompT AbstractTy
data CompTBody a where
- pattern ReturnT :: ValT a -> CompTBody a
- pattern (:--:>) :: ValT a -> CompTBody a -> CompTBody a
- pattern ArgsAndResult :: Vector (ValT a) -> ValT a -> CompTBody a
arity :: CompT a -> Int
data ValT a
- = Abstraction a
- | ThunkT (CompT a)
- | BuiltinFlat BuiltinFlatT
data BuiltinFlatT
- = UnitT
- | BoolT
- | IntegerT
- | StringT
- | ByteStringT
- | BLS12_381_G1_ElementT
- | BLS12_381_G2_ElementT
- | BLS12_381_MlResultT
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
data RenameError
- = InvalidAbstractionReference Int (Index "tyvar")
- | IrrelevantAbstraction
- | UndeterminedAbstraction
data RenameM a
renameValT :: ValT AbstractTy -> RenameM (ValT Renamed)
renameCompT :: CompT AbstractTy -> RenameM (CompT Renamed)
runRenameM :: RenameM a -> Either RenameError a
data TypeAppError
- = LeakingUnifiable (Index "tyvar")
- | LeakingWildcard Word64 Int (Index "tyvar")
- | ExcessArgs (CompT Renamed) (Vector (Maybe (ValT Renamed)))
- | InsufficientArgs (CompT Renamed)
- | DoesNotUnify (ValT Renamed) (ValT Renamed)
checkApp :: CompT Renamed -> [Maybe (ValT Renamed)] -> Either TypeAppError (ValT Renamed)

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 Methods showsPrec :: Int -> AbstractTy -> ShowS # show :: AbstractTy -> String # showList :: [AbstractTy] -> ShowS #
Eq AbstractTy Source #	Since: 1.0.0
Instance details Defined in Covenant.Internal.Type Methods (==) :: AbstractTy -> AbstractTy -> Bool # (/=) :: AbstractTy -> AbstractTy -> Bool #
Ord AbstractTy Source #	Since: 1.0.0
Instance details 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 #

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 Methods showsPrec :: Int -> Renamed -> ShowS # show :: Renamed -> String # showList :: [Renamed] -> ShowS #
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 Methods compare :: Renamed -> Renamed -> Ordering # (<) :: Renamed -> Renamed -> Bool # (<=) :: Renamed -> Renamed -> Bool # (>) :: Renamed -> Renamed -> Bool # (>=) :: Renamed -> Renamed -> Bool # max :: Renamed -> Renamed -> Renamed # min :: Renamed -> Renamed -> Renamed #
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 #

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

ReturnT integerT is !Integer

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

integerT :--:> ReturnT byteStringT is Integer -> !ByteString

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

ArgsAndResult (fromList [integerT, integerT]) integerT is Integer -> Integer -> !Integer

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 Methods showsPrec :: Int -> CompTBody a -> ShowS # show :: CompTBody a -> String # showList :: [CompTBody a] -> ShowS #
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 Methods compare :: CompTBody a -> CompTBody a -> Ordering # (<) :: CompTBody a -> CompTBody a -> Bool # (<=) :: CompTBody a -> CompTBody a -> Bool # (>) :: CompTBody a -> CompTBody a -> Bool # (>=) :: CompTBody a -> CompTBody a -> Bool # max :: CompTBody a -> CompTBody a -> CompTBody a # min :: CompTBody a -> CompTBody a -> CompTBody a #

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.

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 #

data BuiltinFlatT Source #

All builtin types that are 'flat': that is, do not have other types 'nested inside them'.

Constructors

UnitT
BoolT
IntegerT
StringT
ByteStringT
BLS12_381_G1_ElementT
BLS12_381_G2_ElementT
BLS12_381_MlResultT

Instances

Instances details

Show BuiltinFlatT Source #	Since: 1.0.0
Instance details Defined in Covenant.Internal.Type Methods showsPrec :: Int -> BuiltinFlatT -> ShowS # show :: BuiltinFlatT -> String # showList :: [BuiltinFlatT] -> ShowS #
Eq BuiltinFlatT Source #	Since: 1.0.0
Instance details Defined in Covenant.Internal.Type Methods (==) :: BuiltinFlatT -> BuiltinFlatT -> Bool # (/=) :: BuiltinFlatT -> BuiltinFlatT -> Bool #
Ord BuiltinFlatT Source #	Since: 1.0.0
Instance details 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

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

Renaming

Types

data RenameError Source #

Ways in which the renamer can fail.

Since: 1.0.0

Constructors

InvalidAbstractionReference Int (Index "tyvar")

An attempt to reference an abstraction in a scope where this abstraction doesn't exist. First field is the true level, second is the index that was requested.

Since: 1.0.0

IrrelevantAbstraction

A value type specifies an abstraction that never gets used anywhere. For example, the type forall a b . [a] has b irrelevant.

Since: 1.0.0

UndeterminedAbstraction

A computation type specifies an abstraction which is not used by any argument. For example, the type forall a b . a -> !(b -> !a) has b undetermined.

Since: 1.0.0

Instances

Instances details

Show RenameError Source #
Instance details Defined in Covenant.Internal.Rename Methods showsPrec :: Int -> RenameError -> ShowS # show :: RenameError -> String # showList :: [RenameError] -> ShowS #
Eq RenameError Source #
Instance details Defined in Covenant.Internal.Rename Methods (==) :: RenameError -> RenameError -> Bool # (/=) :: RenameError -> RenameError -> Bool #

data RenameM a Source #

A 'renaming monad' which allows us to convert type representations from ones that use relative abstraction labelling to absolute abstraction labelling.

Why this is necessary

Consider the following AbstractTy: BoundAtScope 1 0. The meaning of this is relative to where in a type it is positioned: it could be bound by a scope higher than our own, or something we can unify with. Because its meaning (namely, what it refers to) is situational, type checking becomes more difficult, although it has other advantages.

This monad allows us to convert this relative form into an absolute one. More specifically, the renamer does two things:

Ensures that any given abstraction refers to one, and only one, thing; and
Indicates which abstractions are unifiable, and which are (effectively) constant or fixed.

Since: 1.0.0

Instances

Instances details

Applicative RenameM Source #	Since: 1.0.0
Instance details Defined in Covenant.Internal.Rename Methods pure :: a -> RenameM a # (<>) :: RenameM (a -> b) -> RenameM a -> RenameM b # liftA2 :: (a -> b -> c) -> RenameM a -> RenameM b -> RenameM c # (>) :: RenameM a -> RenameM b -> RenameM b # (<*) :: RenameM a -> RenameM b -> RenameM a #
Functor RenameM Source #	Since: 1.0.0
Instance details Defined in Covenant.Internal.Rename Methods fmap :: (a -> b) -> RenameM a -> RenameM b # (<$) :: a -> RenameM b -> RenameM a #
Monad RenameM Source #	Since: 1.0.0
Instance details Defined in Covenant.Internal.Rename Methods (>>=) :: RenameM a -> (a -> RenameM b) -> RenameM b # (>>) :: RenameM a -> RenameM b -> RenameM b # return :: a -> RenameM a #

Introduction

renameValT :: ValT AbstractTy -> RenameM (ValT Renamed) Source #

Rename a value type.

Since: 1.0.0

renameCompT :: CompT AbstractTy -> RenameM (CompT Renamed) Source #

Rename a computation type.

Since: 1.0.0

Elimination

runRenameM :: RenameM a -> Either RenameError a Source #

Execute a renaming computation.

Since: 1.0.0

Type application

data TypeAppError Source #

Since: 1.0.0

Constructors

LeakingUnifiable (Index "tyvar")	The final type after all arguments are applied is `forall a . a`.
LeakingWildcard Word64 Int (Index "tyvar")	A wildcard (thus, a skolem) escaped its scope.
ExcessArgs (CompT Renamed) (Vector (Maybe (ValT Renamed)))	We were given too many arguments.
InsufficientArgs (CompT Renamed)	We weren't given enough arguments.
DoesNotUnify (ValT Renamed) (ValT Renamed)	The expected type (first field) and actual type (second field) do not unify.

Instances

Instances details

Show TypeAppError Source #	Since: 1.0.0
Instance details Defined in Covenant.Internal.Unification Methods showsPrec :: Int -> TypeAppError -> ShowS # show :: TypeAppError -> String # showList :: [TypeAppError] -> ShowS #
Eq TypeAppError Source #	Since: 1.0.0
Instance details Defined in Covenant.Internal.Unification Methods (==) :: TypeAppError -> TypeAppError -> Bool # (/=) :: TypeAppError -> TypeAppError -> Bool #

checkApp :: CompT Renamed -> [Maybe (ValT Renamed)] -> Either TypeAppError (ValT Renamed) Source #

Since: 1.0.0