On 13-04-05 01:50 AM, Cris Perdue wrote: > Thanks for your input on this. Are there some examples in HOL or HOL > Light where the approach you suggest with option types is used? [...] > On Thu, Apr 4, 2013 at 4:28 PM, Vincent Aravantinos > <vincent.aravanti...@gmail.com <mailto:vincent.aravanti...@gmail.com>> > wrote: > > In my opinion, the best way of dealing with this is to use option > types: None denoting the undefined value. This makes function > composition tedious but you can use a monad to make this easier. > > Now, it is not standard w.r.t. usual maths. But I'm not sure whether > usual maths are doing this the right way...
I offer to show examples. I will use pseudocode that is a mixture of HOL notation, ML notation, and Haskell notation, and just hope that you guess what I mean. Unfortunately, no actual code I know of has done this or gone this far. (That is, even in Haskell with its syntactic help for monads, partial functions in its standard library do not use option types, e.g., head is still 'a list -> 'a, not 'a list -> 'a option. Naturally, quite some people lament it.) We give division this type / : real * real -> real option and at least these theorems x / 0 = NONE y != 0 ==> ?q. (x / y = SOME q) /\ (x = y*q) Whereas in math we write x/y + b, x/(y/z), and x/y + b/c, here we have to write: case x/y of NONE => NONE | SOME q => SOME (q + b) case y/z of NONE => NONE | SOME q1 => x/q1 case x/y of NONE => NONE | SOME q0 => case b/c of NONE => NONE SOME q1 => SOME (q0 + q1) Whew! But there are several ways of abstracting (re-factoring?) out some of the boilerplate. Here is what Wadler suggests (but with Haskell's names and ML's types): return : 'a -> 'a option return x = SOME x >>= : 'a option * ('a -> 'b option) -> 'b option NONE >>= whatever = NONE SOME x >>= kont = kont x >>= is usually called "bind". Its motivation and English name are explained right after the following examples. Using them, expressions can be written with a bit less clutter: x/y >>= \q. return (q + b) y/z >>= \q1. x/q1 x/y >>= \q0. b/c >>= \q1. return (q0 + q1) >>= is analogous to "let" in this sense: y/z >>= \q1. x/q1 is analogous to let q1 = y/z in x/q1 This analogy motivates postulating >>= to play the role of let-binding. We can state and prove theorems like this one, which is roughly "x/(y/z) = x*z/y": z != 0 ==> (y/z >>= \q1. x/q1) = x*z/y We can define more functions based on return and >>= to capture some common patterns, e.g., inspired by "x/y + b/c": liftM2 : ('a * 'b -> 'c) -> 'a option -> 'b option -> 'c option liftM2 binop d0 d1 = d0 >>= \q0. d1 >>= \q1. return (binop (q0,q1)) This helps us write: "x/y + b/c" = liftM2 (op +) (x/y) (b/c) "(x/y) min (b/c)" = liftM2 (op min) (x/y) (b/c) which is not too shabby. Haskell goes further by providing syntactic support for >>=. Recall the earlier x/y >>= \q0. b/c >>= \q1. return (q0 + q1) This can be written in Haskell as: do { q0 <- x/y; q1 <- b/c; return (q0 + q1) } So, we have the polymorphic type "option" (note: I do not say 'a option, I say option), together with the functions return and >>=. We can verify that they satisfy these theorems: return x >>= f = f x m >>= return = m (m >>= f) >>= g = m >>= (\v. f v >>= g) (v is a fresh variable, beware of name clash etc) When these all happen, option is a monad. This is how monad is brought up, but monad is very general (various examples look very different) and we only use option specifically. So this is how things may look like if you replace partial functions by total functions with options. ------------------------------------------------------------------------------ Precog is a next-generation analytics platform capable of advanced analytics on semi-structured data. The platform includes APIs for building apps and a phenomenal toolset for data science. Developers can use our toolset for easy data analysis & visualization. Get a free account! http://www2.precog.com/precogplatform/slashdotnewsletter _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info