In System F I can define the genuine total addition function using Church numerals.

In Haskell I cannot define that function because of the bottom value. For example, in haskell if x + y = x, then I cannot say that y is zero - if x is bottom, x + y = x for any y. So the addition is not the true addition but an approximation to it.

In C I cannot define that function because C specification requires everything to have finite size. So in C possible approximations are even worse than in Haskell.

So we have:

In System F it's possible to define the addition but it's not possible to have a complete implementation (because there are no infinite hardware).

In Haskell it's not possible to define the addition (because of the bottom), and it's not possible to have a complete implementation.

In C it's not possible to define the total addition function (because semantic of everything is bounded) but compliant implementations are possible.

So all 3 formal systems (Haskell, System F and C) seem to have different design tradeoffs.

So what are consequences of choosing one over another?

`pow(2, 8 * sizeof(size_t))`

bytes but you can just chain those if you have hardware that has enough memory.`x + y = x`

problem because`y`

can be infinitely recursive.