Lambda the Ultimate

You can help them if you make error messages really specific and explain *why* the typechecker infers that something is of a particular type, or of each of two conflicting types.

I can do a bit better than that I think by inlining error messages directly into code as part of a live programming experience. They might have to navigate between multiple statements (visible in their scope of course) to debug the type error; inference and a flexible type system definitely makes things harder! I have not designed the visual experience for type error debugging yet, however.

You ought to formalize the 'laws' of this particular graph theory, and explain it with node/edge diagrams and examples.

Definitely! I have one heck of a conference paper to write about this. It doesn't help that much of the existing type theory out there is based on term structure, not graph theory. However, I've done this before for Jiazzi, so I think its doable. It also turns out that any type theory that involves nominative subtyping is also based on some amount of graph theory.

This is reasonable and logical on its face, but it will confuse some because they now get errors not local to the thing they were working on, and the evidence that something is both a 'cat' and a 'dog' in the first place can be hard to follow if it's more than a few steps.

I used to call this explicit "exclusive" inheritance, but realized that exclusion could be established implicitly when two traits implemented the same abstract method. A type error in YinYang then always consists of (a) two incompatible traits extended by the same object and (b) a set of local assignments that cause either trait to be extended. Exposing (a) and (b) to the programmer is key to making the type system usable, but as I stated already, I don't know how this UI looks like yet.

Thanks! I'll check these posts out from work tomorrow (blogspot is unfortunately blocked here) and get back.

That is a quite useful comparison. I don't think YinYang is very close to row polymorphism because it is completely nominative, but I'll try to learn more about the topic to be sure.

I'm not able to relate this system to row polymorphism in any way. Maybe we're thinking differently about what row polymorphism means, or maybe you're having an insight about this that I haven't followed.

Can you explain what you mean here?

Here's the analogy that I saw, with apologies in advance: (1) I'm very good at mixing up (mixing in?) concepts under names that are inappropriate, (2) I think in Lisp syntax so I'm not quite following your YinYang syntactic conventions, and (3) this ended up a lot longer than I'd hoped.

From your YinYang post: "what class an object extends depends on what it does"
The analogous Row Polymorphism style: "the elements required of input types depend on names used"

I have seen the view of row polymorphism that I would characterize as "implementation-oriented", where RP is an indexing trick to expose subsets of a product type. I.e., the type (a * b * c) would carry around the map (a->1, b->2, c->3) so that a use-site requiring (a * c) could look up the appropriate indices in the type it is handed.

I'm here using RP in terms of its type-requirements inference rather than its implementation. That is, seeing a function use (a * c) tells us that it can use any type exposing "a" and "c". To repeat the example from the post:

(def foo (a b)
    (+ a b))
; |+| must be a function of a, b
; for example
(def |+| (a b)
    (_add_ a.as_number b.as_number))
; so now we know that "a" and "b" need an "as_number" named property
; thus, we can infer that "foo" is polymorphic over any types with "as_number" property  

We can apply this kind of reasoning to the ThicknessListener function:

(def ThicknessListener (w)
    (if w.Pressed
        (assign w.Thickness 10)
        nil))
; "w" must have "Pressed" and "Thickness" properties
; deriving type (w::(product Pressed Thickness))  

What I see YinYang as extending this RP-like name-polymorphism inference is the capability to infer construction, and not merely inferring possible uses. Thus, if we use the ThicknessListener as so:

I see YinYang extending this in two ways

1. namespaced product types through the trait extension hierarchy
2. inferred type construction

We can see the first (namespace names) in the trait definitions:

(defTrait Widget () ())
(defTrait Bordered (Widget)
    (Thickness : double))
(defTrait Button (Widget)
    (Pressed : bool)) 

These imply that the named-trait "Pressed" can only be inferred in some type already declared or inferred to be a "Widget".
In RP, I might make a type (say, "Cylinder") with "Thickness:double" and "Pressed:bool" properties, referring to an actual physical object made of pressed metal rather than a graphical widget.

We can see the second (inferred construction) in this hacky use of the above:

(let
    (w (new Widget))
    (assign w.Pressed false)
    (ThicknessListener w) )

The ThicknessListener invocation exports the need for a type that has Pressed and Thickness properties; this can be validated against the declaration of w as a Widget type. Then, this export informs the instantiating environment that it will have to construct a type with the given traits and their initialization/methods mixed in. A (merely) row-polymorphic world would need a full declaration:

 (let
    (w (Thickness Pressed))
    (assign w.Pressed false)
    (ThicknessListener w) )

And doesn't have any native way of delineating identically-named properties.

This is quite useful, thanks!

The fact that YinYang traits are nominal allows us to infer construction, while the structural approach have no hope of doing that (it doesn't even make sense).

But structural typing also has a problem with large libraries and code completion in general. I mean, when all you care about is if some string of bytes is equivalent, what does that mean for a code completion menu?

I guess I think of row polymorphism primarily as a shorthand for composition of application. No type inference required (or allowed!) in the usual case, because typing is something of a Gordian knot under row polymorphism. Every function in the row takes a function as its argument and returns a function as its return value. Further, every function they take (and return) also takes (and returns) functions as its operands (and return values). That has already put us beyond the power of many languages' type systems to express any difference in function types.

But in a language with an absolutely complete type system, we may still have some generics with superposed distinct type signatures, either as functions in the application or as arguments/returns along the application row, or both. In that case an inference process may deduce which type signatures among them can be used.

However, you need the information from the ending type of the row, backpropagated through an arbitrary number of intermediate functions, in order to statically determine what the type-signature of the function something ought to return (and therefore the choices of the type signatures available of the function returning it and the choice of possible function types all of those can take as arguments) needs to be; the type of the argument alone is not sufficient.

The unfortunate things about backpropagating type inference on generic functions under row polymorphism are first that it is hard to guarantee that the inference process gives a unique result, second hard to guarantee that it gives a result at all without actually performing it, and third that it may require exponential compute power relative to the length of the longest application row between any two monomorphic functions.

It simply had never occurred to me to think of type inference on generic functions as part of an implementation of row polymorphism, nor even really to consider generics with multiply-typed definitions to be compatible with row-polymorphism. Now that you have drawn it out I see how the type-inference process required would be related to the type-and-trait inference here.

I'm sure that I've ever seen that type-inference process actually implemented on a row-polymorphic system anywhere, nor worked with any row-polymorphic system that allowed generic functions at all for that matter. I'm somewhat amazed that you were even able to conceive of it.

I guess I was having a blind spot due to my preconceptions about the limited expressiveness of most type systems and the incompatibility of these paradigms. Thanks for explaining.

Bear

?

Where are the constraints though? Back propagating requirements?

Sounds a bit boring, but at least descriptive.

If you're looking for a good acronym, you're pretty close to MOTION or MOAT something.

Modular Object and Type Inference On Naming Association - MOTION-A?

Better as a working title. Here is the working abstract to go with it:

Type inference does not deal well with languages that support nominal subtyping: only local type inference often works reliably without costly global analyses. We present the YinYang language where all program term and object types are inferred with full support for encapsulated mutable fields, nominal subtyping, genericity, easy overriding, downcasting, along with local reasoning about type errors and other forms of semantic feedback. Inference supports these good OO features by forgoing typical unification that computes types, principal or otherwise, and instead by tracking type constraints in term assignment graphs that modularly deals with fields. Required mixin-like trait extensions are then propagated along these graphs towards assignees, providing a basis to form objects and provide semantic feedback; e.g. detect incompatibilities. This paper describes our design, trade-offs made for feasibility, and implementation.

I offer this in the spirit of getting you the best abstract in the end. If you want someone to nitpick in minute detail, here's feedback aiming to improve clarity without much rewording. Basically, this is my reaction on first reading, with each impulse I felt to alter phrasing or punctuation. I'll explain each suggested change. So far I don't have a fix for my impression that modular is undefined where it appears first in "non-modular", but I suppose an earlier extra sentence would work. Feel free to take this any way you find useful. (Yeah, I know this is weird; just consider it my idea of Friday evening amusement.)

Phrase "with having to devise them" seems awkward, and I like a colon better in one spot:

Explicit type declarations enable semantic feedback, but burden programmers with devising them: a high cost when complex types are considered.

Formula rather than X, better Y usually implies some parallel construction, with something that stays the same, like a common subject—possibly implicit. It bothers me the subject of forsake is not repeated in the next phrase, to the extent I re-read multiple times to parse any sense I might have missed. When I look for the referent of "both worlds" I can't find two things. Use of via implies something cooperative, but I think you mean dynamic typing interferes with semantic feedback. If so, here's how I might say it:

Rather than losing semantic feedback under dynamic typing, use of type inference can deliver the best of both worlds—but it's limited by subtyping and intricate relationships in object-based programs.

I also cut definite article the before intricate relationships above because it functions as a back reference. This way proposes the idea now; the original phrasing implies everyone knows that already which gives a reader a chance to start resisting.

Next I make three changes for flow reasons only. The word only often works better in a different spot than one's first impulse. Swapping reliance for relying is probably an attempt to avoid repetition of gerund verb forms. Making analyses singular makes it more generic to me, whereas plural sounds like you have specific ones in mind.

Object-oriented (OO) languages can then be limited to inferring local types only, or reliance on ad-hoc non-modular analysis.

I already noted I don't know what modular means there, so I'd fix it but don't know how.

A hyphen in object-types strikes me as wrong, changing the sense slightly. I think you really mean two words there. When multiple words denote one concept, hyphenation helps a reader parse that correctly. Here I think you mean types of objects, and not more specific jargon.

We present a novel OO language called YinYang where object types are completely inferred.

The next sentence is about a list of four things, but I didn't get that at first. You might re-order those four things, or use semi-colons as list-item separators, or something else to presage list structure. A first complex item in a list is problematic. I assume you wanted semantic feedback to go first. Numbering also works but is heavy-weight. This is just a stab:

Our type system fully supports separate compilation with local reasoning about encapsulation; mutable object fields; subtype and parametric polymorphism; and finally semantic feedback like Intellisense and type errors.

Phrasing infers not just types is slightly awkward, and once again definite article the looks like a back reference when you're introducing class extensions. Note use of as well here only works when removed from the preceding sentence.

YinYang also infers not only types, but class extensions of both object and class definitions as well.

Something awkward happened again with rather, so this is just an attempt at smoothing. (But I still wonder what a modular graph is here.)

For such features we track type requirements rather than type provisions, in a modular graph of assignment relationships.

This arrangement gets it closer to referent type system, hyphenates trade offs which should not be two words, and loses definite article the again because it introduces existence of tradeoffs rather than refers back to them.

This paper describes our type system and its implementation, with trade-offs necessary for feasibility.

If this sort of feedback isn't useful, just ignore it, and warn me off if you hope it never happens again. :-)

Thanks for the feedback. I fixed some of the writing, but its still kind of early; I'll probably re-invent the abstract a few times before I get it right. I eventually want something edgy and confrontational; I prefer to make very strong statements in abstracts.

This is just a first step before I can write the rest of the paper.

This is quite useful, I'll check it out. BTW, bitc-lang.org seems to be down.