Consider
(a->a) -> [a] -> Bool
Is there any meaningful definition for this signature? That is, a definition that not simply ignores the argument?
x -> [a] -> Bool
It seems there are many such signatures that can be ruled out immediately.
Consider
(a->a) -> [a] -> Bool
Is there any meaningful definition for this signature? That is, a definition that not simply ignores the argument?
x -> [a] -> Bool
It seems there are many such signatures that can be ruled out immediately.
You can't do anything interesting with x
on it's own.
You can do stuff with [x]
; for example, you can count how many nodes are in the list. So, for example,
foo :: (a -> a) -> [a] -> Bool
foo _ [] = True
foo _ (_:_) = False
bar :: x -> [a] -> Bool
bar _ [] = True
bar _ (_:_) = False
If you have an x
and a function that turns an x
into something else, you can do interesting stuff:
big :: (x -> Int) -> x -> Bool
big f n = if f n > 10 then True else False
If x
belongs to some type class, then you can use all the methods of that class on it. (This is really a special-case of the previous one.)
double :: Num x => x -> x
double = (2*)
On the other hand, there are plenty of type signatures for which no valid functions exist:
magic :: x -> y
magic = -- erm... good luck with that!
I read somewhere that the type signatures involving only variables for which a real function exists are exactly the logical theorems that are true. (I don't know the name for this property, but it's quite interesting.)
f1 :: (x -> y) -> x -> y
-- Given that X implies Y, and given that X is true, then Y is true.
-- Well, duh.
f2 :: Either (x -> y) (x -> z) -> x -> Either y z
-- Given that X implies Y or X implies Z, and given X, then either Y or Z is true.
-- Again, duh.
f3 :: x -> y
-- Given that X is true, then any Y is true.
-- Erm, no. Just... no.
Carsten König suggested in a comment to use the free theorem. Let's try that.
Prime the cannon
We start by generating the free theorem corresponding to the type
(a->a) -> [a] -> Bool
. This is a property that every function with that type must satisfy, as established by the famous Wadler's paper Theorems for free!.An example
To better understand the theorem above, let's run over a concrete example. To use the theorem, we need to take any two types
t1,t2
, so we can pickt1=Bool
andt2=Int
.Then we need to choose a function
p :: Bool -> Bool
(sayp=not
), and a functionq :: Int -> Int
(sayq = \x -> 1-x
).Now, we need to define a relation
R
betweenBool
s andInt
s. Let's take the standard boolean <->integer correspondence, i.e.:(the above is a one-one correspondence, but it does not have to be, in general).
Now we need to check that
(forall (x, y) in R. (p x, q y) in R)
. We only have two cases to check for(x,y) in R
:So far so good. Now we need to "lift" the relation so to work on lists: e.g.
This extended relation is the one named
lift{[]}(R)
above.Finally, the theorem states that, for any function
f :: (a->a) -> [a] -> Bool
we must havewhere above
f_Bool
simply makes it explicit thatf
is used in the specialised case in whicha=Bool
.The power of this lies in that we do not know what the code of
f
actually is. We are deducing whatf
must satisfy by only looking at its polymorphic type.Since we get types from type inference, and we can turn types into theorems, we really get "theorems for free!".
Back to the original goal
We want to prove that
f
does not use its first argument, and that it does not care about its second list argument, either, except for its length.For this, take
R
be the universally true relation. Then,lift{[]}(R)
is a relation which relates two lists iff they have the same length.The theorem then implies:
Hence,
f
ignores the first argument and only cares about the length of the second one.QED