Long story short, I was watching this lecture from Simon Peyton-Jones, and at the time 21:41 he shows a quote:
I was squashing a bug, got frustrated, and typed "fix error" in ghci…
And I tried.
Result:
λ> import Data.Function -- here is fix
λ> fix error
"*** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: *** Exception: and goes on like this towards infinity
At first I simply thought what the heck does this fix
do?
So I looked at some types
λ> :t error
error :: [Char] -> a
λ> :t fix
fix :: (a -> a) -> a
hence
λ> :t fix error
fix error :: [Char]
but clearly this still didn't tell me much about the result.
The even stranger thing is, though, that even take 10 $ fix error
or length $ take 10 $ fix error
is such a neverending output as the one above (except that the output of the latter, length …
, lacks the initial "
).
What am I looking at?
To be clear, at the moment I still don't understand much out of the docs on hackage. Not that I have dedicated more than 3 minutes to it, but I'm still lost at the first line of it.
CodePudding user response:
It produces error (error (error (error …)))
. Since error
has type [Char] -> a
, we know that here a ~ [Char]
, so the error (error (error (error …)))
will have type [Char]
. Once we evaluate this, it will however raise an error, and thus it prints *** Exception:
and then aims to print the message, but that is also an error
so it prints another *** Exception:
and so on.
why also
take 10 $ fix error
does the same too?
Because it will also error when it aims to take the first 10 elements of the list, since evaluating the list raises an error, and when printing the exception, the same behavior will start.
It thus never generates a list of Char
s: it raises an error and starts printing the error message, not returining it.
CodePudding user response:
fix
calculates a fixed point of a function; a fixed point is a value you can feed to the function for which it will produce exactly the same value as the result.
For example, if you have the function f _ = "hello"
(or const "hello"
), then a fixed point of this function is the string "hello"
. And indeed fix f
is "hello"
.
Many functions have multiple fixed points, so the documentation for fix
needs to specify which one it returns. For example:
g :: Integer -> Integer
g x
| even x = x
| otherwise = x 1
Every even number is a fixed point of g
, but fix g
promises (by its type) to be a specific Integer
. Which one?
The documentation says that fix
produces the least fixed point, and further clarifies that this means the least defined value that is a fixed point of the input function. Note that "least defined" does not mean the smallest value that is defined, it means the value that has the minimum "definedness". This is a technical area I'm not quite as on top of as I'd like to be, in an informal sense: values like 1 :: Integer
, True
, ()
, Just 'a'
etc a fully defined, because you can evaluate them fully without hitting an error. Bottom values (undefined
, let x = x in x
, etc) are completely undefined. In-between are values like 1 : 2 : undefined
, where you can look at some structure without hitting an error, but there is a bottom somewhere inside.
So fix g
is just bottom (GHC detected an infinite loop and aborted it, when I tried), because g undefined
is an error (and all bottoms are "the same value" for this purpose).
This turns out to be the case for most simple functions you might write when playing around with fix
. For any strict function (one which examines its argument in any way), bottom will be a fixed point and that's the one fix
will calculate. So why do we care about it?
fix
is of great theoretical interest because you can use it to implement recursion in a language that lacks direct support for it. In recursive definitions like this:
sum :: [Integer] -> Integer
sum [] = 0
sum (x : xs) = x sum xs
There's actually something slightly impressive going on. You're defining sum
, but sum
is in scope within its own definition. Implementing that feature is a bit more difficult than compiling definitions which only use pre-existing definitions. Let's imagine we couldn't do that, but we still want to write sum
. You can do it like this:
sum' :: ([Integer] -> Integer) -> [Integer] -> Integer
sum' _ [] = 0
sum' rec (x : xs) = x rec xs
sum = fix sum'
Now every definition only uses things that have previously been defined; there is no self reference. Instead of calling itself directly sum'
receives an extra argument which is the function it should call on the tail of the list. That function argument has to have the same type we originally wanted to give sum
, which makes the type of sum'
an instance of a -> a
, so we can call fix
on it. And it turns out the least fixed point of sum'
is a function equivalent to the original sum
!
The way it does this is by generating an "infinitely nested" expression of the form sum' (sum' (sum' (sum' ...)))
(this is basically the way it finds the fixed point of any function; the answer is already getting pretty long so I won't go over why exactly this works here). Each sum'
receives an argument that says what to do with the tail of the list; that argument is itself another call to sum'
that needs an argument saying what to do with the tail of the tail of the original list, and that argument is another call to sum'
, and so on. Eventually (if the list is finite) we hit the base case for the empty list and don't need the next level of nested sum'
call, and thus it doesn't matter that there is no end to the nested expression! (This wouldn't work in an eagerly evaluated language, obviously)
This turns out to be a general pattern you can apply to translate direct recursion into usage of fix
.
So with that all said, hopefully you can see why fix error
behaves the way it does. Willem Van Onsem's answer is good here, so I won't repeat at length. But basically fix error
has to come up with a string s
such that error s
is equivalent to s
. This is of course impossible for any non-bottom string, since error
always produces bottom (that's the whole point of it), so fix error
has to be some form of bottom. In searching for the fixed point it generates an infinitely nested expression error (error (error ...))
, and when GHC is printing an error message which itself generates an error whose message is another error, etc etc, what you have seen is the output that gets produced.