On Sat, Jun 6, 2015 at 11:04 AM, Keean Schupke <[email protected]> wrote: > On 6 Jun 2015 11:46, "Matt Oliveri" <[email protected]> wrote: >> >> What you describe sounds like the intersection of functions on int >> >> with functions on float. This does not tell us what the intersection >> >> of int and float is. There are multiple subtype orders that are >> >> sensible. I was thinking of int and float as unrelated, so their >> >> intersection is empty. >> > >> > Consider: >> > >> > f : Int /\ Float -> String >> >> Consider it considered. What's the point? Do you still deny that (Int >> /\ Float) can be defined as empty? > > Int /\ Float can be either type but you may not be able to do any operations > on it. You still have to propagate it through functions like 'id'. So this > type is definitely inhabited.
I think you're thinking of (Int \/ Float) (union). An element of (Int \/ Float) is either an Int or a Float, and we don't know which. So when using one, we can only do things that are safe for both. An element of (Int /\ Float) has to simultaneously be an Int and a Float. It seems simplest to consider Int and Float disjoint, so (Int /\ Float) is empty. But whether it's empty or not, the operations that are safe on (Int /\ Float) are all of the ones for Int as well as the ones for Float. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
