14 Assignment 14: Reduction and Types for Monads

This assignment just offers you two choices for dessert. Choose either to get bonus (or if you want more, do both of them!).

Just Dessert

1. Recall the three laws defined in valueM.rkt that every monad must obey:

   • left-identity:
     For any types α and β,
     for any values x : α and c : α -> [M β],
     the values (bind (unit x) c) : [M β] and (c x) : [M β] are equal.

   • right-identity:
     For any type α,
     for any value m : [M α],
     the values (bind m unit) : [M α] and m : [M α] are equal.

   • associativity:
     For any types α and β and γ,
     for any values m : [M α] and c1 : α -> [M β] and c2 : β -> [M γ],
     the values (bind (bind m c1) c2) : [M γ] and (bind m (lambda (x) (bind (c1 x) c2))) : [M γ] are equal.

   These laws can often be proven by simple equational reasoning. For instance, using the definition of state-monad in valueM.rkt, we can prove left-identity as follows:

   ; left-identity for state-monad

   (bind (unit x) c)

   = ; inline state-bind and state-unit

   ((lambda (m c)

   (lambda (s)

   (match (m s)

   (`(answer ,x ,s) ((c x) s)))))

   ((lambda (x)

   (lambda (s) `(answer ,x ,s)))

   x)

   c)

   = ; beta

   ((lambda (m c)

   (lambda (s)

   (match (m s)

   (`(answer ,x ,s) ((c x) s)))))

   (lambda (s) `(answer ,x ,s))

   c)

   = ; beta

   (lambda (s)

   (match ((lambda (s) `(answer ,x ,s)) s)

   (`(answer ,x ,s) ((c x) s))))

   = ; beta

   (lambda (s)

   (match `(answer ,x ,s)

   (`(answer ,x ,s) ((c x) s))))

   = ; match

   (lambda (s)

   ((c x) s))

   = ; eta

   (c x)

   Prove the three monad laws for the continuation monad cont-monad, by putting comments in your submission that follow the format above. Write out each beta or eta step separately. This work is not autograded.

2. As you saw in Assignment 12: Monads, types can guide us to write correct monadic programs, especially when we insist that our programs type-check for an arbitrary monad. For instance, below are two attempts at defining ifM:

   • (λ mb (λ mt (λ mf (bind mb (λ b (if b mt mf))))))

   • (λ mb (λ mt (λ mf (if mb mt mf))))

   But the second attempt can’t be right, because for an arbitrary monad M, the type [M Boolean] of mb does not match the type Boolean required by if.

   Similarly, in your definition of filterM, in the case where the input list is empty, you might have been tempted to return the empty list. But for an arbitrary monad M, the type of the empty list does not match the required return type [M [ListOf α]]. That’s why the correct return value is not the empty list, but unit of the empty list.

   To mechanize this guidance, let’s extend our type system to handle an arbitrary monad:

   Expr		=		(unit Expr)
   		|		(bind Expr Expr)
   Type		=		(Type monad)

   For instance, only the first attempt above at defining ifM has the type ((bool monad) -> ((num monad) -> ((num monad) -> (num monad)))). And with the previous assignment’s dessert, the following definition of filterM

   (rec filterM f

   (λ lst

   (lcase lst

   (unit (null))

   x xs (bind (f x)

   (λ b (if b

   (bind ((filterM f) xs)

   (λ ys (unit (cons x ys))))

   ((filterM f) xs)))))))

   has the type ((num -> (bool monad)) -> ((num list) -> ((num list) monad))), but it no longer type-checks if we change (unit (null)) to (null).

   Define and test a function inference-ok-monad? that takes a Proof and determines whether its root is a valid inference for the type of a unit or bind expression. Check just the root inference, not how the premises are themselves proven.