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