HaskHOL.Core.Kernel.Types

This module exports a safe view of HOL types for HaskHOL. It also defines the primitive functions related to types. For clarity, these functions have been seperated based on their influential system: HOL Light, Stateless HOL, and HOL2P.

Note that, per the stateless approach, any stateful, but still primitive, functions related to types have been relocated to the HaskHOL.Core.State module.

A View of HOL Types

A Quick Note on View Patterns

The primitive data types of HaskHOL are implemented using view patterns in order to simulate private data types:

• Internal constructors are hidden to prevent manual construction of terms.
• View constructors (those of HOLTypeView, HOLTermView, HOLThmView) are exposed to enable pattern matching.
• View patterns, as defined by instances of the view function from the Viewable class, provide a conversion between the two sets of constructors.

data HOLType

The HOLType data type defines the internal constructors for HOL types in HaskHOL. For more details, see the documentation for its view pattern data type, HOLTypeView.

Instances

Eq HOLType

Ord HOLType

Typeable HOLType

NFData HOLType

Lift HOLType

Protected HOLType

TypeSubst TypeOp HOLType

TypeSubst HOLType HOLType

Inst TypeOp HOLType

Inst HOLType HOLType

HOLTypeRep HOLType a

ShowHOL HOLType thry

HOLTypeRep (PType thry) thry

data HOLTypeView

The view pattern data type for HOL types.

Constructors

TyVar Bool String

A type variable consisting of a constraint flag and name.

TyApp TypeOp [HOLType]

A type application consisting of a type operator and a list of type arguments. See TypeOp for more details.

UType HOLType HOLType

A universal type consisting of a bound type and a body type. Note that the bound type must be a small, type variable.

A Quick Note on Type Variable Distinction

In order to keep HaskHOL's type system decidable, we follow the same "smallness" constraint used by HOL2P: type variables that are constrained to be small cannot be replaced with types that contain either universal types or unconstrained type variables. This constraint, in addition to the restriction that universal types can only bind small type variables, prevents the system from performing a substitution that would result in a higher rank type than the system is capable of dealing with. This effectively limits the type system to 2nd order polymorphism.

Voelker elected to rely on syntactic distinction to differentiate between the many kinds of type variables (small, unconstrained, and operator); depending on how it was to be used, the name of a variable was prepended with a special symbol. Internal to HaskHOL, we elected to replace these syntactic distinctions with structural ones such that the following hold true:

• TyVarIn True "x" represents the small type variable "'x"
• TyVarIn False "x" represents the unconstrainted type variable "x"
• TyOpVar "x" represents the type operator variable "_x"

Note that external to HaskHOL, during I/O of terms, both the parser and pretty-printer still rely on the syntactic distinctions introduced by Voelker.

data TypeOp

The data type for type operators, TypeOp, is a mashing together of the representation of type operators from both both HOL2P and Stateless HOL. For more information regarding construction of the different operators, see the documentation of the following functions: mkTypeOpVar, newPrimTypeOp, newDefinedTypeOp

Instances

Eq TypeOp

Ord TypeOp

Show TypeOp

Typeable TypeOp

NFData TypeOp

Lift TypeOp

TypeSubst TypeOp TypeOp

TypeSubst TypeOp HOLType

Inst TypeOp TypeOp

Inst TypeOp HOLType

ShowHOL TypeOp thry

type HOLTypeEnv = [(HOLType, HOLType)]

Type synonym for the commonly used, list-based, type environment.

type SubstTrip = (HOLTypeEnv, [(TypeOp, HOLType)], [(TypeOp, TypeOp)])

Type synonym for the commonly used triplet of substitution environments. See TypeSubst for more information.

HOL Light Type Primitives

Alpha-Equivalence of Types

tyAlphaOrder :: HOLType -> HOLType -> Ordering

Provides an ordering for two types modulo alpha-equivalence.

tyAConv :: HOLType -> HOLType -> Bool

Tests if two types are alpha-equivalent.

Predicates, Constructors, and Destructors for Basic Types

isVarType :: HOLType -> Bool

Predicate for type variables.

isType :: HOLType -> Bool

Predicate for type applications

mkVarType :: String -> HOLType

Constructs a type variable of a given name. Note that the resultant type variable is unconstrained.

destVarType :: HOLType -> Maybe String

Destructs a type variable, returning its name. Fails with Nothing if called on a non-variable type.

destType :: HOLType -> Maybe (TypeOp, [HOLType])

Destructs a type application, returning its operator name and its list of type arguments. Fails with Nothing if called on a type that is not an application.

Type Variable Extractors

tyVars :: HOLType -> [HOLType]

Returns the list of all free, type variables in a type, not including type operator variables.

catTyVars :: [HOLType] -> [HOLType]

Returns the list of all type variables in a list of types, not including type operator variables.

Type Substitution

class TypeSubst a b

The TypeSubst class provides the framework for type substitution in HaskHOL. Note that, with the introduction of universal types and type operator variables, we now have three kinds of substitution to handle:

• Substitution of types for type variables, satisfying type variable constraints.
• Instantiation of type operators with universal types.
• Substitution of type operators for type operator variables.

Rather than have three separate functions exposed to the user, we elected to provide a polymorphic type substitution function that will accept any well-formed, homogenous substitution environment.

Note that the internals of TypeSubst are hidden to prevent unsound re-definition. The relevant type substitution function is re-exported as typeSubst. We also provide a function, typeSubstFull, that accepts a triplet of all possible substitution environments that can be conveniently used in combination with typeMatch.

See the ITP2013 paper, Stateless Higher-Order Logic with Quantified Types, for more details.

Instances

TypeSubst TypeOp TypeOp

TypeSubst TypeOp HOLType

TypeSubst HOLType HOLType

typeSubst :: TypeSubst a b => [(a, b)] -> HOLType -> HOLType

Re-exports the internal type substitution function of the TypeSubst class to prevent unsound re-definition. Invalid substitution pairs are pruned from the environment such that substitution never fails.

Note that the order of elements in a substitution pair follows the convention of most Haskell libraries, rather than the traditional HOL convention:

• The second element is substituted for the first, i.e. the substitution pair (tyA, tyBool) indicates that the boolean type should be substituted for the type variable A.

typeSubstFull :: SubstTrip -> HOLType -> HOLType

A version of typeSubst that accepts a triplet of type substitution environments.

Commonly Used Types and Functions

tyBool :: HOLType

Alias to the primitive boolean type.

tyA :: HOLType

Alias to the unconstrained type variable A.

tyB :: HOLType

Alias to the unconstrained type variable B.

destFunTy :: HOLType -> Maybe (HOLType, HOLType)

Specialized version of destType that returns the domain and range of a function type. Fails with Nothing if the type to be destructed isn't a primitive function type.

typeOf :: HOLTerm -> HOLType

Returns the type of term. Fails with a special type, tyBottom, if the type is poorly constructed; this keeps the function total without requiring the use of an additional guard type like Maybe.

In practice, this type will never be seen provided the kernel is not modified to expose the internal constructors for terms.

Stateless HOL Type Primitives

Predicates, Constructors, and Destructors for Type Operators

isTypeOpVar :: TypeOp -> Bool

Predicate for type operator variables.

newPrimTypeOp :: String -> Int -> TypeOp

Constructs a primitive type operator of a given name and arity. Primitive type operators are used to represent constant, but undefined, types.

mkTypeOpVar :: String -> TypeOp

Constructs a type operator variable of a given name. Note that type operator arities are not stored, only inferred from the context where the operator is used.

The parser makes an attempt to guarantee that all instances of a type operator in a term have the same arity. The same protection is not provided for terms that are manually constructed.

destTypeOp :: TypeOp -> (String, Int)

Destructs a type operator, returning its name and arity. Note that we use -1 to indicate the arity of a type operator variable since that information is not carried.

Commonly Used Type Operators

tyOpBool :: TypeOp

Alias to the primitive boolean type operator.

tyOpFun :: TypeOp

Alias to the primitive function type operator.

tyApp :: TypeOp -> [HOLType] -> Either String HOLType

Constructs a type application from a provided type operator and list of type arguments. Fails with Left in the following cases:

• A type operator variable is applied to zero arguments.
• A type operator's arity disagrees with the length of the argument list.

Type Operator Variable Extractors

typeOpVars :: HOLType -> [TypeOp]

Returns the list of all type operator variables in a type.

catTypeOpVars :: [HOLType] -> [TypeOp]

Returns the list of all type operator variables in a list of types.

HOL2P Type Primitives

Predicates, Constructors, and Destructors for Universal Types

isUType :: HOLType -> Bool

Predicate for universal types.

isSmall :: HOLType -> Bool

Predicate for small types. Returns True if all type variables in the type are constrained to be small and the type contains no universal types; returns False otherwise.

mkUType :: HOLType -> HOLType -> Either String HOLType

Constructs a universal type of a given bound type and body type. Fails with Left if the bound type is not a small, type variable.

mkUTypes :: [HOLType] -> HOLType -> Either String HOLType

Constructs a compound universal type given a list of bound types and a body. Fails with Left if any internal call to mkUType fails.

uTypeFromTypeOpVar :: TypeOp -> Int -> Either String HOLType

Constructs a compound universal type from a type operator variable and a given number of bound variables, i.e.

 uTypeFromTypeOpVar _T n === % 'A1 ... 'An. ('A1, ..., 'An)_T  

Fails with Left in the following cases:

• n<=0 which would result in the application of a type operator to an empty list of type arguments.
• The type operator argument is not a variable.

mkSmall :: HOLType -> Either String HOLType

Constructs a small type from a given type by constraining all of the type variables in the type to be small. Fails with Left if the type contains any universal types.

destUType :: HOLType -> Maybe (HOLType, HOLType)

Destructs a universal type, returning its bound type and body type. Fails with Nothing if the provided type is not universally quantified.

destUTypes :: HOLType -> Maybe ([HOLType], HOLType)

Destructs a compound universal type, returning the list of bound variables and the final body type. Fails if the provided type is not universally quantified.

Commonly Used Functions

containsUType :: HOLType -> Bool

Predicate to test if a type contains a universal type at any level.

variantTyVar :: [HOLType] -> HOLType -> HOLType

Renames a type variable to avoid sharing a name with any of a given list of type variables. Note that this function is both smallness presserving and respecting. Returns the original type if it's not a type variable.

variantTyVars :: [HOLType] -> [HOLType] -> [HOLType]

Renames a list of type variables to avoid sharing a name with any of a given list of type variables. As each type variable is processed it is added to the list of avoids such that the resultant list of type variables are all uniquely named.