Nicolas Frisby nicolas.frisby at gmail.com
Tue Mar 20 23:57:31 EDT 2007

```In effect, this is a demonstration that Haskell supports recursive
values and not just recursive functions. If the a in

fix :: (a -> a) -> a

were to be unified always with a function type, then that would imply
that the language only supported recursive definitions for functions,
which would be a bit unfortunate for the co-coders in the community.

It's good to note that simple languages with a strict evaluation
scheme are limited to

fix :: ((a -> b) -> (a -> b)) -> (a -> b)

because functions are the only things that can delay evaluation.

On 3/20/07, Paul Hudak <paul.hudak at yale.edu> wrote:
> 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
>
> _______________________________________________
>
```