Getting infinite type error when making function that runs its input on itself

Viewed 110

I'm trying to figure out why this code is not working as intended.

I want to make a function run that takes as input some function and returns that function applied to itself.

run::(t1->t2)->t2
run a = a a

The types included are supposed to be general because I want this to work on anything, but I'm getting and infinite type error when I try and I'm not sure why.

3 Answers

You say a :: t1 -> t2. This means its argument should have type t1. Then you apply it to itself, a a. This means its argument is a.

So now we have an equation: the argument should have both the type t1 (because it is an argument to a) and the type t1 -> t2 (because it is a):

t1 ~ t1 -> t2
   ~ (t1 -> t2) -> t2
   ~ ((t1 -> t2) -> t2) -> t2
   ~ (((t1 -> t2) -> t2) -> t2) -> t2
   ~ ...

Each line follows from the previous by replacing t1 by the thing it's equal to, t1 -> t2. No finite types satisfy the given equality.

If you want to write the equivalent of (λx. xx) (λx. xx) or a Y combinator in Haskell, it can be done:

Prelude> newtype F t2 = Wrap {unwrap :: F t2 -> t2}
Prelude> run x = (unwrap x) x
Prelude> :t run
run :: F t2 -> t2
Prelude> run (Wrap run)
^C
Interrupted.
Prelude> myFix f = run (Wrap (\x -> f ((unwrap x) x)))
Prelude> factorial = myFix (\fac n -> if n == 0 then 1 else n * fac (n - 1))
Prelude> factorial 5
120

Adding and removing the newtype wrapper is a no-op at runtime.

Haskell doesn't allow this sort of self-referential ("infinite") type without a data or newtype wrapper. Automatically inferring infinite types is possible, and wouldn't make the type system any more inconsistent than it already is, but infinite types aren't very useful, and they often show up by accident in buggy code that really shouldn't type check, so it's probably better that they're rejected.

You write

run::(t1->t2)->t2
run a = a a

Because a is the argument of the function,

a :: t1 -> t2

Now you're applying a to a. The argument of a has type t1, so we must have

a :: t1

The only this can make sense is if t1 is the same as t1 -> t2. So that would mean

t1
= t1 -> t2
= (t1 -> t2) -> t2
= ((t1 -> t2) -> t2) -> t2
= ...

That's probably where your infinite type error comes from. I'm not sure why you don't get a simpler error saying that t1 is not the same as t1 -> t2.

So ... you can't exactly call a function with itself in Haskell. You can do some similar things, with some care. But how you do it will depend on exactly what you're trying to accomplish.

Related