haskelltypessignatureparametric-polymorphismtype-signature

Type signatures that never make sense


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.


Solution

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

    forall t1,t2 in TYPES, R in REL(t1,t2).
     forall p :: t1 -> t1.
      forall q :: t2 -> t2.
       (forall (x, y) in R. (p x, q y) in R)
       ==> (forall (z, v) in lift{[]}(R). f_{t1} p z = f_{t2} q v)
    
    lift{[]}(R)
      = {([], [])}
      u {(x : xs, y : ys) | ((x, y) in R) && ((xs, ys) in lift{[]}(R))}
    

    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 pick t1=Bool and t2=Int.

    Then we need to choose a function p :: Bool -> Bool (say p=not), and a function q :: Int -> Int (say q = \x -> 1-x).

    Now, we need to define a relation R between Bools and Ints. Let's take the standard boolean <->integer correspondence, i.e.:

    R = {(False,0),(True,1)}
    

    (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:

    Case (x,y) = (False,0): we verify that (not False, 1-0) = (True, 1) in R   (ok!)
    Case (x,y) = (True ,1): we verify that (not True , 1-1) = (False,0) in R   (ok!)
    

    So far so good. Now we need to "lift" the relation so to work on lists: e.g.

    [True,False,False,False] is in relation with [1,0,0,0]
    

    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 have

    f_Bool not [True,False,False,False] = f_Int (\x->1-x) [1,0,0,0]
    

    where above f_Bool simply makes it explicit that f is used in the specialised case in which a=Bool.

    The power of this lies in that we do not know what the code of f actually is. We are deducing what f 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:

    forall t1,t2 in TYPES.
     forall p :: t1 -> t1.
      forall q :: t2 -> t2.
       forall z :: [t1].
        forall v :: [t2].
         length z = length v ==> f_{t1} p z = f_{t2} q v
    

    Hence, f ignores the first argument and only cares about the length of the second one.

    QED