On 09/04/13 14:40, Albert Y. C. Lai wrote: > This can be written in Haskell as:
> do {
> q0 <- x/y;
> q1 <- b/c;
> return (q0 + q1)
> }
If you have defined / to return options as Albert suggests, the above can be
mimicked with HOL4's support for monad syntax.
You'd need to
open monadsyntax
val _ = overload_on ("monad_bind", ``OPTION_BIND``)
val _ = overload_on ("monad_unitbind", ``OPTION_IGNORE_BIND``)
val _ = overload_on ("return", ``SOME``)
but could then write
``do
q0 <- x/y;
q1 <- b/c;
return (q0 + q1)
od``
This makes functional programming with options in HOL a great deal nicer!
I don't know of any serious attempt to pursue more mathematical applications in
this style.
Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ 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
