benchung / gradualcomparison Goto Github PK

At the moment, we have a translation mechanism defined for expressions alone, not classes or the program as a whole. In fact, we don't have a definition of a program in the first place, We need to define both programs (expression and list of methods?) and a way to typecheck and translate an entire program at a time.

The monotonic definition that we have right now was written for the previous version, and is overcomplicated for what it does. We need to bring it forward to the new version and simplify how it works.

At the moment, our version of transient uses either consistency (~) or subtyping (<:) to conclude that no cast is needed at a particular location. However, this is too strong a relation to capture the Transient semantics, as a result of consistent subtyping.

The reason why is what we really need to do is show that if there is some type t'' such that t <: t'' ~ t', then t and t' can be converted without a cast. This is the basic justification behind Siek's original notion of consistent subtyping, and is something that we should model if we want to capture Transient correctly.

Since we don't have a representation of consistency as-is, this is not a huge issue. Instead of defining consistency, we just need to define consistent subtyping and we're good.

Based on our discussion today, I came up with the following proposal for a source syntax. This language implies:

• Automatic insertion of @ for dynamic invocation
• No user-inserted casts
• No user access to direct field access (auto-generated getters/setters only, handled by mtypes already).
• No user-defined field accessors.

e ::= x | this | e.f() | e.f(e) | e.m(e) | new C(e ...) 
k ::= class C { fd ... md ... }
md ::= m(x:t):T { e }
fd ::= f:t
t ::= * | C

We've had the chance to discuss all but the last point. Feedback? @janvitek @francesco-zappa-nardelli @Palez

Behavioral cast is broken in the implementation because it does not correctly handle the case where we have both typed and untyped methods in the source and target, which was the subject of #5 in the formalism. We should port the outcome of #5 forward from the formalism into the implementation.

At the present time, the figures that contain the translations are not up to date with the results of #7. This is obviously not ideal, so we should port the new translation definitions up.

Right now, rule MTT (soon to be renamed TA-TYMETHOD) is designed to retain one of Transient's semantics: if you call a typed function, its arguments will be checked before entry.

This means that if you have a function that looks like

get2(x:int):int = 2

Then the call get2("hello world") will fail, even though nothing goes wrong, as get2 never refers to x. However, because we do not have sequences in function bodies, we have to encode this in the translation as a new object creation, giving us the relevant generated body, which would be

new A2(<int>x, 2).f2()

This rule means that we have to always make a class A2, and makes the translation rule in question much wider. If we were to get rid of this semantic, we would make class table translation simpler, and shrink the Transient translation rules. However, this is a deviation from the original.

An alternative approach is to change how method generation works. Instead of having a guard object that lets us sequence expressions (which in turn requires that we cast the variable in the body of the method in every use), we can generate a guard method that does the cast, then passes the casted result to the actual implementation. This guarantees that the cast will happen, reduces the total number of casts, and achieves the goal of removing A2, but requires a slightly more complex MTT.

The appendix is a jumbled mess. Unmess it up.

The new version of the translations, unlike the bidirectional cast insertion system, is not itself a type system. As a consequence, it requires a source level type system to allow it to work correctly, and only translate well-typed terms. We only have a source level type system for Thorn, not for any of the others, so we should define some.

Ideally, we would be able to use the same source level typing for all of the systems. However, there is one case where this cannot work, which is Typescript. Typescript has the interesting circumstance that we cannot do field access on anything besides the this reference, and as a result, will have to use a different source level typing.

Behavioural cast was made for when we were making the same 100% or 0% typed assumption about classes as TR does. However, in Kafka core we can't make that assumption, so the behavioural cast implementation isn't really sane. For example, given a well-formed class that has an overloaded method (with both typed and untyped variants), and asked for both typed and untyped wrapped methods, behcast will produce 4 methods (one typed/untyped pair for each of the two methods in the source class).

To solve this, we need to handle this case in both a type-safe and morally correct manner. This means that a wrapper's methods need to satisfy something like the following table (t1 -> t1 => t2 -> t2 means that the function with signature t1 -> t1 forwards to function t2 -> t2):

I think that this table could be simplified into a much simpler set of generation rules, but can't think of them right now.

Now that we have a new and improved source language (#6), we should rewrite the somewhat dated translations. The issue with what we have now is that they were right for various old versions of the Kafka target, but aren't all correct for the modern Kafka. Moreover, they don't properly enforce the well-formedness relation, most notably overloading, so the mostly-common class translation overhead needs to be fixed.

The transient semantics is an important one for us as it exposes some interesting edge cases in our formalism. We need to define a translation to the base language that supports it.

We're currently doing most of the work in a tiny enclosed environment, away from the majority of the text. The final paper needs to be written somewhere, and it would be best to do it in the main file.