关于Option Monad定律证明的疑问：为何定律1无需考虑None情况？

1. Option Monad 的 OCaml 实现 #

module OptMonad = 
  struct
    type 'a t = 'a option
    let return v = Some v
    let bind m f = 
      match m with
      | Some v -> f v
      | None -> None
    let (>>=) = bind (* as always *)
  end

2. 需要证明的两个单子定律 #

• 定律1: (return x) >>= f ⇔ f x
• 定律2: m >>= return ⇔ m

3. 已完成的推导过程 #

• 对于定律1：return x = Some x, so: Some x >>= f ⇔ f x
• 对于定律2：
  • Case 1: m = Some x，因此 Some x >>= return ⇔ Some x = m
  • Case 2: m = None，因此 None >>= return ⇔ None = m

4. 疑问解答 #

证明定律1时不需要考虑None的核心原因是：return x的结果是固定的Some x，根本不会产生None。

根据OptMonad中return的定义，return v的实现就是直接返回Some v，不存在任何能让return x变成None的情况。所以定律1的左式(return x) >>= f只会对应bind函数中m = Some x的分支，自然不需要讨论None场景。

而定律2中的m是任意的'a option类型值，它既可能是Some x也可能是None，所以必须分两种情况验证等式成立。

内容的提问来源于stack exchange，提问作者v_head