A lattice is a partial ordering where any two elements have a supremum and infinum. I.E., for any two types in avail's lattice, there is a unique super type, and a unique sub type. A partial ordering means that -- given any two elements -- I can say that either one is a subtype of the other or that the types are not in relation. The super type of every type is known as 'top', and the sub type of every type is known as 'bottom'. An infinite lattice just means that there is an infinite amount of types in the Avail type system.

Well said, that’s exactly right. Most languages lack a bottom type, or screw it up by pretending that “null” fits that role and falsely promises everything that every other type promises.

Languages like Java (and many more) fail to even have a top type, which leads to kludgey add-ons to the type system — boxed, @Nullable, erased generics, annotations, dependency injection, purity annotations, etc., all of which should have been part of a single type system.

I forgot to add the interfaces versus classes, inner classes, and lambda notation, with the tons of trivial FunctionalInterface interfaces to deal with a smattering of the combinations of number of inputs, void or primitive or class output, which inputs or inputs can be null, and which exceptions can be thrown by the evaluation method (having many different names, etc).

Almost all of these monstrosities are caused by the “object purity” mindset that kept the designers from including first-class functions in the language. Avail attempts to include a large set of paradigms instead of trying to “axiomatize” the exposed surface (although we do axiomatize the construction of these constructs).

FWIW, latices are a pretty easy concept once you grok the basic idea.

I first encountered them when doing work-related reading on dataflow analysis, and I'm very glad I did. Interesting stuff.

(edit) Summary: the topic might look scary at first blush, but it's actually not.

It’s a big concern, but technically most of the world doesn’t actually use ASCII. We use shortcuts in IntelliJ (and Eclipse before that), so if you want a right arrow, you type “rig”, pause a split second, and hit return to accept the “rightarrow” suggestion, which it replaces with a real right arrow. It’s as easy to use in that environment as any other kind of autocompletion.

Here is an infinite lattice (roughly speaking):

            o
            /\
           o  o
          /\  /\
         o  o  o
        /\ /\  /\
       o  o   o  o
      /\ /\  /\  /\
     o  o  o   o   o
    ...   ...   ...