在 System FI 中，可以使用 Church 数字定义真正的总加法函数。
在 Haskell 中，由于底部值，我无法定义该函数。例如，在 haskell 中，如果 x + y = x，那么我不能说 y 为零 - 如果 x 是底部，对于任何 y，x + y = x。所以加法不是真正的加法，而是它的近似值。
在 CI 中无法定义该函数，因为 C 规范要求所有内容都具有有限的大小。所以在 C 中可能的近似值甚至比在 Haskell 中更糟糕。
所以我们有：
在 System F 中，可以定义加法，但不可能有完整的实现（因为没有无限的硬件）。
在 Haskell 中，不可能定义加法（因为底部），也不可能有完整的实现。
在 C 中，不可能定义总加法函数（因为一切的语义都是有界的），但兼容的实现是可能的。
因此，所有 3 个正式系统（Haskell、System F 和 C）似乎都有不同的设计权衡。
那么选择一个而不是另一个的后果是什么？
You have a set of theories as frameworks to do your reasoning with; finite reality, Haskell semantics, System F are just ones of them.
You can choose appropriate theory for your work, build new theory from scratch or from big pieces of existing theories gathered together. For example, you can consider set of always terminating Haskell programs and employ bottomless semantics safely. In this case your addition will be correct.
For low level language there may be considerations to plug finiteness in but for high level language it is worth to omit such things because more abstract theories allow wider application.
While programming, you use not "language specification" theory but "language specification + implementation limitations" theory so there is no difference between cases where memory limits present in language specification or in language implementation. Absence of limits become important when you start building pure theoretic constructions in framework of language semantics. For example, you may want to prove some program equivalences or language translations and find that every unneeded detail in language specification brings a much pain in proof.
相信大家都听过这样一句格言：“理论上，理论与实践没有区别，但在实践中是有区别的”。
在这种情况下，理论上存在差异，但所有这些系统都处理相同的有限数量的可寻址内存，因此在实践中没有区别。
编辑：
假设您可以在这些系统中的任何一个中表示自然数，您可以在其中任何一个中表示加法。如果您担心的约束阻止您表示自然数，那么您不能表示 Nat*Nat 加法。
将自然数表示为一对（最大位大小的启发式下限和延迟评估的位列表）。
在 lambda 演算中，您可以将列表表示为一个函数，该函数返回一个以 true 调用返回 1 位的函数，以 false 调用返回一个对 2 位执行相同操作的函数，依此类推。
然后，加法是应用于传播进位位的这两个惰性列表的 zip 的操作。
您当然必须将最大位大小启发式表示为自然数，但如果您只实例化位数严格小于您所表示的数字的数字，并且您的运算符不会破坏该启发式，那么位size 是一个比您要操作的数字更小的问题，因此操作终止。
关于考虑边缘情况的难易程度，C 对你的帮助很少。您可以返回特殊值来表示上溢/下溢，甚至尝试使它们具有传染性（如 IEEE-754 NaN），但如果您未能检查，您将不会在编译时收到投诉。您可以尝试重载信号 SIGFPE 或类似陷阱问题的东西。
我不能说 y 为零 - 如果 x 是底部，则对于任何 y，x + y = x。
如果您希望进行符号操作，Matlab 和 Mathematica 是用 C 和 C 类语言实现的。也就是说，python 有一个优化良好的 bigint 实现，可用于所有整数类型。不过，它可能不适合表示非常大的数字。