User loginNavigation 
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 (pseudohaskell): 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 typechecking, but I'm just trying to work out the framework first and maybe there's a sidestep I can take later on..
Thanks! By Bryan Turner at 20061206 22:40  LtU Forum  previous forum topic  next forum topic  other blogs  4868 reads

Browse archivesActive forum topics 
Recent comments
2 days 14 hours ago
3 days 9 hours ago
3 days 13 hours ago
3 days 14 hours ago
3 days 15 hours ago
3 days 15 hours ago
3 days 16 hours ago
3 days 16 hours ago
3 days 20 hours ago
3 days 20 hours ago