Tesla Coils & Corpses report: programming language design

[Zooko Wilcox-OHearn]

[Folks: the weekly “Tesla Coils & Corpses” meetings are, by design,
not limited to any particular topic, or to any practical requirements.
We let out imaginations fly free! This week, our imaginations flew
into new programming languages…]

Tahoe-LAFS Tesla Coils & Corpses, 2014-12-18
============================================

in attendance: Daira, Zooko (scribe), Za (briefly), Graydon Hoare

Unifying types and values.

A singleton type is, for example, a type representing a single value,
such as 3, instead of representing a domain of values, such as the
type "int32".

(A "domain" is a generalization of a set. Domain theory works by
having a partial order on the information that you have about a value,
and elements of a domain are limits of a sequence of values that are
each giving you more information.)

Abstract interpretation is where you compute all possible results from
some given information about the inputs. It is the generalization of
constant computation in current normal programming languages.

You can obviously do abstract interpretation using types. Let's say
you have a range type of the integers from A‥B. (Let's use the
convention that this is inclusive of A and exclusive of B.) So we can
have A‥B + C‥D = (A+C)‥(B+D).

Aside: much of Rust's region-memory-management system is copied from
Cyclone. A lot of the improvement is easing the cognitive and
notational burden and making the error messages helpful.

Dependent types. In most languages the value space and the type space
are completely separate, so you have expressions involving values and
expressions involving types and they are completely separate. You can
have annotations which combine those two spaces by saying that a value
is of a given type, but you can't say that this type depends on this
value.

One of the reasons why dependent type systems haven't caught on is the
perceived complexity between these two levels, one of which depends on
the other.

There's this set of type systems called "pure type systems" which try
to simplify this by unifying certain constructs that appear both at
the value level and at the type level. A Π-type is, you can think of
it as a function from values to types, although it is part of the type
language and so strictly speaking not a function.

The basic idea is that you compute using singleton types. So you're
treating normal computation as a special case of abstract computation.
If you do that then you don't actually need the value level. Or
equivalently you don't need the type level. You just need one.

Q: Aren't there going to be some things that are going to be
intractable with abstract interpretation?

Well, you need only to compute approximations.

Abstract interpretation is in general only ever computing approximations.

For example, suppose you have an if statement, and you want to compute
an approximation of the possible outputs, taking into account both
cases of the if, so you run the program abstractly through both
branches of the if and then take the union of the results.

Graydon says C++ has dependent types, but people use it for very little.

This sort of programming is trying to see into the future and define
invariants that will hold through all time. In Graydon's experience,
people can't see very far.

Daira's theory, which might turn out to be wrong, is that the
clunkiness is part of the problem. Graydon agrees that better notation
can let the user see further.

Daira is hopeful that if we reduce the impedance mismatch between the
value and the type language — ideally by making them identical — then
it will be easier to incrementally make the types more precise. For
example, by writing QuickCheck-style checks, and then converting them
into proofs.

Graydon says that the incrementalism is interesting. The layering,
stratification, and incrementalism in the design of Noether is
interesting to him. Most systems today, says, Graydon, assume that you
want all of the machinery turned on all the time.

Most proof assistants are not useful for mucking around — you can use
it if you know what theorem you want to prove, but if you don't them
you can't do anything, can't even write "Hello world". ACL2 is an
exception to that pattern.

Noether uses the effects system to specify which sublanguage a given
function is in. That's actually really important to making it
tractable, both cognitively and in terms of the type system. You can
specify that certain functions are total.

Graydon was worried that abstract interpretation would end up with not
being able to say very much about the outputs, because the function
could diverge, throw an exception, but those are precisely the kind of
thing that the effects system is excluding.

Type systems are very advanced, there are very sophisticated tools, as
long as you have really well-behaved domains. But if you include a
little bit of stuff that happens in practice — a little bit of I/O, a
little bit of floating point that might become a NaN— then we've got
nothing.

Effect systems are about capturing new territory. We've consolidated
*really* good territory in the domain of pure values, but where else
can we go.

In Noether the sublanguage that is deterministic is incredibly useful.
It is a language that gives a very good tradeoff of expressivity and
safety.

To a large measure the actual machine model in modern languages is
stateful and deterministic but not aware of I/O.

So the deterministic sublanguage of Noether is the one that is closest
to the machine model.

The design in Daira's head currently requires functions that are
evaluated at compile time to be terminating but not necessarily total.

As far as we can see the vast majority of things that people write are
trivially terminating, or they have an infinite loop based on I/O.

Graydon wants to know about the notation for Noether. There's so much
machinery in Noether…

Daira's going to try to write a prototype of Noether in Idris. Idris
is the closest existing language.

… discussion of LLVM that Zooko failed to write down…

In defining this new idea of folding the value and type systems
together, Daira has been very careful to preserve the possibility that
you can treat them as separate if you want.

There was this one very specific purpose for Rust. There's this island
of poor, trapped programmers who are very good, but they have to use
C++. The goal for Rust was just that when their boss comes to them and
says that they have to start a new project, there's an alternative
which is not worse than C++ in any way, but at least it has memory
safety and thread-safety.

Really good C++ programmers do two things: 1. They lean on the
expressivity of the language, so that the resulting code ends up being
very terse. 2. They spend a lot of time doing careful adjustments,
very patiently, in order to get everything right, running it under a
memory debugger, …

This is something we [Graydon] discovered with Rust — to our surprise
— if you've ever done a lot of object-oriented programming… for
Graydon personally, object-oriented, he didn't enjoy it. The methods
are small, that's annoying. Polymorphic dispatch is annoying, but the
really unsafe part is the this pointer, which is implicit state that
shows up in every function. Rust's mutability-controls prevent that.

Daira thinks of the value of ownership types as being in controlling
aliasing (particularly mutable aliasing) rather than memory
management, since memory management is already largely a solved
problem from Daira's point of view.



Regards,

Zooko Wilcox-O'Hearn

Founder, CEO, and Customer Support Rep
https://LeastAuthority.com
Freedom matters.