3 ms·
> If you say a function has type a->a (for all a), it only admits one possible implementation... except for bad ones, like 'undefined' or an infinite recursion
by chowells 2y ago
> If you say a function has type a->a (for all a), it only admits one possible implementation... except for bad ones, like 'undefined' or an infinite recursion - both of which termination would catch for you.
To be super-pedantic, it only admits one possible denotation, assuming termination. There are an infinite number of implementations that waste finite time on something useless before returning the argument. We usually don't talk about those, because... Why would you write code that does that? But it's worth keeping in mind as an edge case in this sort of discussion.
- AlotOfReading 2y agoThere's some useful cousins to the sleep() function in that family.
- mrkeen 2y agoAre there any examples of such a function (a->a) which will eventually terminate, but cannot be optimised away at compile-time?
- chowells 2y agoCannot be optimized away? No. Will not be optimized away? Sure. Given: verySilly :: Int -> (a -> a) verySilly = go . abs . toInteger where go n | n == 1 = id | even n = go (n `div` 2) | otherwise = go (n * 3 + 1) On a 64-bit platform, `verySilly 976532468728515` has type (a -> a) and will eventually terminate (the hailstone sequence is known to enter the 4-2-1 loop on all inputs that small), but no compiler is going to prove it. In theory it could happen. In practice it won't, especially when you consider that there are countless problems you could substitute in.
- chowells 2y agoWhoops. Need to replace that abs with a max 1. Otherwise it doesn't Always terminate. Remember to check your boundary conditions!