Thanks you very much.
On 05/12/17 16:17, michael.norr...@data61.csiro.au wrote:
I’m afraid it depends.
There are at least three different options.
The obvious one is to use an option type in the range. This makes everything
very explicit, but can be quite ugly.
Another approach is to just use the normal function space, knowing that you
will have the intended domain provided “at some distance”. For example, define
a monoid type:
<| carrier : α set; opn : α -> α -> α; id: α |>
The third approach would more explicitly tie the domain into the type
representing the function value so that you might write
type_abbrev (“fn”, ``:(α -> β) # (α set)``)
If manipulating such values, you’d end up wanting to define what it means to
apply these, to compose them etc. I don’t know of any serious attempts to
follow this sort of approach through.
Michael
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
