Paul Hudak paul.hudak at yale.edu
Tue Mar 20 23:10:46 EDT 2007

```Assuming 1 :: Int, then:
ones = 1 : ones
is equivalent to:
ones = fix (\ones -> 1:ones)
where fix has type ([Int] -> [Int]) -> [Int].

It's also the case that:
inf = 1+inf
is equivalent to:
inf = fix (\inf -> 1+inf)
where fix has type (Int -> Int) -> Int.
Unfortunately (perhaps), the fixed point returned is _|_,
since it is the LEAST solution to the recursive equation.

-Paul

Dan Weston wrote:
> But in fact it seems to me that the type variable "a" not only can,
> but must unify with "b->c".
>
> Is there any use of fix for which this is not true? If this is true,
> is the type "a" instead of "b->c" because it is not possible in
> general for the type checker to verify this fact, making it some kind
> of underivable true statement?
>
> If it is not true, I would dearly love to see a use of fix with a type
> for which functional application is not defined.
>
> For me, it is this aspect (the type of fix) that has made it so much
> harder to understand fix than it should have been.
>
> Dan

```