A new runtime for Lever 0.10.0

I set up the environment for myself to rewrite Lever's runtime. It is a task that is going to take at least 2 months to finish.

In the current version there are 14000 lines of Python and 30000 lines of Lever code.

Since one of the objectives in rewriting is to improve the readability of the code, you may like to read the code in the repository. The 'next' branch in Lever repository.

The rewrite is appropriate because the changes that are needed will change everything anyway. I cleaned out myself a 'next' branch so that the existing runtime stays in working order while I work on the new branch.

Type system changes

Finally discovered how the subtyping type inference can be made to work. I turned the suoml project into a working prototype.

Key to this was understanding that if you have multiple potential combinations of inputs, then you have to go through all of them. Also there is no sense in doing it as a post-processing step. It should be done at the same time when the type constraint are eliminated. There are many other rules that derived from this observation, they need their own blog post at some time.

There is one remaining very hard problem that is the simplification of the resulting type annotations. Some of the ways MLsub does it still apply, but we still end up with an operator graph that doesn't seem like a good fit for simplifying through subset construction.

Computer algebra modules

The main motivation for this change sprung from the necessity to run linear algebra on more things than floats.

The new design replaces multimethods by operations that resolve themselves through coercion. You can only create coercions between types that you create, and it is checked that the produced coercions are unique.

All of this is compatible with the type inferencing, so it remains available if code must run through an optimizing compiler.

I did try to produce good algebraic structures in my previous language. Once I figured out many enough things and studied enough abstract algebra, I could have implemented them in the existing language. Doing it right from the beginning is probably a better solution.

Documentation format

The Texopic syntax that I experimented on has to go away. It doesn't look bad at first but has too many surprises and is difficult to implement. I'm planning to move into XML that I didn't even consider at first.

Turns out that the text mode was not going to be the mode where I write documentation in. Good documentation also needs extensive use of graphics and other means of communication. You need a graphical editor for producing good documentation with most comfort that you can get.

Additionally I explored literate programming and realised that it might be what I want to do in the future. I think it is near to my original plan of writing documentation, upwards from the source code.

So how do you keep the source code as readable text while you have a fancy XML-based graphical documentation format?

I guess this would work, here's file listing:

example.lc
example.lc.doc

The example.lc contents:

import display

# @main This comment would be grabbed from here and end
# up into the documentation from here. The snippet would
# continue up to the next point.
main = ():
    dpy = display.open()
    print(dpy)

The example.lc.doc:

<doc src="example.lc"/>

<h1>The example documentation</h1>
The plain text written would cut itself into
paragraphs by itself when detecting empty lines in the
input text. Everything requiring to be vertical would
cut the paragraph automatically.

You could drop the full snippet like this:

<full-snippet name="main"/>

The snippet would be also available as plain paragraphs
and separable with the 'snippet' 'comment' -tags.
Likewise the documentation format could grasp to the
module contents and reference those.

Several things here make it meaningfully different from the usual XML documents you read. It is the recognition that the XML tags themselves are extremely heavy for the reader. Also, tracking indentation in a file that can be several hundred pages long is so tedious that you shouldn't at least have the outermost mandatory html and body there.

Documentation effort

I think I have reached the point where documentation can be pleasing to write. But the problem is that it has become too pleasing and I write about all the right things, but don't provide all the context or structure for people to understand my text.

Additionally I have noticed that people simply do not read everything. If I write too much, they start skimming and scanning the texts I write. I notice I do that myself as well, when reading my own texts.

It helps to keep the paragraphs short, but really what helps best is to write to the point and remove or move away everything that goes sideways from what you're trying to tell.

Also I've noticed tendencies to write "marketing hype", the kind of text that tries to impress people but does not really say anything that I would really want to communicate, or tells everything that any other general run-off-the-mill text would write. If anyone else could write it then perhaps I should not write it?

To get better at writing, I propose the most help you can get by getting better at reading. Dan Kurland's critical reading may be a good starting point for your research. Once you've become a good reader, you may then become good writer by reading your own texts as if they were written by someone else.

The lesson about scalability

Overall I do this rewrite for making Lever more scalable without making it considerably less dynamic. The first two changes will make the code further much more compact than what it was and more effective your line of code is, less there is something left to maintain that would limit you from scaling it up.

You are not always sure what people mean when they say 'scalable'. They might mean to scale up in features or scale up into handling larger inputs at once.

Overzealous static typing hinders feature scalability because it introduces the danger of introducing excessive or unsound invariances, for example, when representing gender with a boolean when you are tracking snails because you were previously tracking mice. Type checker zealotry finds it important to validate that a value of a variable stays within a given set of elements, even if you didn't do anything with that information afterwards.

Static typing may improve mass scalability, but the amount of work and effort you do depends on where you have to start, and how much you have to bend the rest of the software to follow those changes. If everything is statically typed then that effort is humongous.

Static typing may improve feature scalability too if the type annotations are correct and on to the point. Correctly documenting the boundaries where some abstractly defined operation succeeds. There's also value if you can verify that interfaces do not inadvertendly change without a version/standard update.

Ironically people who blast loudest about the merits of static typing are themselves likely to get it wrong in the worst possible ways.

Were in one kind of scalability or another, I think the main barrier to scaling up software comes from the documentation effort, or failure of that documentation effort.

If you have the documentation just right, and it shows that you understand your system extremely well, there won't be limits for being able to scale.