From 5f8ea7e4c56ab00888ca59c5ba0fb6e3d5d5a65c Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Wed, 1 Dec 2010 03:46:37 -0500 Subject: [PATCH] manip trees: tweaks Signed-off-by: Jim Pryor --- manipulating_trees_with_monads.mdwn | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/manipulating_trees_with_monads.mdwn b/manipulating_trees_with_monads.mdwn index a05fa259..69b5131e 100644 --- a/manipulating_trees_with_monads.mdwn +++ b/manipulating_trees_with_monads.mdwn @@ -280,7 +280,7 @@ interesting functions for the first argument of `treemonadizer`: We could simulate the tree state example too, but it would require generalizing the type of the continuation monad to - type ('a -> 'b -> 'k) continuation = ('a -> 'b) -> 'k;; + type ('a, 'b, 'c) continuation = ('a -> 'b) -> 'c;; The binary tree monad --------------------- @@ -297,29 +297,29 @@ monad, the binary tree monad: For once, let's check the Monad laws. The left identity law is easy: - Left identity: bind (unit a) f = bind (Leaf a) f = fa + Left identity: bind (unit a) f = bind (Leaf a) f = f a To check the other two laws, we need to make the following observation: it is easy to prove based on `tree_bind` by a simple induction on the structure of the first argument that the tree resulting from `bind u f` is a tree with the same strucure as `u`, -except that each leaf `a` has been replaced with `fa`: +except that each leaf `a` has been replaced with `f a`: \tree (. (fa1) (. (. (. (fa2)(fa3)) (fa4)) (fa5))) . . __|__ __|__ | | | | - a1 . fa1 . + a1 . f a1 . _|__ __|__ | | | | - . a5 . fa5 + . a5 . f a5 bind _|__ f = __|__ | | | | - . a4 . fa4 + . a4 . f a4 __|__ __|___ | | | | - a2 a3 fa2 fa3 + a2 a3 f a2 f a3 Given this equivalence, the right identity law @@ -344,18 +344,18 @@ proceed. Let `f a = Node (Leaf a, Leaf a)`. Then . . | | bind __|__ f = __|_ = . . | | | | __|__ __|__ - a1 a2 fa1 fa2 | | | | + a1 a2 f a1 f a2 | | | | a1 a1 a1 a1 Now when we bind this tree to `g`, we get - . - ____|____ - | | - . . - __|__ __|__ - | | | | - ga1 ga1 ga1 ga1 + . + _____|______ + | | + . . + __|__ __|__ + | | | | + g a1 g a1 g a1 g a1 At this point, it should be easy to convince yourself that using the recipe on the right hand side of the associative law will -- 2.11.0