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
> <[email protected] <mailto:[email protected]>>
> 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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
