Typing a function which includes its axioms?

I'm trying to figure out how to type a function and include a set of axioms at the same time.

Here's a concrete example.. Let's say I decide to build a system which uses Natural numbers:

   Nat = Z
       | Succ( Nat )

Now I want to be able to add two Nats together in one of the system's modules so I define a function called Add for this purpose. Its type (pseudo-haskell):

   Add :: a -> a -> a

And a version which implements addition of Naturals (using rewrite rule notation):

   Add( x Z ) = x
   Add( x Succ( y ) ) = Succ( Add( x y ) )

Note that Add does not restrict the type of its arguments to Nat, since I may want to introduce a version which adds Int, or Real down the road. However, when I use Add in the system, I expect it to follow some basic axioms:

    Add( a b ) = Add( b a )
    Add( Add(a b) c ) = Add( a Add(b c) )
    There exists some Z such that: Add( a Z ) = a

Basically, I want to include these axioms as part of the TYPE of Add.. If someone writes a version of Add which does not also fulfill the axioms, there should be a type error. I understand that this means a lot of tricky design to avoid bumping into the Halting Problem during type-checking, but I'm just trying to work out the framework first and maybe there's a side-step I can take later on..

My first pass goes something like this:

  • For starters, each axiom can be given a name to use as an identifier.
       axiomX :: Add( a b ) = Add( b a )
       axiomY :: Add( Add(a b) c ) = Add( a Add(b c) )
  • The axioms are attached to the function type like arguments to a constructor.
        Add :: a -> a -> a


        Add[axiomX axiomY axiomZ] :: a -> a -> a
  • During type-checking, the set of axioms are checked alongside its usual type. Axioms can be matched in any order, like typical sets.
      Add[X Y Z] matches any of Add[X Z Y], Add[Y X Z], Add[Z Y X], ...
  • Here's where things get messy...
    • If all axioms are identical, the types are equivalent.
    • If the required type contains more axioms than the supplied type, there is a type error (insufficient axioms to ensure correctness).
    • If the required type contains fewer (or different) axioms than the supplied type then the type in question MAY be compatible. For instance, it may include an axiom to improve efficiency or restrict the set of values, both of which would be compatible with the existing axioms. So we have to start comparing axioms to check for equivalency of terms (ie: Halting Problem).

Has anyone studied this before? Is there a name for what I'm trying to do?


Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

umm, i think that you can

umm, i think that you can encode this sort of stuff without all the extra complexity using either typeclasses or functors...

tags and assert

First post at this forum. Hi.

Not sure if this is related, but I've been thinking of a similar problem. Maybe it will inspire you in some direction.

Anyway, I was thinking about the problem of how to make some kinds of "sticky assertions" to avoid having to do redundant tests on arguments. (not null tests in Java f.ex.)

One solution that came to mind was to have assertions that "tag" data (decorator pattern?). If the assertion can be proven at compile time the assertion would be optimized away, otherwise it will be a runtime test.

In a way the assertions would thus dynamically alter the type of the data so it would be equivalent with having a function that just outputs it's argument as a subtype or else throws an exception.

The main point is that the compiler doesn't have to enforce the assertion, it can simply trust the programmer and assist in spotting problems when possible.

So the commutation rule of the function could be expressed with some assertion and the meaning of it.

assertCommutative(f) could tag f after some limited unit testing with
∀x ∀y f(x, y) = f(y, x)


You might want to look at the OBJ family, including Maude. It includes things like commutativity axioms.

Qualified Types

Qualified types are an old idea but a really powerful one: it can be used to explain both type classes and row variables. The axioms could be encoded as predicates on types and the function can only be applied to values of types that have evidence of satisfying the predicate.

Algebraic specification

I think what you're after is work on algebraic specification, and verification of programs against algebraic specifications. As someone else pointed out there's the OBJ family. There's also ExtendedML, CASL, and HasCASL. Just generally reading up on algebraic specification might be a practical approach.

Looks like just the thing!

A cursory scan of the ExtendedML literature included several examples of modules and axioms I've been using as examples in my head. Thanks! I'll read up on algebraic specification and the other languages suggested.


How did that work out?

I have been looking at algebraic specifications from a "that sounds interesting" point of view. What I have found is that they give you a way to formalize axioms that code must adhere to, but I have yet to see an example that makes is clear how to use them outside of design. I guess, can anyone explain how to use algebraic specifications when actually writing functions that the must adhere to the specifications, in a way that if they do not the compiler will catch it?

Just do it!

This is perfectly doable in a system where proofs are first-class citizens like Coq. Even with typeclasses niceness.

In general,

Could someone use an algebraic specification language like some OBJ, to verify that the axioms are being met by some implementation in a more general purpose language like Java? If so, this could really help a project I am working on to create testing, and programming assignments from abstract (or even algebraic) problem descriptions.

Java+ITP and the Key project

I don't know of any work trying to validate Java programs directly in OBJ, but there are related tools based on rewriting logic and dynamic logic.

Related LTU discussion

Benjamin Pierce has a marvelous talk that describes why incorporating things like pre- and post-conditions into a static type system is problematic. There was a discussion of this on LtU here, including a reference to the original slides, which are both readable and humorous.