1

根据Curry-Howard 对应，sum-type aka tagged-union 相当于析取，逻辑 OR

为什么会这样？不是更接近异或吗？(a or b)意味着它可以是aorb或both，而Either a b必须是aorb但绝不是两者。

4

1 回答 1

1

Curry-Howard 对应说 的元素Either a b代表的证明。a or b为了证明析取，证明（提供一个元素）a或就足够了b。您可以通过Either a b使用Left a或构造来做到这一点Right b。

于 2022-01-16T07:32:31.150 回答