Lambda the Ultimate

Many texts on untyped lambda calculus are heavily loaded with math.

I have tried a different approach to look at lambda calculus from a programming point of view. The results are posted in a little paper on this website.

As a special add-on, I show how to systematically construct algebraic datatypes in lambda calculus.

Comments, hints etc. are welcome.

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?