Axioms and properties for haskell classes

Alberto Gómez Corona agocorona (at) gmail.com

NOTE: added changes to avoid error due to duplicated instances. See code below.

Eureka!!!

Eureka!!!

. I found someting interesting that have something in the middle
of the heaven of universal algebras and the firm ground of quickcheck:

This is a way to express axioms in pure Haskell and make practical use of them at the same time:

First, I start by defining a special class called Axioms that contains list of different properties with different arities.

data Axiom a= Axiom String a

**class Axioms a where**

unaryAxioms :: [Axiom (a -> Bool)]

unaryAxioms = []

binaryAxioms :: [Axiom ((a,a) -> Bool)]

binaryAxioms = []

ternaryAxioms :: [Axiom ((a,a,a) -> Bool)]

ternaryAxioms = []

unaryAxioms :: [Axiom (a -> Bool)]

unaryAxioms = []

binaryAxioms :: [Axiom ((a,a) -> Bool)]

binaryAxioms = []

ternaryAxioms :: [Axiom ((a,a,a) -> Bool)]

ternaryAxioms = []

For properties involving relations between two or many classes, a similar multiparameter type class is also possible (see code below).

If I need to define axioms/properties for the the methods of a
class, I just make the class a instance of Axioms:. For example, for a
Ring:

class Eq a => Ring a where

op1 :: a -> a -> a

op2 :: a -> a -> a

zero :: a

inverse :: a -> a

You see that the kind of both op1 and op2 say very little about the structure of the ring. Anyone can instantiate a Num class without respecting the nature of * and + operations.

**What gives a Class the meaning and structure of the Class for which he was designed are the axioms.***I want to express that whenever a Ring a is defined, it must agree with some Axioms. I think that this way of defining properties is fairly meaningful to say in haskell:*

instance Ring a => Axioms a where

unaryAxioms = [Axiom "identity" (\x -> zero `op2` x == zero)

,Axiom "inverse element" (\x -> x `op1` (inverse x) == zero)

]

binaryAxioms = [Axiom "commutative" (\(x, y) -> x `op1` y == y `op1` x)]

ternaryAxioms = [Axiom "associative `op1`" (\(x,y,z) -> (x `op1` y) `op1` z== x `op1` (y `op1` z))

,Axiom "associative `op2`" (\(x,y,z) -> (x `op2` y) `op2` z== x `op2` (y `op2` z))

,Axiom "distributive" (\(x,y,z) -> x `op2` (y `op1` z)== (x `op2` y) `op1` (x `op2` z))

,Axiom "distributive2" (\(x,y,z) -> (x `op1` y) `op2` z== (x `op2` z) `op1` (y `op2` z))

]

What practical use can I extract from this stuff?

Lets define any object of the class Num as a Ring

instance Num a => Ring a where

op1= (+)

op2= (*)

zero = 0

inverse= negate

Now we will see te return of all of this stuff. We have Num, We have the operators of Num and we have the

**meaning, the semantic that glue all pieces togeter**captured in the Ring axioms. Now, in a Galaxy far away, someone define a new data type as member of the class Num. Because Num is a Ring , It can test the compliance with the axioms of this new Ring candidate:

instance Num N where

(+) (N x) (N y)= N (x + y) `verify` binaryAxioms `with` ((N x), (N y))

(-) (N x) (N y)= N (x - y)

(*) (N x) (N y)= N (x * y)

negate (N x)= N (-x)

abs (N x) = N (abs x)

signum (N x)= N (signum x)

fromInteger i= N (fromInteger i)

main= do

let x= N 5

let y= N 3 `verify` unaryAxioms `with` x

let z= x + y

print z

let t= N 7

print t `verify` ternaryAxioms `with` (x,y,z)

Here I show two different ways to test axioms/ properties: Either in the instance definition or in the middle of the code

With "verify axiom data" inserted in strategic parts of the
code i have a cheap quickcheck with the advantage that I can test the
real data of my aplication. you can play with the class definitions and see the violated axioms.

Note that with the Ring properties I can define subtractions in a counterintuitive way, since the ring properties say nothing practical
about substraction. Here we can see the difference between axiom and
the more practical concept of "property". although both can have the
same shape.

Note that for this ring is fairly straighforward to realize that
it is a ring since it is a small modification of Number. This would be
not so obvous for more complicated datatypes, maybe this is a way to add confidence for
managing complicated pieces of code with unsafe IO operations and other beasts as Rings or other mathematical structures!.

This can be applied of course for anything you may think that may have a property to check.

I´m excited!

*NOTE : I had to eliminate the separate Axioms class and put the properties directly inside the class definitions due to some limitations. that makes thigs a little less flexible. Here is the code:*The complete code:

Copyright (c) Alberto Gómez Corona 2008 agocorona@gmail.com

see http://docs.google.com/Doc?id=dd5rm7qq_165rshp74gf&hl=en

version 2.0

corrected some instantiation problems

All rights reserved.

Redistribution and use in source and binary forms, with or without

modification, are permitted provided that the following conditions

are met:

1. Redistributions of source code must retain the above copyright

notice, this list of conditions and the following disclaimer.

2. Redistributions in binary form must reproduce the above copyright

notice, this list of conditions and the following disclaimer in the

documentation and/or other materials provided with the distribution.

3. Neither the name of the author nor the names of his contributors

may be used to endorse or promote products derived from this software

without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND

ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE

IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE

ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE

FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL

DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS

OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)

HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT

LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY

OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF

SUCH DAMAGE.

{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}

import Debug.Trace

import Control.Concurrent.MVar

import System.IO.Unsafe

import Control.Exception(evaluate)

import Data.Maybe(catMaybes)

import Control.Monad(when)

import Debug.Trace

debug a b= trace b a

data Axiom a= Axiom String a

data Axioms a=

Axioms{unary :: [Axiom (a -> Bool)]

,binary :: [Axiom ((a,a) -> Bool)]

,ternary :: [Axiom ((a,a,a) -> Bool)]

}

axioms= Axioms [] [] []

type Relations a b = [Axiom ((a,b) -> Bool)]

type TermaryRelation a b c = [Axiom ((a,b,c) -> Bool)]

inTest= unsafePerformIO $ newMVar True

with= ($)

verify :: Show b => a ->[Axiom (b -> Bool)] -> b -> a

verify res axioms v = check `seq`res where

check =unsafePerformIO $

do

int <- tryTakeMVar inTest

if int == Nothing then return ()

else do

errors <- evaluate$ unlines $ catMaybes $ map ( test v) axioms

when (not $ null errors) ( putTraceMsg errors)

putMVar inTest False

return ()

where

test v (Axiom n f) = if f v then Nothing

else Just $ "violated axiom "++n ++ " with value/s: " ++ show v

--------------------------- Example for a Ring -------

class Eq a => Ring a where

op1 :: a -> a -> a

op2 :: a -> a -> a

zero :: a

inverse :: a -> a

ringAxioms :: Axioms a

ringAxioms= axioms{

unary= [Axiom "identity" (\x -> zero `op2` x == zero)

,Axiom "inverse element" (\x -> x `op1` (inverse x) == zero)]

,binary= [Axiom "commutative" (\(x, y) -> x `op1` y == y `op1` x)]

,ternary= [Axiom "associative `op1`" (\(x,y,z) -> (x `op1` y) `op1` z== x `op1` (y `op1` z))

,Axiom "associative `op2`" (\(x,y,z) -> (x `op2` y) `op2` z== x `op2` (y `op2` z))

,Axiom "distributive" (\(x,y,z) -> x `op2` (y `op1` z)== (x `op2` y) `op1` (x `op2` z))

,Axiom "distributive2" (\(x,y,z) -> (x `op1` y) `op2` z== (x `op2` z) `op1` (y `op2` z))

]

}

----------------Define a simple Ring set --------------

instance Num a => Ring a where

op1= (+)

op2= (*)

zero = 0

inverse= negate

data N= N Int deriving ( Eq, Show)

instance Show N => Num N where

(+) (N x) (N y)= N (x + y) `verify` (binary ringAxioms) `with` ((N x), (N y))

(-) (N x) (N y)= N (x - y)

(*) (N x) (N y)= N (x * y)

negate (N x)= N (-x)

abs (N x) = N (abs x)

signum (N x)= N (signum x)

fromInteger i= N (fromInteger i)

class (Eq a) =>String1 a where

(+++) :: a -> a -> a

len :: a -> Int

stringAxioms :: Axioms a

stringAxioms=

axioms {binary=[Axiom "length" (\(x, y)-> (len (x+++y))== ((len x) + (len y)))]}

data A= A String deriving Eq

instance String1 A where

(+++) (A x) (A y)= A (x++y++"hola")

len (A x)= length x

main= do

let x= N 5

let y= N 3 `verify` (unary ringAxioms) `with` x

let z= x + y

print z

let t= N 7

print t `verify` (ternary ringAxioms) `with` (x,y,z)

let

print x