### 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 -> bor

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

### Output formats

The following output formats can be selected:

- PNG
- Result is displayed on webpage, formulae are rendered as PNG images —
*This is the default.* - Plain
- Result is displayed on webpage, formulae are rendered as plain text.
- TeX
- A TeX file is generated. You need lambdaTeX.tex (adapted from Patryk Zadarnowski) and pdflatex to get the same result as by selecting the 'PDF' option.
- A PDF file is generated.

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

### Supported algebraic data types (excluding T0 to T9)

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