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
- : int option = Some 2
</pre>
- The parentheses is the magic for telling Ocaml that the
- function to be defined (in this case, the name of the function
- is `*`, pronounced "bind") is an infix operator, so we write
- `m * f` or `( * ) m f` instead of `* m f`.
+The parentheses is the magic for telling Ocaml that the
+function to be defined (in this case, the name of the function
+is `*`, pronounced "bind") is an infix operator, so we write
+`m * f` or `( * ) m f` instead of `* m f`.
* Associativity: bind obeys a kind of associativity, like this:
- (m * f) * g == m * (fun x -> f x * g)
+ `(m * f) * g == m * (fun x -> f x * g)`
- If you don't understand why the lambda form is necessary, you need
- to look again at the type of bind. This is important.
+ If you don't understand why the lambda form is necessary (the "fun
+ x" part), you need to look again at the type of bind.
For an illustration of associativity in the option monad:
- : int option = Some 3
</pre>
- Of course, associativity must hold for arbitrary functions of
- type `'a -> M 'a`, where `M` is the monad type. It's easy to
- convince yourself that the bind operation for the option monad
- obeys associativity by dividing the inputs into cases: if `m`
- matches `None`, both computations will result in `None`; if
- `m` matches `Some n`, and `f n` evalutes to `None`, then both
- computations will again result in `None`; and if the value of
- `f n` matches `Some r`, then both computations will evaluate
- to `g r`.
+Of course, associativity must hold for arbitrary functions of
+type `'a -> M 'a`, where `M` is the monad type. It's easy to
+convince yourself that the bind operation for the option monad
+obeys associativity by dividing the inputs into cases: if `m`
+matches `None`, both computations will result in `None`; if
+`m` matches `Some n`, and `f n` evalutes to `None`, then both
+computations will again result in `None`; and if the value of
+`f n` matches `Some r`, then both computations will evaluate
+to `g r`.
* Right identity: unit is a right identity for bind. That is,
`m * unit == m` for all monad objects `m`. For instance,
different types. But if we generalize bind so that both arguments are
of type `'a -> M 'a`, then we get plain identity laws and
associativity laws, and the monad laws are exactly like the monoid
-laws (see <http://www.haskell.org/haskellwiki/Monad_Laws>).
+laws (see <http://www.haskell.org/haskellwiki/Monad_Laws>, near the bottom).
Monad outlook
though without explicitly using monads.
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";;`.
+To run it, download the file, start Ocaml, and say
+
+ # #use "intensionality-monad.ml";;
+
+Note the extra `#` attached to the directive `use`.
Here's the idea: since people can have different attitudes towards
different propositions that happen to have the same truth value, we