Tesla Coils & Corpses report: programming language design

Thu Dec 18 23:19:21 UTC 2014

> 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.

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.

See eg http://blog.sigfpe.com/2007/07/data-and-codata.html?m=1

On Fri, 19 Dec 2014 08:17 Zooko Wilcox-OHearn <zooko at leastauthority.com>
wrote:

> [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.
> _______________________________________________
> tahoe-dev mailing list
> tahoe-dev at tahoe-lafs.org
> https://tahoe-lafs.org/cgi-bin/mailman/listinfo/tahoe-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://tahoe-lafs.org/pipermail/tahoe-dev/attachments/20141218/8f55e4c8/attachment-0001.html>