Well, listTheory and optionTheory (in HOL4) already have many monad-related definitions (there's a comment in optionScript.sml about "The Option Monad").
I wonder if my "map_option" (which is probably a bad name for it) can be made up out of the existing definitions. On 26 September 2015 at 21:59, Jeremy Dawson <jeremy.daw...@anu.edu.au> wrote: > Hi Ramana, > > Does it deserve a place in optionTheory? > > On its own, maybe it depends on what your use of it was. > > But it would always be good to see more monad-related stuff in theories, > and your function would come into the definition functions for the compound > monad 'a list option (as in my Isabelle theory file, > http://users.cecs.anu.edu.au/~jeremy/isabelle/2005/fgc/Dtc.thy > where it's called swap_tc (changing Term to SOME, NonTerm to NONE, set to > list)) > > As a matter of fact often monad related functions are found, in theories, > without the recognition of this. eg in SML. option structure, we have > val ('a, 'b) mapPartial = fn : ('a -> 'b option) -> 'a option -> 'b > option > val ('a, 'c, 'b) composePartial = fn : > ('a -> 'b option) * ('c -> 'a option) -> 'c -> 'b option > val 'a join = fn : 'a option option -> 'a option > which are all basically alternative ways of defining a monad > > I wonder if it would be worth putting monad-related definitions and > theorems in HOL theory files such as list, option? Then one might consider > extending this to certain compound monads. > > Cheers, > > Jeremy > > On 26/09/15 09:56, Ramana Kumar wrote: > >> Hi Jeremy, >> >> Thanks for the links and information. It's rather more than I was >> expecting. Do you (or anyone on list) think that function deserves a >> place (perhaps under a different name) in optionTheory? >> >> Cheers, >> Ramana >> >> On 25 September 2015 at 21:21, Jeremy Dawson <jeremy.daw...@anu.edu.au >> <mailto:jeremy.daw...@anu.edu.au>> wrote: >> >> Hi Ramana, >> >> It's rather a similar situation to what I wrote about in >> >> http://users.cecs.anu.edu.au/~jeremy/pubs/fgc/fgs/fgs.pdf >> >> and also >> >> http://users.cecs.anu.edu.au/~jeremy/pubs/fgc/cats/fgc.ps >> >> except that I seem to have used sets instead of lists (which I don't >> think should make a difference), and I seem to not have noticed that >> I was reinventing the standard option type. >> >> I used these types to represent a non-deterministic computation with >> the possibility of non-termination. >> >> For the 'a set option result type, a computation is regarded as >> (let's say) "unreliable" and so non-terminating, when there is only >> the possibility of non-termination. >> For the 'a option set result type, you are interested in the >> possible (terminating) results even when non-termination is also >> possible. >> >> Both types, ie, 'a option set, and 'a set option, are compound >> monads, and your function is a monad morphism, which is also used in >> a certain construction which can be used to prove that the latter is >> indeed a compound monad. >> >> Cheers, >> >> Jeremy >> >> >> On 20/09/15 18:08, Ramana Kumar wrote: >> >> Hi all, >> >> I think this must be some neat combination of category theory >> things. >> Does anyone know which? Or if it's already defined somewhere? >> >> val map_option_def = Define` >> (map_option [] = SOME []) ∧ >> (map_option (NONE::_) = NONE) ∧ >> (map_option (SOME x::ls) = >> case map_option ls of >> | SOME ls => SOME(x::ls) >> | NONE => NONE)`; >> >> Cheers, >> Ramana >> >> >> ------------------------------------------------------------------------------ >> _______________________________________________ >> hol-info mailing list >> hol-info@lists.sourceforge.net >> <mailto:hol-info@lists.sourceforge.net> >> https://lists.sourceforge.net/lists/listinfo/hol-info >> >> >>
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
