To take a trivial (but, as we will see, still useful) example,
consider the Identity box type: `α`. So if `α` is type `bool`,
-then a boxed `α` is ... a `bool`. In terms of the box analogy, the
-Identity box type is a completely invisible box. With the following
+then a boxed `α` is ... a `bool`. That is, <code><u>α</u> = α</code>.
+In terms of the box analogy, the Identity box type is a completely invisible box. With the following
definitions:
mid ≡ \p. p
Identity is a monad. Here is a demonstration that the laws hold:
- mcomp mid k == (\fgx.f(gx)) (\p.p) k
- ~~> \x.(\p.p)(kx)
- ~~> \x.kx
- ~~> k
- mcomp k mid == (\fgx.f(gx)) k (\p.p)
- ~~> \x.k((\p.p)x)
- ~~> \x.kx
- ~~> k
- mcomp (mcomp j k) l == mcomp ((\fgx.f(gx)) j k) l
- ~~> mcomp (\x.j(kx)) l
- == (\fgx.f(gx)) (\x.j(kx)) l
- ~~> \x.(\x.j(kx))(lx)
- ~~> \x.j(k(lx))
- mcomp j (mcomp k l) == mcomp j ((\fgx.f(gx)) k l)
- ~~> mcomp j (\x.k(lx))
- == (\fgx.f(gx)) j (\x.k(lx))
- ~~> \x.j((\x.k(lx)) x)
- ~~> \x.j(k(lx))
-
-The Identity Monad is favored by mimes.
+ mcomp mid k ≡ (\fgx.f(gx)) (\p.p) k
+ ~~> \x.(\p.p)(kx)
+ ~~> \x.kx
+ ~~> k
+ mcomp k mid ≡ (\fgx.f(gx)) k (\p.p)
+ ~~> \x.k((\p.p)x)
+ ~~> \x.kx
+ ~~> k
+ mcomp (mcomp j k) l ≡ mcomp ((\fgx.f(gx)) j k) l
+ ~~> mcomp (\x.j(kx)) l
+ ≡ (\fgx.f(gx)) (\x.j(kx)) l
+ ~~> \x.(\x.j(kx))(lx)
+ ~~> \x.j(k(lx))
+ mcomp j (mcomp k l) ≡ mcomp j ((\fgx.f(gx)) k l)
+ ~~> mcomp j (\x.k(lx))
+ ≡ (\fgx.f(gx)) j (\x.k(lx))
+ ~~> \x.j((\x.k(lx)) x)
+ ~~> \x.j(k(lx))
+
+The Identity monad is favored by mimes.
To take a slightly less trivial (and even more useful) example,
consider the box type `α list`, with the following operations:
mapply gs xs ==> [49, 25, 14, 10]
-As we illustrated in class, there are clear patterns shared between lists and option types and trees, so perhaps you can see why people want to identify the general structures. But it probably isn't obvious yet why it would be useful to do so. To a large extent, this will only emerge over the next few classes. But we'll begin to demonstrate the usefulness of these patterns by talking through a simple example, that uses the Monadic functions of the Option/Maybe box type.
+As we illustrated in class, there are clear patterns shared between lists and option types and trees, so perhaps you can see why people want to identify the general structures. But it probably isn't obvious yet why it would be useful to do so. To a large extent, this will only emerge over the next few classes. But we'll begin to demonstrate the usefulness of these patterns by talking through a simple example, that uses the monadic functions of the Option/Maybe box type.
## Safe division ##
But we can automate the adjustment, using the monadic machinery we introduced above.
As we said, there needs to be different `>>=`, `map2` and so on operations for each
-Monad or box type we're working with.
+monad or box type we're working with.
Haskell finesses this by "overloading" the single symbol `>>=`; you can just input that
symbol and it will calculate from the context of the surrounding type constraints what
monad you must have meant. In OCaml, the monadic operators are not pre-defined, but we will
material within the sentence can satisfy presuppositions for other
material that otherwise would trigger a presupposition violation; but,
not surprisingly, these refinements will require some more
-sophisticated techniques than the super-simple Option monad.)
+sophisticated techniques than the super-simple Option/Maybe monad.)