Lambda the Ultimate

Edwin Brady has been working on the next version of the dependently-typed, eager, general-purpose Idris. It is now self-hosting.

tl;dr (twitter)

Edwin's press release (from the Idris mailing list):

Hi all,

I decided a couple of days ago, it was finally to time to have a go at
seriously porting Idris 2 to compile itself. To my surprise, it actually
worked (barring a couple of bits and pieces such as some details of the
IDE mode, and a couple of language issues that I'll resolve shortly.)

You can see the results here: https://github.com/edwinb/Idris2-SH

At some point in the next couple of weeks, I'll probably move to this as
the main development version - once I've ironed out the issues, and
worked out what a good process is for building and developing.

[..]

This also enables some other things that I've been holding back on for
the moment: plugin code generators, and better metaprogramming, among
other things.

Much more on this later. For now, I thought it would be nice to let
other people have a go with it.

My favourite new feature is that building the whole thing from scratch,
in the fully self hosted version, now takes about 1m45 on my machine,
which is about as long as the code generation along for the Idris 1
version :).

A shout-out to Chez Scheme, which Edwin uses for bootstrapping.

Perhaps some of you here might be interested in modus_ponens [1]. It is a rust library to develop forward chaining inference engines that are performant and scalable, comparing in that arena very favorably with CLIPS. In addition, the syntax for the facts that an engine developed with modus_ponens understands is provided by the developer as a Parsing Expression Grammar, with little restrictions.

[1] https://gitlab.com/enriquepablo/modus_ponens/-/blob/mirrors/README.md

Owl is a parser generator which targets the class of visibly pushdown languages. It is:

• Efficient - Owl can parse any syntactically valid grammar in linear time.
• Understandable - like regular expressions, its parsing model (and error messages) can be understood without talking about parser states, backtracking, lookahead, or any other implementation details.
• Easy to use - using Owl's interpreter mode, you can design, test, and debug your grammar without writing any code. An Owl grammar compiles to a single C header file which provides a straightforward parse tree API.

The restriction to visibly pushdown languages imposes restrictions on recursion. Rules can only refer to later rules, not earlier ones, and all recursion must be guarded inside guard brackets.

[ begin ... end ]

The symbols just inside the brackets are the begin and end tokens of the guard bracket. Begin and end tokens can't appear anywhere else in the grammar except as other begin and end tokens. This is what guarantees the language is visibly pushdown: all recursion is explicitly delineated by special symbols.

https://github.com/ianh/owl

Note: I am not the Owl author, but I found it to be a useful tool for my own projects. I play around with toy programming languages as a hobby and I am not well-versed on automata theory.

I am posting here because I would be interested to know what your thoughts are about the class of visibly pushdown languages, specifically the constraints it imposes on recursion, how that compares to recursive descent, and any pointers to variations or similar approaches that you know of.

From machine code to assembly and from that to APL, LISP, Algol, Prolog, SQL etc there is a pretty big jump in productivity and almost no one uses machine code or assembly anymore, however it appears there's been almost not progress in languages for 50 years.

Why is that? Are these the best possible languages? What is stopping the creation of languages that are regarded by everyone as a definite improvement over the current ones?

I redesigned the constructors in Theme-D version 2.0.0, see [1]. The design is inspired by the OCaml object system. Constructors are special procedures used to create instances (objects) of classes. They are not defined like other procedures but Theme-D creates them using the construct statement in a class and field initializers in a class. The translator-generated default constructor is sufficient in many cases. For example, consider the class <complex> defined in the standard library:

  (define-class <complex>
    (attributes immutable equal-by-value)
    (inheritance-access hidden)
    (fields
     (re <real> public hidden)
     (im <real> public hidden))
    (zero (make <complex> 0.0 0.0)))

The translator-generated default constructor takes two real arguments and sets the first to the field re and the second to the field im.

The programs objects1.thp and objects2 in subdirectory theme-d-code/examples of the source code [1] demonstrate user-defined constructors. Here is the first example:

  (define-class <widget>
    (fields
     (str-id <string> public module)))

  (define-class <window>
    (superclass <widget>)
    (construct ((str-id1 <string>) (i-x11 <integer>) (i-y11 <integer>)
		(i-x21 <integer>) (i-y21 <integer>))
	       (str-id1))
    (fields
     (i-x1 <integer> public module i-x11)
     (i-y1 <integer> public module i-y11)
     (i-x2 <integer> public module i-x21)
     (i-y2 <integer> public module i-y21)
     (i-width <integer> public module (+ (- i-x21 i-x11) 1))
     (i-height <integer> public module (+ (- i-y21 i-y11) 1))))

The constructor of class <window> passes the first argument str-id1 to the constructor of its superclass <widget>. The constructors also initialize the fields using their arguments. Note that the field initializers may contain more complex expressions than just copying an argument variable.

Here is the second example:

  (define-class <widget>
    (construct ((str-id1 <string>)) () (nonpure))
    (fields
     (str-id <string> public module
	     (begin
	       (console-display "new widget: ")
	       (console-display-line str-id1)
	       str-id1))))

  (define-class <window>
    (superclass <widget>)
    (construct ((str-id1 <string>) (i-x11 <integer>) (i-y11 <integer>)
		(i-x21 <integer>) (i-y21 <integer>))
	       (str-id1) (nonpure))
    (fields
     (i-x1 <integer> public module i-x11)
     (i-y1 <integer> public module i-y11)
     (i-x2 <integer> public module i-x21)
     (i-y2 <integer> public module i-y21)
     (i-width <integer> public module (+ (- i-x21 i-x11) 1))
     (i-height <integer> public module (+ (- i-y21 i-y11) 1))))

Here we log the calls to the constructor of <widget> to the console. Note that we have to declare the constructors as nonpure if they have side effects.

[1] Theme-D Homepage

Toward a deterministic treatment of concurrency for the general case.

A small study in the vagaries of Rgular types in C++.

Abseil blog post.

How can we get better statically typed assurances around the nuances of such concepts? Which languages help the most? Things like Rust or ATS come to mind.

Lex Fridman just interviewed Bjarne Stroustrup on youtube. It's long; a bit over an hour and a half.

But they're talking extensively about C++ and its origins and evolutions and guiding principles.

Here's a handy link to the interview.

I'm in the middle of writing an Object-Pascal-to-Java translator. One interesting aspect is the mapping between source and target types. Is anybody aware of literature about this topic, books, papers, etc.?

I would be interested in things like rules for "widening" a target type over the source type; constraints that must hold on operations applied in the target language so that the result complies with the result in the source language; maybe a formalism where you could even show (prove) that, given some sets of types and operations; etc.

I do not aim to set things up this way, but would enjoy reading some theoretical material about what I'm doing. Is there serious research in the area of source translation, anyway?

Histogram: You have to know the past to understand the present by Tomas Petricek, University of Kent

Programs are created through a variety of interactions. A programmer might write some code, run it interactively to check whether it works, use copy and paste, apply a refactoring or choose an item from an auto-complete list. Programming research often forgets about these and represents programs as the resulting text. Consequently, thinking about such interactions is often out of scope. This essay shifts focus from programs to a more interesting question of programming.

We represent programs as lists of interactions such as triggering an auto-complete and choosing an option, declaring a value, introducing a variable or evaluating a piece of code. We explore a number of consequences of this way of thinking about programs. First, if we create functions by writing concrete code using a sample input and applying a refactoring, we do not lose the sample input and can use it later for debugging. Second, if we treat executing code interactively as an interaction and store the results, we can later use this information to give more precise suggestions in auto-complete. Third, by moving away from a textual representation, we can display the same program as text, but also in a view inspired by spreadsheets. Fourth, we can let programmers create programs by directly interacting with live previews as those interactions can be recorded and as a part of program history.

We discuss the key ideas through examples in a simple programming environment for data exploration. Our focus in this essay is more on principles than on providing fine tuned user experience. We keep our environment more explicit, especially when this reveals what is happening behind the scenes. We aim to show that seeing programs as lists of interactions is a powerful change of perspective that can help us build better programming systems with novel features that make programming easier and more accessible. The data exploration environment in this interactive essay may not yet be that, but it gives a glimpse of the future.