* On Thu, Feb 12 2009, Michael G Schwern wrote: > chromatic wrote: >> On Thursday 12 February 2009 14:09:41 Michael G Schwern wrote: >> >>> I hope somebody writes a provable kernel. >> >> Why? It would be practically useless unless they proved all cases of input >> (user and hardware), in which case it would only be practically useless for >> every case which lacks complete proofs. > > I'm no expert, but I'm given to understand this exactly the problem Monads > were developed to deal with.
No, monads exist to abstract away the sequencing of computations. In perl, we use the ";" to sequence computations, which is a function of two arguments that executes the first argument, and then executes the (optional) second argument. Monads generalize this concept and let you make ";" behave differently for different types of arguments. (There are some mechanics involved, but this is the basic idea.) An example: http://www.haskell.org/all_about_monads/html/meet.html mothersPaternalGrandfather :: Sheep -> Maybe Sheep mothersPaternalGrandfather s = case (mother s) of Nothing -> Nothing Just m -> case (father m) of Nothing -> Nothing Just gf -> father gf See the repeated "Nothing / Just" block? (Before we do the next computation, we see if the previous on returned Nothing. If it did, we don't do the nexe computation). If we define a monad over the type of function that returns "Maybe" (Nothing / Just), then we can rewrite this as: mothersPaternalGrandfather s = do { m <- mother s; gf <- father m; father gf } Now the redundant check is gone. The ";" operator does it for us. (The compiler knows that we want this behavior because `mother` and `father` return values of the type Maybe.) So sorry, nothing to do with proving the correctness of software. Just another way to abstract away common code. We don't use Monads in Perl because they only save typing if you have type inference, and because we don't have the syntax sugar that Haskell does. We can do the same thing in a different way. (In this case, block eval works. If we call a method on undef, the block exits, returning undef.) Regards, Jonathan Rockway -- print just => another => perl => hacker => if $,=$"
