<p dir="ltr">> 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.</p>
<p dir="ltr">You might want to look up co-recursion and codata, a way to deal with I/O based infinite loops, and still keep some notion of totality and (co-) termination. </p>
<p dir="ltr">See eg <a href="http://blog.sigfpe.com/2007/07/data-and-codata.html?m=1">http://blog.sigfpe.com/2007/07/data-and-codata.html?m=1</a></p>
<br><div class="gmail_quote">On Fri, 19 Dec 2014 08:17 Zooko Wilcox-OHearn <<a href="mailto:zooko@leastauthority.com">zooko@leastauthority.com</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">[Folks: the weekly “Tesla Coils & Corpses” meetings are, by design,<br>
not limited to any particular topic, or to any practical requirements.<br>
We let out imaginations fly free! This week, our imaginations flew<br>
into new programming languages…]<br>
<br>
Tahoe-LAFS Tesla Coils & Corpses, 2014-12-18<br>
==============================<u></u>==============<br>
<br>
in attendance: Daira, Zooko (scribe), Za (briefly), Graydon Hoare<br>
<br>
Unifying types and values.<br>
<br>
A singleton type is, for example, a type representing a single value,<br>
such as 3, instead of representing a domain of values, such as the<br>
type "int32".<br>
<br>
(A "domain" is a generalization of a set. Domain theory works by<br>
having a partial order on the information that you have about a value,<br>
and elements of a domain are limits of a sequence of values that are<br>
each giving you more information.)<br>
<br>
Abstract interpretation is where you compute all possible results from<br>
some given information about the inputs. It is the generalization of<br>
constant computation in current normal programming languages.<br>
<br>
You can obviously do abstract interpretation using types. Let's say<br>
you have a range type of the integers from A‥B. (Let's use the<br>
convention that this is inclusive of A and exclusive of B.) So we can<br>
have A‥B + C‥D = (A+C)‥(B+D).<br>
<br>
Aside: much of Rust's region-memory-management system is copied from<br>
Cyclone. A lot of the improvement is easing the cognitive and<br>
notational burden and making the error messages helpful.<br>
<br>
Dependent types. In most languages the value space and the type space<br>
are completely separate, so you have expressions involving values and<br>
expressions involving types and they are completely separate. You can<br>
have annotations which combine those two spaces by saying that a value<br>
is of a given type, but you can't say that this type depends on this<br>
value.<br>
<br>
One of the reasons why dependent type systems haven't caught on is the<br>
perceived complexity between these two levels, one of which depends on<br>
the other.<br>
<br>
There's this set of type systems called "pure type systems" which try<br>
to simplify this by unifying certain constructs that appear both at<br>
the value level and at the type level. A Π-type is, you can think of<br>
it as a function from values to types, although it is part of the type<br>
language and so strictly speaking not a function.<br>
<br>
The basic idea is that you compute using singleton types. So you're<br>
treating normal computation as a special case of abstract computation.<br>
If you do that then you don't actually need the value level. Or<br>
equivalently you don't need the type level. You just need one.<br>
<br>
Q: Aren't there going to be some things that are going to be<br>
intractable with abstract interpretation?<br>
<br>
Well, you need only to compute approximations.<br>
<br>
Abstract interpretation is in general only ever computing approximations.<br>
<br>
For example, suppose you have an if statement, and you want to compute<br>
an approximation of the possible outputs, taking into account both<br>
cases of the if, so you run the program abstractly through both<br>
branches of the if and then take the union of the results.<br>
<br>
Graydon says C++ has dependent types, but people use it for very little.<br>
<br>
This sort of programming is trying to see into the future and define<br>
invariants that will hold through all time. In Graydon's experience,<br>
people can't see very far.<br>
<br>
Daira's theory, which might turn out to be wrong, is that the<br>
clunkiness is part of the problem. Graydon agrees that better notation<br>
can let the user see further.<br>
<br>
Daira is hopeful that if we reduce the impedance mismatch between the<br>
value and the type language — ideally by making them identical — then<br>
it will be easier to incrementally make the types more precise. For<br>
example, by writing QuickCheck-style checks, and then converting them<br>
into proofs.<br>
<br>
Graydon says that the incrementalism is interesting. The layering,<br>
stratification, and incrementalism in the design of Noether is<br>
interesting to him. Most systems today, says, Graydon, assume that you<br>
want all of the machinery turned on all the time.<br>
<br>
Most proof assistants are not useful for mucking around — you can use<br>
it if you know what theorem you want to prove, but if you don't them<br>
you can't do anything, can't even write "Hello world". ACL2 is an<br>
exception to that pattern.<br>
<br>
Noether uses the effects system to specify which sublanguage a given<br>
function is in. That's actually really important to making it<br>
tractable, both cognitively and in terms of the type system. You can<br>
specify that certain functions are total.<br>
<br>
Graydon was worried that abstract interpretation would end up with not<br>
being able to say very much about the outputs, because the function<br>
could diverge, throw an exception, but those are precisely the kind of<br>
thing that the effects system is excluding.<br>
<br>
Type systems are very advanced, there are very sophisticated tools, as<br>
long as you have really well-behaved domains. But if you include a<br>
little bit of stuff that happens in practice — a little bit of I/O, a<br>
little bit of floating point that might become a NaN— then we've got<br>
nothing.<br>
<br>
Effect systems are about capturing new territory. We've consolidated<br>
*really* good territory in the domain of pure values, but where else<br>
can we go.<br>
<br>
In Noether the sublanguage that is deterministic is incredibly useful.<br>
It is a language that gives a very good tradeoff of expressivity and<br>
safety.<br>
<br>
To a large measure the actual machine model in modern languages is<br>
stateful and deterministic but not aware of I/O.<br>
<br>
So the deterministic sublanguage of Noether is the one that is closest<br>
to the machine model.<br>
<br>
The design in Daira's head currently requires functions that are<br>
evaluated at compile time to be terminating but not necessarily total.<br>
<br>
As far as we can see the vast majority of things that people write are<br>
trivially terminating, or they have an infinite loop based on I/O.<br>
<br>
Graydon wants to know about the notation for Noether. There's so much<br>
machinery in Noether…<br>
<br>
Daira's going to try to write a prototype of Noether in Idris. Idris<br>
is the closest existing language.<br>
<br>
… discussion of LLVM that Zooko failed to write down…<br>
<br>
In defining this new idea of folding the value and type systems<br>
together, Daira has been very careful to preserve the possibility that<br>
you can treat them as separate if you want.<br>
<br>
There was this one very specific purpose for Rust. There's this island<br>
of poor, trapped programmers who are very good, but they have to use<br>
C++. The goal for Rust was just that when their boss comes to them and<br>
says that they have to start a new project, there's an alternative<br>
which is not worse than C++ in any way, but at least it has memory<br>
safety and thread-safety.<br>
<br>
Really good C++ programmers do two things: 1. They lean on the<br>
expressivity of the language, so that the resulting code ends up being<br>
very terse. 2. They spend a lot of time doing careful adjustments,<br>
very patiently, in order to get everything right, running it under a<br>
memory debugger, …<br>
<br>
This is something we [Graydon] discovered with Rust — to our surprise<br>
— if you've ever done a lot of object-oriented programming… for<br>
Graydon personally, object-oriented, he didn't enjoy it. The methods<br>
are small, that's annoying. Polymorphic dispatch is annoying, but the<br>
really unsafe part is the this pointer, which is implicit state that<br>
shows up in every function. Rust's mutability-controls prevent that.<br>
<br>
Daira thinks of the value of ownership types as being in controlling<br>
aliasing (particularly mutable aliasing) rather than memory<br>
management, since memory management is already largely a solved<br>
problem from Daira's point of view.<br>
<br>
<br>
<br>
Regards,<br>
<br>
Zooko Wilcox-O'Hearn<br>
<br>
Founder, CEO, and Customer Support Rep<br>
<a href="https://LeastAuthority.com" target="_blank">https://LeastAuthority.com</a><br>
Freedom matters.<br>
______________________________<u></u>_________________<br>
tahoe-dev mailing list<br>
<a href="mailto:tahoe-dev@tahoe-lafs.org" target="_blank">tahoe-dev@tahoe-lafs.org</a><br>
<a href="https://tahoe-lafs.org/cgi-bin/mailman/listinfo/tahoe-dev" target="_blank">https://tahoe-lafs.org/cgi-<u></u>bin/mailman/listinfo/tahoe-dev</a><br>
</blockquote></div>