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