Robbert, I believe Avail breaks new ground in its balance between soundness and expressiveness. I call its type system “first-order safe”, because if semantic restrictions are all correct, then no expression can fail to produce the right type at run time. The language’s implicit rules for propagating values ensure this. However, since it’s possible to write a semantic restriction that is incorrect, we don’t have "second-order type safety” – we can’t check the semantic restrictions for correctness, any more than we could check an arbitrarily complex program in some other language for correctness (other than type-correctness). So Avail balances its first-order soundness with second-order unsound semantic restrictions, tempered by run time checks.
There are languages that claim to do better, say rejecting programs that have no proof of correctness, but the programs that can be written in those languages are still quite restricted… and the correctness is only relative to a spec, which is just another program in a more declarative form. In my experience the spec is wrong often enough that a deep, formal proof of an implementation is almost pointless. Now to be more specific, consider how we ensure first-order safety. The primitives declare in the VM what types they require and produce. If those declarations within the VM are correct (a requirement of any language), then what they produce can be relied on. In fact, L2 doesn’t check the results of primitives. The primitive declarations are even able to be more precise than just specifying a flat type signature. They say that given a particular collection of argument types, the result is constrained to a particular type that’s a function of the input types (provided by a method in that subclass of Primitive). They also declare under what circumstances the primitives are known to succeed, known to fail, or are unknown. L2 makes use of this information as well at each call site for performance. But we wanted the library’s function/method types to be independent of improvements to this detailed but incomplete information provided by the VM. Otherwise when we improved a bound on some primitive we would produce a different type signature in the library. Typically just stronger, but in theory we might have to weaken some result types to fix bugs. So we keep this detailed information out of the Avail programer’s visibility. The “_+_” operation takes two numbers and produces a number. It’s up to a semantic restriction in the library to determine how to assert that a call site that’s adding (say) two natural numbers can only produce a natural number – and can’t fail. In general the addition can fail, say for ∞ + (-∞), which is undefined, but natural numbers don’t contain ±∞, so such an addition won’t fail. We restrict the call site by the intersection of the semantic restrictions (and the primitive’s basic result type, number), but we don’t actually check the result's run-time type if the primitive has guaranteed at least as strong a result for those inputs. The same way we block propagation of nulls out of variables, the VM also prevents propagation of incorrectly typed information past the returns from method invocations. We also check the input types for general operations like function application, but… no surprise… L2 is able to skip the run-time checks if it can statically prove that there will be the right number of arguments of the right types for the provided function. So to get better performance we can simply assert stronger things in the VM, without affecting any of the types in the library. A tighter return type can even reduce the potential polymorphic calls that subsequently operate on the value. Assuming we get those assertions correct, the VM runs faster while still being type-correct. But when we express stronger semantic restrictions we (the VM writers) no longer have the responsibility of coding them correctly, like we require in the VM. That’s because anybody may write a semantic restriction. The code’s static type safety is as correct as those restrictions, no more and no less (assuming a correct VM), but there is always run time type safety (again assuming a correct VM), because anything the VM can’t prove is simply checked at run time, invoking the run time type failure handler if something goes wrong. That’s not something you want to happen very often, of course, but it helps you debug your library by refusing to propagate anything that’s the wrong type. The other reason to separate VM primitive assertions and semantic restrictions is expressivity. In theory what you can write in Java (for primitive strengthening) and what you can write in Avail (semantic restrictions) cover the same territory, but obviously there are huge differences in expressiveness. In fact, when you write such code in Java, the Java type system is so incredibly weak that almost any gibberish will compile. That’s partly due to how we use Java’s types in the VM, but really Java doesn’t provide anything close to strong enough to have benefit for us in the VM. It was originally written in Smalltalk, and we really get very little mileage out of Java’s types. The A_* interfaces are only there to reduce the chance you’ll shoot yourself in the foot, and to make auto-complete suggestions more narrowly focused. If I have an A_Map and I extract a key from it, I have to broaden it from AvailObject to A_Tuple or whatever I already “know” is supposed to be the kind of key in that map. I’ve played with the idea of making A_Map be generic in two parameters, but since Java generics are erased and most values pass through Avail at some time anyhow, the Java types would just be made-up anyhow. Java’s type system provides about as much help with correctness with the Avail VM as assembly language’s type system (i.e., none). Note that since semantic restrictions are written in Avail, their bodies have first-order type safety. So you get the benefit of the type rules and any existing semantic restrictions even when writing new semantic restrictions. This assistance is compounded by the principle of meta-covariance (given two types t1 and t2, (t1 ⊆ t2) = (t1’s type ⊆ t2’s type)), which Avail automatically guarantees for all of its types. So maybe the right way to describe all these things is that Avail separates the concepts of: first-order type safety (guaranteed by the VM), second-order type safety (provided by libraries, but checked at runtime), and performance (by using type deduction within the VM). It makes sense that several years down the road we could start applying guided theorem proving to statically check the correctness of semantic restrictions. I suspect we could eventually prove the majority of them, but simply validating a user-provided proof might be easier (the name Cayenne comes to mind, but I think that project is defunct now). Some semantic restrictions, however, one may want to simply accept as axioms. I think all of this depends on how the market chooses to accept Avail. After all, people are still using PHP and Javascript (for anything ever). One more thing before I go: Say we invoke a method and get back a result that has a semantic restriction that narrows it such that its run-time type has to be checked. Yes, we take a hit checking that value's type, but after the check passes we know that the value really has that narrowed type. We can pass it around with confidence, and the VM will optimize using the assumption that this already-checked value has the type that we expect. When passed to a primitive, this narrowed type is what gets used to deduce what type of value the primitive will produce (and whether it can fail), so the actual number of run-time checks is probably lower than you’d expect. -Mark > On Mar 11, 2015, at 3:43 PM, Robbert van Dalen <[email protected]> wrote: > > Hi, > > The following has been bugging me for a while: > Avail’s type system is not sound in the present of semantic restrictions. > I could be wrong of course :) > > Blurp lifted from: https://developers.google.com/v8/experiments > <https://developers.google.com/v8/experiments> > > "Soundness is a formal correctness property of a type system. It guarantees > that (1) an expression that has a static type T can never evaluate to a value > that is not a T, and that (2) evaluation cannot run into unexpected runtime > type errors”. > > Not so with Avail’s semantic restrictions. > I’m pretty sure when Avail is compared to other strongly-typed languages, > Avail's soundness will be a big discussion topic. > (Especially when we release the "Language Feature Comparison Matrix”). > > So it is claimed that soundness potentially allows for better optimisations, > as certain properties will be statically *proven* to be true. > In contrast, Avail has to resort to VM runtime optimisations: it has to guess > and construct the *real* types at runtime in order to be efficient (like the > Self, Smalltalk, Lua and Javascript VMs). > > But does that really matter? > Sure, non-soundness makes it hard for the Avail's runtime to be as efficient > as - say the JVM. > > The good thing is that with semantic restrictions we gain much more power at > compile time: > Avail can reject programs at a much more sophisticated level than any other > programming language to date. > But Avail also allows you to strengthen types at compile time that don’t hold > up at runtime. > > Of course, nothing prevents us from adding a (very advanced) semantic > restriction checker that is sound and doesn’t get in the way. > But that time is not there yet. > > I guess it is all about trade-offs. > > cheers, > Robbert. > > > >
signature.asc
Description: Message signed with OpenPGP using GPGMail
