证明单子第一定律

Question

给定：

module FunMonad = struct
  type 'a t = (unit -> 'a)
  let return x = fun () -> x
  let bind m f = fun () -> ((f (m ())) ())
  (* explain why not: let bind m f = f (m ()) *)
  let (>>=) = bind
  end

module ListMonad = struct
  type 'a t = 'a list
  let return x = [x]
  let bind m f = List.concat (List.map f m) 
  let (>>=) = bind
  let zero = [] 
  let (++) = List.append

我想证明前两个单子定律，这是我所做的：

(* thunk: 证明*)

(* 法则 1:

(return x) >>= f ⇔ f x

*)

(* 所以:

fun () -> x >>= f ⇔ fun () -> ((f (x)) ()) = fun () -> (x) = f x

*)

(* 法则 2:

m >>= return ⇔ m

*)

(* 所以:

fun () -> x >>= return ⇔ fun () -> (return (x) ()) = fun () -> ((fun () -> x) ()) = fun () -> x = m

*)

(* 列表：证明*)

(* 法则 1:

(return x) >>= f ⇔ f x

*)

(* 所以:

[x] >>= f ⇔ List.concat (List.map f [x]) = ?

*)

(* 法则 2:

m >>= return ⇔ m

*)

(* 所以:

[x] >>= return ⇔ List.concat (List.map return [x]) = List.concat ([[x]]) = [x] = m

*)

但是我对列表的定律1有疑问，如何证明？