[seanmcdirmid]

> An infinite algebraic type lattice that confers a distinct type upon every distinct value. Intrinsic support for a rich collection of immutable types, including tuples, sets, maps, functions, and continuations.

Ok, I consider myself OK at type theory but I'm still lost in what this claim actually means. And if it is what I think it is (that all values have types), I wonder how this doesn't run afoul of decidability of fancy dependent type systems (perhaps 1 has a type, 2 has a type, but 1 + 2's type isn't 3?).

[tathougies]

Avail does not seem to have dependent types. The term 'dependent type' is overused. It means that the type system must allow the compile-time type of an expression to depend on the run-time value. This is not totally decidable. Most type systems, including advanced ones, such as Haskell's, do not have this property. Avail seems no different.

[markvangulik]

Haskell has infinite and recursive constructs, lazily computed. That’s what makes their type system undecidable. Avail is constructivist in that sense, so immutable structures must be finite (i.e., you can draw them as a dag). For cyclic structures, you have to include mutable “variable” objects as well, but in that case the type of the construct stops at the boundary of the variable. The type of a tuple of variables is a composition of the declared types of the variables, not their current content. This is essential to ensure an object’s type is permanent, and the immutable acyclicity condition ensures everything reachable without hitting a variable contributes to an object’s type.

[tome]

> Haskell has infinite and recursive constructs, lazily computed. That’s what makes their type system undecidable.

Haskell (98) has infinite and recursive constructs and its type system is not undecidable.

[tathougies]

Haskell has infinite and recursive types but its type system is perfectly decidable, mainly because Haskell's type system is nominal, so cycles are easily detected and dealt with.

[pubby]

IIRC, semilattices in type systems usually means subtypes, and lattices in type systems usually means subtypes plus a bottom type.

[markvangulik]

Yes, that agrees with the shape of Avail’s type hierarchy. There’s a top type and a bottom type, and the latter has no instances.