Previous Up Next

9  Typing

Terms in Bedwyr form a strongly typed language with polymorphism and type constructors. This language is statically type-checked; once definition files are loaded and queries are read, types are discarded and the prover handles only untyped terms. Therefore, to ensure that “well-typed formulae don’t go wrong”, a form of the Hindley-Milner type system is used instead of the full System Fω. The polymorphism has therefore those properties:

parametric
type parameters are given as uppercase letters in constant or predicate declarations
predicative
terms are always monomorphic (apart from definitions), so the type parameters of a polymorphic object have to be instantiated with monotypes whenever it is used in a term
prenex
type quantifiers can only occur at the outermost level of a type, and therefore can be omitted

As the language is fairly specific, what we have is not let-polymorphism but “define-polymorphism”: while it is not possible to give a polytype to a bound variable (whether it is bound by an abstraction or a quantifier), a definition can be polymorphic, and must be if the predicate was declared so. With the syntax Bedwyr uses for clauses, this means that the type of the occurence of a predicate at the head of the application that is itself the head of a clause is not instantiated. In ??, the commented out clause wouldn’t type-check as it assumes print? has type option int instead of option A, and the last clause type-checks as println is itself polymorphic and adds no constraints on the type of X.


Listing 9: Polymorphism in Bedwyr.

Kind option type -> type. Type none option A. Type some A -> option A. Define print? : option A -> prop by print? none ; % print? (some 42) ; print? (some X) := println X.

The only two constraints on type parameters are that they must be of kind type, and therefore cannot appear at the head of an type application, and that types must be definite, i.e. a type parameter that appears in a type must appear in the goal of that type, so as to forbid heterogeneous wrappers like Type c A -> t.

Recursive algebraic types are de facto available via constant declarations, e.g. the predeclared type constructor list is morally defined as

list A = nil | (::of (A * list A)

in pseudo-OCaml notation. It is even possible to emulate type deconstruction (matching) by using clause heads that cannot unify simultaneously with a ground term, as is done in ?? with the constants none and some.


Previous Up Next