%
' as in the example
Monoid : Category == BasicType with { * : (%,%) -> %; 1 : %; }This states that for a structure over a type `
%
'
to be a monoid it has to supply two
bindings; in other words a Category
describes a signature.
The first name in the signature is `*
' and is a binary operation
over the type `%
'; the second is an element of `%
'.
Implementations of a category are only accessible by means of the operations
of the signature, and so are very much like abstract data types.
vectorSum : (n:Integer)->Vector(n)->DoubleWhen
vectorSum
is applied, the type of its result depends upon
the value of its argument, so that, for example, the application
vectorSum(42)
is a function expecting an argument of type
Vector(42)
.
Type
is itself a type and so
the system allows
functions over types, such as the function which taking a type ty
to
a type of queues over ty
, say, or a type of fields F
to the category
of vector spaces over F
.
In the last fifteen years a number of theorem proving systems - including Lego, Coq and others - have been designed to exploit the Curry-Howard correspondence between logic and programming. Under this correspondence, logical propositions can be seen as types, and proofs can be seen as members of these types. Central to this correspondence are dependent types, which allow the representation of predicates and quantification. A summary of the correspondence follows.
Programming | Logic | |
Type | Formula | |
Program | Proof | |
Product/record | (...,...) | Conjunction |
Sum/union | ...\/... | Disjunction |
Function type | ...->... | Implication |
Dependent function type | (x:A)->B(x) | Universal formula |
Dependent product type | (x:A,B(x)) | Existential formula |
Empty type | Exit | Contradiction |
One element type | Triv | True proposition |
lessThan(n:Nat,m:Nat) : Type == if m=0 then Exit else (if n=0 then Triv else lessThan(n-1,m-1));We discuss other possible approaches below.
If we identify propositions with types, then the process of proof becomes one of
defining the appropriate functions (or other values) which represent proofs, so that a
proof of the transitivity of lessThan
will be an expression of type
(n:Nat,m:Nat,k:Nat) -> lessThan(n,m) -> lessThan(m,k) -> lessThan(n,k)
We have shown that Axiom/Aldor has a complex type system with dependent types, and that dependent types have been used to represent logics in various theorem proving systems. We therefore propose to use the type system of Axiom/Aldor to represent a logic.
In order for this to operate successfully, we will need to make
modifications to the implementation of dependent types in Axiom/Aldor, as we outline now.
Consider the lessThan
predicate defined (in Axiom/Aldor) earlier,
and suppose that we form the expression lessThan(9,3)
, which
represents the proposition `9<3'; we expect this to be manifestly
false, and evaluating the expression will indeed lead to Exit
,
the type which is uninhabited, and which thus contains no proofs of
`9<3'. Unfortunately, as Axiom/Aldor is currently implemented, there is no
evaluation of Type
expressions, and so any proposition formed in
the same way as lessThan(9,3)
will remain unevaluated. In order
to integrate a logic we need to incorporate evaluation of type
expressions into Axiom/Aldor.
A second approach to defining predicates introduces a predicate inductively as a generalisation of the algebraic types like list and trees which appear in modern functional languages like Haskell and SML.
We might define the
less than predicate `<
' of type Nat -> Nat -> Type
by saying that there are two
constructors - axioms, that is - for the type of the following signature
ZeroLess : (n:Nat) -> (O < S n) SuccLess : (m:Nat) -> (n:Nat) -> ((m < n) -> (S m < S n))
This approach leads to a powerful style of proof which has been used extensively in the type theory community, see, for instance, Paulin's work.
It is possible to write in Axiom/Aldor expressions whose evaluation
fails to terminate; if one of these appears as part of a Type
expression then a type checker evaluating such expressions will not
terminate.
In type theory systems such as Lego, the definition mechanism is such that only
terminating functions can be defined. There is also a body
of work on defining terminating sub-languages of existing programming
languages, an example being Turner's recent work on elementary strong
functional programming.
The restriction to terminating (well-founded) recursions is also necessary for consistency of the logic. For the logic to be consistent, we need to require that not all types are inhabited, which is clearly related to the power of the recursion schemes allowed in Axiom/Aldor. One approach is to expect users to check this for themselves: we would expect this to be replaced by some automated or machine-assisted checking of termination, which ensures that partially- or totally-undefined proofs are not permitted.
Consistency also depends on the strength of the type system itself; a sufficiently powerful type system will be inconsistent as shown by Girard's paradox.
A more expressive type system allows programmers to give more accurate types to functions, expressing their logical pre- and post-conditions. An example is the function which indexes the elements of a vector, which can be defined to reflect the fact that it only gives a result when the index value is in range; its type is
(m:Nat) -> (n:Nat) -> (Vector(n) -> (m < n) -> Double)The extra argument - a proof that
m
is less than n
- becomes a proof obligation which
must be discharged - or at least noted -
when the function is applied to elements m
and
n
.
We discuss examples of pre- and post-conditions from the case study of symbolic asymptotics in below.
In introducing the types we gave the category of
monoids,
Monoid
. Using `==' for the
identity predicate we can add the appropriate logical properties to
the signature in Monoid
:
leftUnit : (g:%) -> (1*g == g); rightUnit : (g:%) -> (g*l == g); assoc : (g:%,h:%,j:%) -> (g*(h*j) == (g*h)*j);The Axiom/Aldor operations over categories, such as extension and join, will lift to become operations of extension and join over the extended `logical' categories like the example here.
One can interpret the obligations given above
with differing degrees of rigour.
Using the pretend
function - which changes the type of a value -
we can conjure up proofs of the
logical requirements of Monoid
; even in this case they appear as
important documentation of requirements, and they are related to the
lightweight formal methods work at St Andrews.
Alternatively we can build fully-fledged proofs as in the numerous implementations of constructive type theories mentioned above, or we can indeed adopt an intermediate position of proving properties seen as `crucial' while asserting the validity of others.