> 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 <zo...@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@tahoe-lafs.org > https://tahoe-lafs.org/cgi-bin/mailman/listinfo/tahoe-dev >
_______________________________________________ tahoe-dev mailing list tahoe-dev@tahoe-lafs.org https://tahoe-lafs.org/cgi-bin/mailman/listinfo/tahoe-dev
