Free theorems

Free Theorems were first described in the paper "Theorems for free!" by Philip Wadler. Their special property is that they can be derived solely from the type of a function. The key idea is to interpret types as relations. To reflect the structure of types, a relational action, which maps relations to a relation, is defined for every type constructor. Using relational actions, a relation can be constructed for every type, and, by applying the definitions of these relational actions, free theorems are obtained.

General recursion and selective strictness weaken free theorems. To show the influences caused by adding these constructs, several sublanguages of Haskell are supported in this tool. The theoretical foundations are described in the paper "Free theorems in the presence of seq" by Patricia Johann and Janis Voigtländer. As motivated there, it is possible to derive both equational and inequational free theorems.

Types

Types can be entered in two ways, either with a name or without one. Examples would be

g :: forall b . (Int -> b -> b) -> b -> b

or

[a] -> [a]

It is also possible to simply enter the name of a predefined Haskell function (see the list given below). The tool knows about standard Haskell data types, type synonyms, and type classes (again, see the lists below). Additionally, T0 to T9 may be used as placeholders for arbitrary, but fixed types.

Supported algebraic data types

Bool
Maybe
Either
Ordering
Complex
Ratio

Supported type synonyms

String
Rational
ShowS
ReadS
FilePath

Supported type classes

Eq
Ord
Enum
Bounded
Num
Real
Integral
Fractional
Floating
RealFrac
RealFloat
Show
Read
Monoid

Types of predefined functions

(&&) :: Bool -> Bool -> Bool
(||) :: Bool -> Bool -> Bool
not :: Bool -> Bool
otherwise :: Bool
maybe :: forall a b . b -> (a -> b) -> Maybe a -> b
either :: forall a b c . (a -> c) -> (b -> c) -> Either a b -> c
fst :: forall a b . (a, b) -> a
snd :: forall a b . (a, b) -> b
curry :: forall a b c . ((a, b) -> c) -> a -> b -> c
uncurry :: forall a b c . (a -> b -> c) -> (a, b) -> c
max :: forall a . a -> a -> a
min :: forall a . a -> a -> a
subtract :: forall a . Num a => a -> a -> a
even :: forall a . Integral a => a -> Bool
odd :: forall a . Integral a => a -> Bool
gcd :: forall a . Integral a => a -> a -> a
lcm :: forall a . Integral a => a -> a -> a
(^) :: forall a b . (Num a, Integral b) => a -> b -> a
(^^) :: forall a b . (Fractional a, Integral b) => a -> b -> a
fromIntegral :: forall a b . (Integral a, Num b) => a -> b
realToFrac :: forall a b . (Real a, Fractional b) => a -> b
id :: forall a . a -> a
const :: forall a b . a -> b -> a
(.) :: forall a b c . (b -> c) -> (a -> b) -> a -> c
flip :: forall a b c . (a -> b -> c) -> b -> a -> c
($) :: forall a b . (a -> b) -> a -> b
until :: forall a . (a -> Bool) -> (a -> a) -> a -> a
asTypeOf :: forall a . a -> a -> a
error :: forall a . [Char] -> a
undefined :: forall a . a
seq :: forall a b . a -> b -> b
($!) :: forall a b . (a -> b) -> a -> b
map :: forall a b . (a -> b) -> [a] -> [b]
(++) :: forall a . [a] -> [a] -> [a]
filter :: forall a . (a -> Bool) -> [a] -> [a]
head :: forall a . [a] -> a
last :: forall a . [a] -> a
tail :: forall a . [a] -> [a]
init :: forall a . [a] -> [a]
null :: forall a . [a] -> Bool
length :: forall a . [a] -> Int
(!!) :: forall a . [a] -> Int -> a
reverse :: forall a . [a] -> [a]
foldl :: forall a b . (a -> b -> a) -> a -> [b] -> a
foldl1 :: forall a . (a -> a -> a) -> [a] -> a
foldr :: forall a b . (a -> b -> b) -> b -> [a] -> b
foldr1 :: forall a . (a -> a -> a) -> [a] -> a
and :: [Bool] -> Bool
or :: [Bool] -> Bool
any :: forall a . (a -> Bool) -> [a] -> Bool
all :: forall a . (a -> Bool) -> [a] -> Bool
sum :: forall a . Num a => [a] -> a
product :: forall a . Num a => [a] -> a
concat :: forall a . [[a]] -> [a]
concatMap :: forall a b . (a -> [b]) -> [a] -> [b]
maximum :: forall a . Ord a => [a] -> a
minimum :: forall a . Ord a => [a] -> a
scanl :: forall a b . (a -> b -> a) -> a -> [b] -> [a]
scanl1 :: forall a . (a -> a -> a) -> [a] -> [a]
scanr :: forall a b . (a -> b -> b) -> b -> [a] -> [b]
scanr1 :: forall a . (a -> a -> a) -> [a] -> [a]
iterate :: forall a . (a -> a) -> a -> [a]
repeat :: forall a . a -> [a]
replicate :: forall a . Int -> a -> [a]
cycle :: forall a . [a] -> [a]
take :: forall a . Int -> [a] -> [a]
drop :: forall a . Int -> [a] -> [a]
splitAt :: forall a . Int -> [a] -> ([a], [a])
takeWhile :: forall a . (a -> Bool) -> [a] -> [a]
dropWhile :: forall a . (a -> Bool) -> [a] -> [a]
span :: forall a . (a -> Bool) -> [a] -> ([a], [a])
break :: forall a . (a -> Bool) -> [a] -> ([a], [a])
elem :: forall a . Eq a => a -> [a] -> Bool
notElem :: forall a . Eq a => a -> [a] -> Bool
lookup :: forall b a . Eq a => a -> [(a, b)] -> Maybe b
zip :: forall a b . [a] -> [b] -> [(a, b)]
zip3 :: forall a b c . [a] -> [b] -> [c] -> [(a, b, c)]
zipWith :: forall a b c . (a -> b -> c) -> [a] -> [b] -> [c]
zipWith3 :: forall a b c d . (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
unzip :: forall a b . [(a, b)] -> ([a], [b])
unzip3 :: forall a b c . [(a, b, c)] -> ([a], [b], [c])
lines :: [Char] -> [[Char]]
words :: [Char] -> [[Char]]
unlines :: [[Char]] -> [Char]
unwords :: [[Char]] -> [Char]
shows :: forall a . Show a => a -> [Char] -> [Char]
showChar :: Char -> [Char] -> [Char]
showString :: [Char] -> [Char] -> [Char]
showParen :: Bool -> ([Char] -> [Char]) -> [Char] -> [Char]
reads :: forall a . Read a => [Char] -> [(a, [Char])]
readParen :: forall a . Bool -> ([Char] -> [(a, [Char])]) -> [Char]
           -> [(a, [Char])]
read :: forall a . Read a => [Char] -> a
lex :: [Char] -> [([Char], [Char])]
realPart :: forall a . RealFloat a => Complex a -> a
imagPart :: forall a . RealFloat a => Complex a -> a
mkPolar :: forall a . RealFloat a => a -> a -> Complex a
cis :: forall a . RealFloat a => a -> Complex a
polar :: forall a . RealFloat a => Complex a -> (a, a)
magnitude :: forall a . RealFloat a => Complex a -> a
phase :: forall a . RealFloat a => Complex a -> a
conjugate :: forall a . RealFloat a => Complex a -> Complex a
intersperse :: forall a . a -> [a] -> [a]
transpose :: forall a . [[a]] -> [[a]]
foldl' :: forall a b . (a -> b -> a) -> a -> [b] -> a
foldl1' :: forall a . (a -> a -> a) -> [a] -> a
mapAccumL :: forall acc x y . (acc -> x -> (acc, y)) -> acc -> [x] -> (acc, [y])
mapAccumR :: forall acc x y . (acc -> x -> (acc, y)) -> acc -> [x] -> (acc, [y])
unfoldr :: forall a b . (b -> Maybe (a, b)) -> b -> [a]
group :: forall a . Eq a => [a] -> [[a]]
inits :: forall a . [a] -> [[a]]
tails :: forall a . [a] -> [[a]]
isPrefixOf :: forall a . Eq a => [a] -> [a] -> Bool
isSuffixOf :: forall a . Eq a => [a] -> [a] -> Bool
find :: forall a . (a -> Bool) -> [a] -> Maybe a
partition :: forall a . (a -> Bool) -> [a] -> ([a], [a])
zip4 :: forall a b c d . [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
zip5 :: forall a b c d e . [a] -> [b] -> [c] -> [d] -> [e]
                   -> [(a, b, c, d, e)]
zip6 :: forall a b c d e f . [a] -> [b] -> [c] -> [d] -> [e] -> [f]
                     -> [(a, b, c, d, e, f)]
zip7 :: forall a b c d e f g . [a] -> [b] -> [c] -> [d] -> [e] -> [f]
                       -> [g] -> [(a, b, c, d, e, f, g)]
zipWith4 :: forall a b c d e . (a -> b -> c -> d -> e) -> [a] -> [b] -> [c]
                   -> [d] -> [e]
zipWith5 :: forall a b c d e f . (a -> b -> c -> d -> e -> f) -> [a] -> [b]
                     -> [c] -> [d] -> [e] -> [f]
zipWith6 :: forall a b c d e f g . (a -> b -> c -> d -> e -> f -> g) -> [a]
                       -> [b] -> [c] -> [d] -> [e] -> [f] -> [g]
zipWith7 :: forall a b c d e f g h . (a -> b -> c -> d -> e -> f -> g -> h)
                         -> [a] -> [b] -> [c] -> [d] -> [e] -> [f] -> [g] -> [h]
unzip4 :: forall a b c d . [(a, b, c, d)] -> ([a], [b], [c], [d])
unzip5 :: forall a b c d e . [(a, b, c, d, e)] -> ([a], [b], [c], [d], [e])
unzip6 :: forall a b c d e f . [(a, b, c, d, e, f)]
                     -> ([a], [b], [c], [d], [e], [f])
unzip7 :: forall a b c d e f g . [(a, b, c, d, e, f, g)]
                       -> ([a], [b], [c], [d], [e], [f], [g])
nub :: forall a . Eq a => [a] -> [a]
delete :: forall a . Eq a => a -> [a] -> [a]
(\\) :: forall a . Eq a => [a] -> [a] -> [a]
union :: forall a . Eq a => [a] -> [a] -> [a]
intersect :: forall a . Eq a => [a] -> [a] -> [a]
sort :: forall a . Ord a => [a] -> [a]
insert :: forall a . Ord a => a -> [a] -> [a]
nubBy :: forall a . (a -> a -> Bool) -> [a] -> [a]
deleteBy :: forall a . (a -> a -> Bool) -> a -> [a] -> [a]
deleteFirstsBy :: forall a . (a -> a -> Bool) -> [a] -> [a] -> [a]
unionBy :: forall a . (a -> a -> Bool) -> [a] -> [a] -> [a]
intersectBy :: forall a . (a -> a -> Bool) -> [a] -> [a] -> [a]
groupBy :: forall a . (a -> a -> Bool) -> [a] -> [[a]]
sortBy :: forall a . (a -> a -> Ordering) -> [a] -> [a]
insertBy :: forall a . (a -> a -> Ordering) -> a -> [a] -> [a]
maximumBy :: forall a . (a -> a -> Ordering) -> [a] -> a
minimumBy :: forall a . (a -> a -> Ordering) -> [a] -> a
genericLength :: forall b i . Num i => [b] -> i
genericTake :: forall a i . Integral i => i -> [a] -> [a]
genericDrop :: forall a i . Integral i => i -> [a] -> [a]
genericSplitAt :: forall b i . Integral i => i -> [b] -> ([b], [b])
genericIndex :: forall b a . Integral a => [b] -> a -> b
genericReplicate :: forall a i . Integral i => i -> a -> [a]
isJust :: forall a . Maybe a -> Bool
isNothing :: forall a . Maybe a -> Bool
fromJust :: forall a . Maybe a -> a
fromMaybe :: forall a . a -> Maybe a -> a
listToMaybe :: forall a . [a] -> Maybe a
maybeToList :: forall a . Maybe a -> [a]
catMaybes :: forall a . [Maybe a] -> [a]
mapMaybe :: forall a b . (a -> Maybe b) -> [a] -> [b]
(%) :: forall a . Integral a => a -> a -> Ratio a
numerator :: forall a . Integral a => Ratio a -> a
denominator :: forall a . Integral a => Ratio a -> a
approxRational :: forall a . RealFrac a => a -> a -> Ratio Integer