> 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.
Cannot 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.
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.