axioms-properties for haskell classes

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!!!

 

. 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 = []

 

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

  

  

  

  

  

number lines:format