- A View of HOL Types
- HOL Light Type Primitives
- Stateless HOL Type Primitives
- HOL2P Type Primitives
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.
- data HOLType
- data HOLTypeView
- data TypeOp
- type HOLTypeEnv = [(HOLType, HOLType)]
- type SubstTrip = (HOLTypeEnv, [(TypeOp, HOLType)], [(TypeOp, TypeOp)])
- tyAlphaOrder :: HOLType -> HOLType -> Ordering
- tyAConv :: HOLType -> HOLType -> Bool
- isVarType :: HOLType -> Bool
- isType :: HOLType -> Bool
- mkVarType :: String -> HOLType
- destVarType :: HOLType -> Maybe String
- destType :: HOLType -> Maybe (TypeOp, [HOLType])
- tyVars :: HOLType -> [HOLType]
- catTyVars :: [HOLType] -> [HOLType]
- class TypeSubst a b
- typeSubst :: TypeSubst a b => [(a, b)] -> HOLType -> HOLType
- typeSubstFull :: SubstTrip -> HOLType -> HOLType
- tyBool :: HOLType
- tyA :: HOLType
- tyB :: HOLType
- destFunTy :: HOLType -> Maybe (HOLType, HOLType)
- typeOf :: HOLTerm -> HOLType
- isTypeOpVar :: TypeOp -> Bool
- newPrimTypeOp :: String -> Int -> TypeOp
- mkTypeOpVar :: String -> TypeOp
- destTypeOp :: TypeOp -> (String, Int)
- tyOpBool :: TypeOp
- tyOpFun :: TypeOp
- tyApp :: TypeOp -> [HOLType] -> Either String HOLType
- typeOpVars :: HOLType -> [TypeOp]
- catTypeOpVars :: [HOLType] -> [TypeOp]
- isUType :: HOLType -> Bool
- isSmall :: HOLType -> Bool
- mkUType :: HOLType -> HOLType -> Either String HOLType
- mkUTypes :: [HOLType] -> HOLType -> Either String HOLType
- uTypeFromTypeOpVar :: TypeOp -> Int -> Either String HOLType
- mkSmall :: HOLType -> Either String HOLType
- destUType :: HOLType -> Maybe (HOLType, HOLType)
- destUTypes :: HOLType -> Maybe ([HOLType], HOLType)
- containsUType :: HOLType -> Bool
- variantTyVar :: [HOLType] -> HOLType -> HOLType
- variantTyVars :: [HOLType] -> [HOLType] -> [HOLType]
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
HOLThmView) are exposed to enable pattern matching.
- View patterns, as defined by instances of the
viewfunction from the
Viewableclass, provide a conversion between the two sets of constructors.
The view pattern data type for HOL types.
|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
|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.
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:
Type synonym for the commonly used, list-based, type environment.
Type synonym for the commonly used triplet of substitution environments.
TypeSubst for more information.
HOL Light Type Primitives
Alpha-Equivalence of Types
Provides an ordering for two types modulo alpha-equivalence.
Predicates, Constructors, and Destructors for Basic Types
Constructs a type variable of a given name. Note that the resultant type variable is unconstrained.
Destructs a type variable, returning its name. Fails with
Nothing if called
on a non-variable type.
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
Type Variable Extractors
Returns the list of all free, type variables in a type, not including type operator variables.
Returns the list of all type variables in a list of types, not including type operator variables.
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,
accepts a triplet of all possible substitution environments that can be
conveniently used in combination with
See the ITP2013 paper, Stateless Higher-Order Logic with Quantified Types, for more details.
Re-exports the internal type substitution function of the
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 version of
typeSubst that accepts a triplet of type substitution
Commonly Used Types and Functions
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
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
Constructs a primitive type operator of a given name and arity. Primitive type operators are used to represent constant, but undefined, types.
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.
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
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
Returns the list of all type operator variables in a list of types.
HOL2P Type Primitives
Predicates, Constructors, and Destructors for Universal Types
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.
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
Left in the following cases:
n<=0which would result in the application of a type operator to an empty list of type arguments.
- The type operator argument is not a variable.
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.
Destructs a universal type, returning its bound type and body type. Fails
Nothing if the provided type is not universally quantified.
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
Predicate to test if a type contains a universal type at any level.
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.