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 > 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
