use a container metaphor: if `x` has type `int option`, then `x` is
a box that (may) contain an integer.
- type 'a option = None | Some of 'a;;
+ `type 'a option = None | Some of 'a;;`
* A way to turn an ordinary value into a monadic value. In Ocaml, we
did this for any integer n by mapping an arbitrary integer `n` to
the option `Some n`. To be official, we can define a function
called unit:
- let unit x = Some x;;
- val unit : 'a -> 'a option = <fun>
+ `let unit x = Some x;;`
+
+ `val unit : 'a -> 'a option = <fun>`
So `unit` is a way to put something inside of a box.
* A bind operation (note the type):
- let bind m f = match m with None -> None | Some n -> f n;;
- val bind : 'a option -> ('a -> 'b option) -> 'b option = <fun>
+ `let bind m f = match m with None -> None | Some n -> f n;;`
+
+ `val bind : 'a option -> ('a -> 'b option) -> 'b option = <fun>`
`bind` takes two arguments (a monadic object and a function from
ordinary objects to monadic objects), and returns a monadic
Then the second argument uses `x` to compute a new monadic
value. Conceptually, then, we have
- let bind m f = (let x = unwrap m in f x);;
+ `let bind m f = (let x = unwrap m in f x);;`
The guts of the definition of the `bind` operation amount to
specifying how to unwrap the monadic object `m`. In the bind
All of the code in the discussion below can be found here: [[intensionality-monad.ml]].
To run it, download the file, start Ocaml, and say `# #use
-"intensionality-monad.ml"`.
+"intensionality-monad.ml";;`.
Here's the idea: since people can have different attitudes towards
different propositions that happen to have the same truth value, we