Lambda the Ultimate

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
    etc..

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
  

  becomes:

      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?

Thanks!
--Bryan