**isA**declarations. The sup/lub/join is

*Union*, the inf/glb/meet is

*Intersection*. Unions between otherwise unrelated types are new types created as required. The intersection is just the union of types below all the types being intersected. So, for some examples:

*Integer*

**isA**

*Rational*,

*Integer*

**isA**

*GaussianInteger*.

*Union*[

*Integer Rational*] is

*Rational*, but

*Union*[

*Integer String*] is a new type (with few properties, just the ability to extract one or other). And, of course,

*Intersection*[

*Rational GaussianInteger*] is

*Integer*. The intersection of unrelated types is the type

*Empty*, which has no values.

[notational note: list entries are separated by spaces. The parameter of Union and of Intersection is a set of types, but can be given as a list as I have done here (because, in a forgetful way,

*List X*

**convertsTo**

*Set X*). The / operator invoked below takes 2

*Integer*s and returns a

*Rational*.]

I've been following along, in a desultory way, with a Mathematics discussion (https://golem.ph.utexas.edu/category/2015/09/the_free_modular_lattice_on_3.html) where I learnt of the difference between a lattice (which has sups and infs for finite sets of members of the lattice) and a bounded lattice which also has sups and infs for an empty set of members. Things usually work better when you include these degenerate cases, so I thought: I wonder if I can make Wombat's type hierarchy into a bounded lattice.

It doesn't take much imagination to see that

*Union*[] is going to be

*Empty*. And then it is natural, looking at everything upside down, to see that

*Intersection*[] is the type

*Any*which is the

*Union*of all types.

Now consider the list [7 3/2 4/5]. What is this a list of? It is naturally a list of the

*Union*of the types of its elements. Since those types are

*Integer*and

*Rational*, the result is a

*List Rational*(as any ordinary mortal would expect).

So what is the type of the empty list []? The set of types of the members is the empty set. The

*Union*is thus type

*Empty*. So [] is a

*List Empty*. But we've seen that

*Empty*is below any other type

*X*, so

*Empty*

**isA**

*X*. So a

*List Empty*

**isA**

*List X*for any

*X*. Which is exactly what you need to allow the empty list to be used in the situations where one might want to use it.

And, of course, none has type Option(Empty), and explicit closures have type Any->Empty which isA any more appropriate procedure type you want to specify.

ReplyDeleteIt's interesting that Empty, which wasn't originally in the spec, is suddenly crucial.

I previously said: " (because, in a forgetful way, List X isA Set X) ". Of course isA is never forgetful: it must somehow remember. Corrected to "convertsTo".

ReplyDelete