2

I don't understand the answer to this question:

Q: Can Haskell find a type for the function selfapply defined by: selfapply f = f f

A: The function selfapply is not typeable in the simple system of types: we need to associate to f two types which are not compatible: α → α and α.

So I know a -> a means alpha input and alpha return, but why is it a->a and a instead of a->a->a?

Also another question regarding this topic:

Find a polymorphic type for the functions quad, double

quad x = y*y where y = x*x 
double x = x*2

How can we determine a polymorphic type for these two functions?

  • My first thought is that this can be solved (but not in Haskell) with an infinite type so that adding/removing layers of application still leaves the same infinite type - kind of the same as saying infinity + 1 = infinity. I think that would mean either a = a -> (a -> (a -> (...))) or a = (((...) -> a) -> a) -> a - not sure which ATM. – Steve314 May 2 '15 at 14:00
3

Hm, well for the first one this is because let's say f f was well typed. We're applying f so it has to be a function. Functions have the type f : A -> B for some A and B. Since f is also the argument, it must also be the case that f : A. This means that A = A -> B. Moreover since f = f f, the the type of f f is also the type of f. Since f f : B this means f : B. This means that A = B and so f : A -> A and A -> A = A as required.

For the second, what's the type of *? This is the key to understanding the type of these functions since we're applying * to the input. In Haskell * :: Num a => a -> a -> a, which must mean that our functions have the type Num a -> a -> B for some B. I'll let you figure it out from there :)

  • Why f = f f? The selfapply definition does not require that... – Idan Arye Aug 28 '15 at 1:43
0

There are a couple of levels to your first question. As an aside, though, I recommend learning about unification if you are not already familiar with it as it is a key part of understanding type checking and type inference.

To type check selfApply provisionally give f the type a which we will solve for. (At this point it is just a unification variable, the key difference between Hindley-Milner type checking and type checking for simple types is that we'll generalize (quantify over) any unbound variables at the end.) Since we are using f as a function we know a = b -> c for new variables b and c. Since we are applying f to something of type a, namely f itself, we know b = a. There is no constraint on c, so you are correct to be confused about the provided answer since f isn't required to be a and a -> a and it could indeed be a and a -> a -> a or a and a -> Bool as well. Of course, as you no doubt understand, the issue is solving the equation a = a -> c. In attempting to unify these with traditional unification we will fail what is known as the occurs check. This check is to avoid infinite terms. Rational tree unification is, however, one way to deal with this issue and leads to equi-recursive types. Haskell intentionally does not support equi-recursive types, but O'Caml, for example, does with the -rectypes flag. To validate that c is free we can use an iso-recursive type, namely:

data X c = X (X c -> c)
selfApply f = f (X f)

which will type check, and, in particular, selfApply :: (X c -> c) -> c.

There are two reasons Haskell (and almost all polymorphic languages) do not support equi-recursive types. First, pragmatically, many type errors show up as infinite types and if equi-recursive types were supported (tacitly) then they'd turn into broken but type correct programs. More philosophically, outlawing equi-recursive types and similar things was exactly why type systems were originally invented going all the way back to Bertrand Russell.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.