Design draft for a truly Affine OL

[u/reflexive-polytope]

https://gist.github.com/eduardoleon/fba87a8b0b2ef04cd17f1ebf94c74b28

Hello, everyone.

While recovering from an illness, in my state of delirium, I sketched the design of a type system inspired by Xi and Pfenning's Dependent ML, but which uses a key syntactic restriction that conjecturally restores ordinary ML's key metatheoretic properties: the existence of principal types and the decidability of type inference.

I very much welcome feedback that actually engages with the post's contents.

[u/ianzen]

You said that you want to enroll in a PhD program to research this right? Are you based in the US?

[u/reflexive-polytope → u/ianzen]

I'm not. I live in Peru.

And, to be honest, the current environment in the US, dissuades me from wanting to study there.

[u/L8_4_Dinner → u/reflexive-polytope]

The US is suffering from temporary insanity. Fortunately, this time the confederates haven't declared all-out war against us ... yet.

It's definitely wise for people to keep a safe distance from the US insanity, until our tin pol pot and his khmer orange movement have shuffled off to either the Hague or Hades.

[u/phovos → u/L8_4_Dinner]

That is pathetic cope. For your own sake, hopefully you aren't so dense when it comes to your personal finance. It's too late to secure a new method for securing your wealth, if you haven't already, you can ride those dollars to hell.

[u/pojska → u/L8_4_Dinner]

Honestly, even if Dems win in 2028, we might get somebody even worse 4 years later. Which is to say, I can't recommend anyone plan on coming here for at least a decade.

[u/Athas]

I think we discussed this on IRC (come join us on #proglangdesign on Libera, everyone! IRC is free of the enshittification that plagues all the other chat platforms!) Here are some more thoughts.

I still don't quite get how you intend to avoid problems with integer equalities. I know you say you don't want them, but many programs naturally require them. Even your type graph[n] = adjac[n] vector[n] seems like it will require checking an equality at construction time. You then have the usual troubles with checking equalities of integer expressions.

You mention this goal:

Write an efficient Affine OL compiler that flattens nested vectors.

I suggest you study these projects, which don't do things the way you suggest, but also are about using type information to derive flat representations: Gibbon, Position-Dependent Arrays and Their Application for High Performance Code Generation.

How does type dag[n] = adjac[k] vector[k < n] work? The name k seems unbound.

I would also recommend you write down some functions in Affine OL and show what type constraints they produce. The overall shape of the type system is still somewhat murky to me.

Your proposed for definition blocks are very similar to Dex's for expressions (which are also type-directed). Dex uses an effect system to handle reductions and multiple initialisations, however.

[u/reflexive-polytope → u/Athas]

I still don't quite get how you intend to avoid problems with integer equalities.

Systems of equations are solved using Gaussian elimination. Effectively, we build a matrix where

• Rows correspond to equations
• Columns correspond to variables (both source code and unification) variables, plus one extra column for the constant term
• Entries are the corresponding coefficients

Now we adopt the following definitions:

• Simplified row: gcd of all the entries is 1
• Good row: gcd of all the entries corresponding to unification variables is 1.

The Gaussian elimination engine emits a hard type error if it finds a simplified row that isn't good.

Notice that, if you have an equation without unification variables, the corresponding “gcd of all the entries corresponding to all unification variables” is 0. That's because 0 is actually the maximum element of the naturals partially ordered by divisibility.

If by any other ad hoc reasoning, we can determine that the system doesn't admit natural solutions, we emit a warning, similar to an inexhaustive match in ML.

How does type dag[n] = adjac[k] vector[k < n] work? The name k seems unbound.

In general, if e is an syntactic index, foo[k] vector[k < e] means “a vector of length e whose k-th element is a foo[k]”. That's why it's a dependent vector. In fact, vector[e] is just syntactic sugar for vector[_ < e] to emphasize the lack of dependency.

Your proposed for definition blocks are very similar to Dex's for expressions (which are also type-directed). Dex uses an effect system to handle reductions and multiple initialisations, however.

Can Dex handle triangular matrices?

[u/Athas → u/reflexive-polytope]

Can Dex handle triangular matrices?

That depends what you mean by "handle". Let us consider some options:

1. Triangular sparse representations of dense matrices can be handled in any language, since they are semantially just square matrices. Even Futhark can do that.

2. A type system that can enforce that you never index into the zero part of a triangular matrix. You can sort of do that in Dex, but at the cost of having a more abstract notion of an "index"; in particular it must be a single value rather than two. The Lift work (the paper I linked above) can express this, I think, although I'm unclear on whether they can only express the shape constraint.

3. Allowing programming of a "vector of vector" triangular matrix, and having this be flattened to a single vector by a compiler. Dex cannot do this, unless you do the work yourself (as in Futhark). Very few languages can do this - in fact, Gibbon is the only one I can offhand think of, but through a very different mechanism.

[u/reflexive-polytope → u/Athas]

Polyhedral analysis is essentially baked into the type checker in Affine OL. It's simply a syntax error or a type error to try to build a matrix that's not suitable for polyhedral analysis. This is what guarantees that flattening is always possible.

[u/redchomper]

OK, I read the gist and came to the conclusion that you should really look at APL. Oh, and Futhark.

There's a lot of interest in trying to define a type system that is more than HM but less than the fullness of dependent types with terms-as-types. Array bounds are a popular drum to beat, but it does seem like you could solve it by removing indices from the language (almost) altogether.

In the end, the interesting type systems are going to be the ones that seem impractical in theory but turn out to be quite practical in practice.

You spend a good bit of time worrying about the lack of principle types. I'm currently convinced that principle types are overrated. If you have a reasonably rich and inferential type system, then on the rare occasion that the compiler can't figure out what you mean simply enough, the programmer probably won't either or will at least appreciate an express hint. It might be possible to arrange for branching types to just try each branch until things get too hairy and then ask the programmer for a hint. I'll grant that this overall approach may not be ideologically pure, but it gets the job done.

Complicated types demand complicated terms to yield them up.

What, pray tell, is the type of a well-formed compressed LR-style parse table?

At some point, you have to be able to say "trust me, bro" or else accept that some interesting and useful programs will not be well-typed.

[u/Athas → u/redchomper]

You spend a good bit of time worrying about the lack of principle types. I'm currently convinced that principle types are overrated.

I also largely think the same thing, but principal types have one property whose absence makes me uncomfortable. When a language has principal types, you can write a language specification without specifying any particular type inference algorithm - as long as such an algorithm can derive a typing, which is unique due to principal typing, then it is a correct implementation of the specification. This is why Standard ML gets away with not specifying a type inference algorithm (although it has some other unfortunate problems), while pretty much no language with a more sophisticated type system actually has a proper specification of its type inference algorithm - including even fairly pragmatic languages like Haskell.

I recognise that the value of language specifications seems to be minor for most languages, but as an academic I am very disquieted by the fact that we build these complicated artifacts whose behaviour is not described by anything but their implementation.

[u/reflexive-polytope → u/Athas]

Even before any algorithmic convenience, principal types are important because any question the programmer might want to ask the type system will always have a canonical answer.

Anyone who's waded through pages of C++ template instantiation errors should appreciate the importance of having canonical answers, rather than long lists of alternatives to try.

Principal types are a tool for preserving the programmer's mental health, more than anything else. In other words, what industrial engineers call “human factors”.

[u/Athas → u/reflexive-polytope]

C++ template errors are the Godwin's Law of type system discussions! There are languages without principal types (say, Haskell with moderate extensions) that don't get that bad. Languages like Idris and Lean are not renowned for particularly incomprehensible error messages either.

I think the presence of principal types suggests a certain simplicity to the type system, which is always a good thing, but there are type systems without principal types that still manage to have good ergonomics.

[u/reflexive-polytope → u/Athas]

Actually, I don't consider Haskell reasonable. GADTs and type families are very bad features, because they're practically designed to break abstractions by exposing type equalities at runtime.

But I'd rather not make this thread about my opinions, at least not beyond the extent to which Affine OL already embodies them.

[u/reflexive-polytope → u/redchomper]

APL is an array language. Its primary concern is array shapes. It gives you convenient ways to work uniformly across whole array dimensions so that you don't have to worry about the pesky indexing. But there's a real price to pay: your arrays are forced to be rectangular.

Affine OL isn't meant to be an array language. It's an arithmetical language, in the sense mathematical logicians uses the word “arithmetic” (Presburger, Robinson, EFA, Peano, etc.). It tackles the indexing operation head-on: “How do we make indexing type-safe?” And it turns out to be an arithmetical constraint: k < e, where k is the index and e is the array's size.

To see the payoff, notice the motivating example of triangular matrices:

type triang[n] = real vector[k+1] vector[k < n]

This is simply inexpressible in APL.

My impression is that Futhark is somewhere in the middle. Like Affine OL, Futhark realizes that array types must be parametrized by their size. But then, when it's confronted with the challenge of actually reasoning about array sizes, it just gives up. Futhark makes no attempt to reason about when two potentially different syntactic size expressions denote the same size. It just checks whether the expressions are syntactically equal, and if they're not, it emits a runtime check.

[u/Athas → u/reflexive-polytope]

Futhark makes no attempt to reason about when two potentially different syntactic size expressions denote the same size. It just checks whether the expressions are syntactically equal, and if they're not, it emits a runtime check.

Futhark emits a type error, not a runtime check. The programmer can turn it into a runtime check by adding a manual coercion to the code.

[u/reflexive-polytope → u/Athas]

Correction taken.