Free theorems

Free Theorems were first described by Wadler in "Theorems for free!". Their special property is that they can be derived solely from the type of a function.

For this to work, types have to be interpreted as relations opposed to the usual way of viewing them as sets. Then, for every type construct (e.g. algebraic datatypes or type abstractions), a corresponding relation can be defined, and by this, using the structure of types, every type can be transformed into a relation. Expansion of such a relation yields a free theorem.

This application provides the described algorithm for a restricted set of Haskell types. Excluding type classes and type renamings, all Haskell type constructs are covered, which includes also higher-rank functions.

Since fixpoints and undefined values weaken free theorems, there have to be two different ways to generate them. When considering types of terms using fixpoints, the FixModel has to be used. Otherwise, the BasicModel may be applied.

The presence of "seq" restricts free theorems even more than fixpoints. However, they are not covered by this application, i.e. for types of terms, which are defined using "seq", no free theorem can be generated in this shell.

Types

Types can be entered in two ways, either with a name or without it. Types with a name are described by the syntactic symbol NamedType, while types without it have to be conforming to the syntax described by TypeTerm.

The following EBNF definitions give the syntax of types:

NamedType ::= Name :: TypeTerm

TypeTerm ::= SimpleTypeTerm
           | SimpleTypeTerm -> TypeTerm
           | forall TypeVariableList . TypeTerm

SimpleTypeTerm ::= ATypeTerm
                 | TypeConstructor ATypeTermList
                 | [] ATypeTerm
                 | (,) ATypeTerm ATypeTerm
                 | (,,) ATypeTerm ATypeTerm ATypeTerm
                 | ...
                 | {- tuple in prefix notation of arity 15 -}
                 | (->) ATypeTerm ATypeTerm

ATypeTerm ::= Char | Int | Integer | Float | Double
            | TypeVariable
            | ()
            | [ TypeTerm ]
            | ( TypeTerm , TypeTerm )
            | ( TypeTerm , TypeTerm , TypeTerm )
            | ...
            | {- tuple of arity 15 -}
            | ( TypeTerm )

ATypeTermList ::= ATypeTerm
                | ATypeTermList ATypeTerm

TypeVariableList ::= TypeVariable
                   | TypeVariableList TypeVariable

An additional rule limits the valid type terms: The number of type -- arguments for a type constructor must match the type constructors arity.

Name and TypeVariable are tokens starting with a lower letter or "_", and consisting of alphanumeric letters and the characters "_" and "'" from the second character onwards. A Name or a TypeVariable starting with "_" has to be at least two characters long, because "_" is a reserved identifier in Haskell.

Alternatively, a Name can also be an operator which has to be enclosed in parentheses. Allowed characters of operators are:

!  #  0  &  *  +  .  /  <  =  >  ?  @  \  ^  |  -  ~

In addition to the above symbols, the colon ":" may be used to form operators, but only from the second character onwards. Note that the following operators are restricted keywords in Haskell and cannot be used as names of types:

..  :  ::  =  \  |  <-  ->  @  ~  =>

The tokens described by TypeConstructor start with a capital letter and may consist of alphanumeric letters and the characters "_" and "'" from the second character onwards. Although allowed by the Haskell standard, here, type constructors can not be formed by non-alphanumeric symbols. See the following list of supported type constructors.

Supported algebraic datatypes

Bool
Maybe
Either
Ordering
IOMode
BufferMode
SeekMode
Permissions
ExitCode
Month
Day
CalenderTime
TimeDiff
TimeLocale

Supported type synonyms

String
ReadS
ShowS
FilePath

Predefined Haskell types

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
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. String -> 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 b. (a -> a -> a) -> [a] -> a
foldr :: forall a b. (a -> b -> b) -> b -> [a] -> b
foldr1 :: forall a. (a -> a -> a) -> [a] -> a
any :: forall a. (a -> Bool) -> [a] -> Bool
all :: forall a. (a -> Bool) -> [a] -> Bool
concat :: forall a. [[a]] -> [a]
concatMap :: forall a b. (a -> [b]) -> [a] -> [b]
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])
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])
readParen :: forall a. Bool -> ReadS a -> ReadS a