Lambda the Ultimate

Maybe two differences. First, we are inferring where to add traits to make the program well typed vs. checking type compatibility. Second, there are no real type variables...trait flow is inferred/propagated as a graph, so differently expressive.

I don't follow. Haskell type classes are about inferring instances (multi-parameter traits) to make the program well typed. It looks like you have type variables to me, though maybe you're thinking about it differently. Looking at your last example, where e and g are inferred ducks, isn't that done by first inferring the type of dict to be array of Duck?

What I'm doing in my language (at least the relevant part) seems even more similar to what you're doing. For example, I also have flat namespaces (and use tags rather than hierarchies to disambiguate), and am developing a very implicit style of programming. My philosophy is that the maxim "explicit is better than implicit" is too simplistic. At the IDE level, we want everything to be as implicit as possible, filling in the holes whenever possible. At the same time, we want any assumption required for correctness to be recorded explicit in the code, so that changes elsewhere cannot silently break it. To achieve both, you need an IDE (not just a text editor). But I'm pointing out one difference I see right away, which is that I'm inferring theories (multi-parameter type classes) rather than traits.

Anyway, I'm at the end of a big project at work, and this discussion is already causing major cache thrashing in my head, so I'll revisit later after the project is out the door. I didn't mean to imply that this sounds like merely type classes. Rather just that I think it is related to type classes and considering the relation might be fruitful for you.

Honestly, I don't understand type classes very well, they look like signatures to me but perhaps I'm missing something big, do they have code additive capabilities that go beyond checking?

In my dictionary example, there is a relationship between set ([] :=) and get ([]) in the graph: the result of get is connected to the subject of set so inference flows that way. There is no explicit type parameter to bind or constrain, although you can take certain nexuses in the graph and think of them as type parameters. Actually, we can define an abstract dictionary implementation by using dummy vars to form the graph...where these dummy vars look very much like type parameters! Code:

class Dictionary {
  private var e, k;
  this[a]:=(b) {
    k := a;
    e := b;
  }
  this[a] {
    if (k.equals(a)) return e;
    else throw new KeyNotFoundException();
  }
}

The resulting graph can then be adhered to by a real dictionary implementation.

I've discussed the flat namespace before as part of a vision to make code sharing easier/more common. I also believe in "going more implicit" as a way of reducing programmer burden. Its not appropriate for all use cases; consider the good and bad of garbage collection. But there is space for languages that do more scary things under the covers (Ruby, to some extent Python).

The type classes mechanism in Haskell is not just about checking -- it's also about using types to infer pieces of programs. If you tried to erase types in Haskell to produce terms in an untyped language, you'd need to encode that extra instance selecting aspect of type classes first.

I don't understand all of the details of your graph algorithm, but I agree it looks similar to type checking. I will go further and predict that when you've worked all the kinks out of it and added the features that you find needed, it will be isomorphic to a type system! For example, aren't you going to want to annotate a function as "List(T) -> T" and be able to conclude that if the input is a list of Ducks, then the output is a Duck? It looks like you'll need that for modularity reasons.

I remember that thread of yours on flat namespaces. It wasn't directly what I was thinking about when I decided to go that route (I was considering other issues), but I'm sure it was in the back of my mind.

I don't agree that garbage collection is a counter example to my thesis, which I'll rephrase:

- Implicit is good: Tooling should strive to provide the easiest way to write the desired code.

- Explicit is good: Code should capture the logical intent of the programmer and should transform in a way that preserves that intent

The issue with garbage collection is that sometimes memory management is part of what the programmer intends to specify and sometimes it's accidental complexity. In the former case, explicitly capturing memory layout requirements is good and in the latter case bad.

For example, aren't you going to want to annotate a function as "List(T) -> T" and be able to conclude that if the input is a list of Ducks, then the output is a Duck? It looks like you'll need that for modularity reasons.

Actually you don't. In this case, there is no constraint that list must contain only ducks unless we write some code that assumes that all of list's members are ducks (e.g., iterate and call quack), in which case everything you put in the list becomes a duck or fails with a type error. The type checking still has modularity since the graph is modular, but there are definitely issues with usability...I can't pre decide what the list will contain and mistakes won't be caught as easily; e.g., if I accidentally put the wrong thing in the list. Just another example of the tension between implicit and explicit.

If I just go down this route, I don't see the need for type parameters at all, in fact, the type system can be based solely on traits. This has a usability benefit compared to a language like scala that supports many different kinds of types. By extending traits by need, we can avoid scala's LUB issues that result from combining hindley Milner with oo.

I think my example was the wrong direction. The interesting case for you is probably where you have foo: List(T) -> T implemented in another module, and then you create a list, lst, of Panels and access foo(lst).position. Can you infer that these are Canvases in this situation?

When you talk about the graph being modular, what do you mean? How do you know the graph behind foo until you've seen its implementation? I'll agree that if you wait until you have the whole program before you do any inference, then you'll have a solution for this, but I wouldn't call it modular.

Yes, but foo's signature is more like list -> list.e, the position access the vibrates through list.e.

Modular means that a signature graph only relates non private members, yes you still need the implementation to generate the signature. But you can compose your signature graphs without peaking inside implementations. Of course, modularity is a gray term, the real question we need to ask is what can/cannot be encapsulated by a signature. Worst case is signature = implementation and we are doing some kind of unscalable whole program call graph/pointer analysis. I'm hoping to do much better than that, but I haven't done the design on that part yet (obviously non-fun declarative doesn't have those problems).

Do you have in mind a way to explicitly encode signature graphs?

Each method call adds a bunch of relationships into the graph, we only need to concern ourselves in the signature with relationships between an encapsulated unit's abstractions. The nodes that still need to be in the graph after we get rid of the private stuff somewhat resemble type variables if we label them. Say dictionary.set(a,b) has the signature k := a, e := b, that means a flows into the k node while b flows into the e node; dictionary.get(a) then has the signature k.equals.arg1 := a and return := e, meaning a will be used in a key equality test and e flows into the return value. e and k
are just junction nodes between set and get; they aren't actually labelled. The signature then also contains method calls (k.equals.arg1 := a) that could occur, so they are somewhat higher order and potentially scary. These higher order nodes lead to further structure once we know what potential implementations of equals do.

The signature language itself just resembles a bunch of assignments between values, junction nodes, and traits with no control flow or order.

This sounds like it is very close to what I'm doing, which is to solve a bunch of equality constraints between types (Haskell allows more general constraints, which I find harmful). I'm still sketchy on the details, though. Why do you refer to constraints such as "a = b" flows from b to a? Those constraints are undirected, aren't they?

e and k are just junction nodes between set and get; they aren't actually labelled.

How do you reference a junction node, then, in the signature language?

Also, I'm not sure what you mean by "higher order nodes". Is that a special condition for you? For me, the theory of dictionary would have free type parameters for Dictionary and Key, and then you could have further constraints on the type Key, but those aren't really higher order. I do still wonder whether separating theories from types (which seem munged together into traits) might be fruitful for you. Edit: Fixed bungled description

It's not equivalence at all, e := a means "e" could be "a," but not always or even sometimes. A trait required for "e" will be required for "a," but a trait required for "a" will not be required for "e."   The reasoning behind this is that "a" must conform to e's interface, but not vice versa. 

Signatures are always generated from and used by implementation, the programmer never writes or references them directly. Labels might be useful if we want to use the signatures as documentation, however. 

A higher-order node is simply a node that refers to an unresolved function. When that function becomes known during composition, it must be applied to the existing graph. 

I'm very interested in how far a trait-only type system could go; it would be a very big thing if we could get the functionality of generics and maybe even virtual types without the complexity of type variables. 

Yes, that should have been clear from what you've written, sorry. So there are big difference between our systems. You want to, e.g., implicitly infer polymorphism when Panels are placed in the same list.

Do you have a plan for supporting first class polymorphic functions? Something like this:

foo(f: List(T) -> List(T))
{
    f(listOfCanvases).head.position
    f(listOfDocks).head.dock
}

Wouldn't the above generate a single node for f, and then fail upon trying to unify Canvas and Dock? Do you have an encoding that would allow this kind of polymorphism?

There are two nodes for each call to f. There is one sig graph for f that will get copied twice into the internal graph for foo; the sig graph can share nodes with the object (not duplicated on call) and have their own (duplicated on copy). Since we don't know f yet, these nodes make it into the signature of foo that then get translated on foo calls where bindings for f are known (i.e., implementations flow into f).

Sorry my comments haven't been so clear, I'm still trying to think this through while typing on a virtual keyboard keeps explanations too short!

I'm trying to figure out how your system relates to mine. I'm not really sure that your use of subtyping is that big of a difference in the algorithm and might be more a difference of how we're using the systems. This explanation you gave for how parameters get multiple nodes would seem correspond to something like inferring an intersection type for f in my system, which I don't do but possibly could. I'm a little surprised that this is all efficiently computable for you and not undecidable or NP. Maybe it's because you wait until the entire program is available. Are you reasonably sure that it is?

Hopefully I'll get a chance to think deeply about this over the weekend.

I've thought about this a little bit, and while there are certainly similarities, I think there are sizable differences between our approaches. You're doing more of an OOP subtyping style, whereas I'm doing theories and type parameters. Also, you're using "big bag of constraints" as semantics, hiding those constraints from the programmer, whereas I try to simplify constraints down to an understandable form and present them to the programmer.

One place where I think you might run into problems with the "build a graph of everything" is when you have a universally quantified function instantiated at infinitely many types. For example:

foo :: (a -> Maybe a) -> b -> Bool
foo f b = case f b of 
            Nothing -> True
            Just c -> foo f [c]

It's contrived, but I think code that does something similar happens in practice when dealing with recursive data types. What would your system do with code like this?

Each instantiation is unique except....when recursion is detected. In that case, we can create a cycle in the loop to bind the arguments of the existing instance with the recursive instance. This is quite inaccurate but mirrors a looping alternative to recursion, and is general; doesn't depend on tail cursion, just draw more edges from the reused call's output, and no need for a fix point.

I figured you were doing something like that, actually. So you might end up with errors from bringing in too many constraints in cases that would be relatively easy to type with a quantified type. I guess you'll find out if this is a problem in practice as you play with the system.

Sure. This approach easily fails if you have some sort of hetero ABAB structure that is traversed with the same function, where we get a merge for the function target of A and B whether that is meaningful or not. But does that occur in practice? Keep in mind that this language is not meant to heavily rely on recursion...maybe as much as Java does.

Your project sounds interesting. Good luck!

Actually, the only case I can think of is where a function with a quantified type calls itself recursively with a different type argument. This is no surprise since type inference for polymorphic recursion is undecidable.

Or is there another case that you have in mind?

If you have control of the type parameters (not using inference), then you could easy have the implementation F[A,B] call F[B,A], which I couldn't handle in my proposal. I'm not sure if that is useful, but its definitely possible to write that in current languages. I don't know yet what the expressiveness impact of taking that away is.

Isn't that an instance of polymorphic recursion? If we define the following function in ML:

let rec foo a b : unit = foo b a

We get the inferred type:

foo : 'a -> 'a -> unit

foo 3 "4" // type error

In other words, the type inference algorithm unified the type of a with the type of b due to the recursive call. If we do an explicitly type annotated one in C#, this passes type checking just fine:

static void Foo<A, B>(A a, B b) { Foo(b, a); }

Foo(3, "4"); // no type error

For further illustration, if we do this:

let rec foo x : unit = foo 3

Then the type inference concludes that x should have type int, even though foo works perfectly well for any type. And indeed, C# allows this:

static void Foo<A>(A a) { Foo(4); }

Incidentally I used a similar type inference algorithm that you're using to do type/shape analysis for a dynamically typed language. This is to compile it more efficiently, so rather than ML-style type inference that produces the most general type for a function, I want the most specific type (because that gives the compiler more information to optimize it). It does lead to exponential running times though, in this case:

f x = g 3 + g "a"
g x = h 3 + h "a"
h x = i 3 + i "a"
i x = j 3 + j "a"
...

Therefore it greatly helps to memoize/cache results. If we've analyzed h 3 once, we can remember the result and not do it again if we encounter it again via a different call chain. In more complicated cases you'll still have exponential running time however. I imagine that in your case for interactive type inference this helps even more, because when the programmer changes the program you only have to re-analyze the things that actually changed, and look up the rest in the cache.

It would be an instance of polymorphic recursion if it was allowed. My current system just merges nodes when recursion is detected, so you could never expression void Foo(A a, B b) { F(b,a); } or even recursive object compositions that weren't type uniform. I thought about memoization and even fixpoints, but there is no really straightforward way to guarantee reasonable convergence. In most other languages, you would just give up and require explicit type annotations, but that won't work here since the type variables don't explicitly exist.

How do you detect recursion? You'd want to detect recursion in the following case:

F(f,n) = if n=0 then 1 else n*f(f,n-1)
factorial(n) = F(F,n)

Even though syntactically no recursion is apparent. However, you would not want to detect recursion in the following case:

f(n) = n+1
g(ns) = ns.map(f)
h(nss) = nss.map(g)

Even though the map call in h calls g, which calls map again. If you detected recursion in this case you might wrongly conclude that the value nss flows into the inner map.

How do you do this?

What I do is the following: if there is a call chain from f(x) leading to f(y) then recursion is detected if all of the nodes in the graph representing the abstract value x are present in the graph of y. This makes the analysis terminate because on each call the set of nodes shared with the first call to f is reduced by at least 1. The intuition is that if we would allow y to contain all the nodes in x, then it could happen that some computation extracted exactly those nodes and built a graph out of them with the same shape as x, and then called f(same_as_x), leading to analysis non-termination. In case of the f,g,h example: the call to f calls map on nss, which is a list of lists of ints (which is actually represented as an object graph with cycles -- there is no predetermined notion of "list"). Then this nss.map(g) calls g internally, which calls ns.map(f). Even though we now have a map call that results in another map call, we don't detect recursion because ns is strictly smaller than nss (it is missing the outer list structure nodes).

However, in the following case:

rev(nil,ys) = ys
rev(cons(x,rest),ys) = rev(rest,cons(x,ys))

reverse(xs) = rev(xs,nil)

If xs in reverse(xs) is an arbitrary length list then the call to rev is considered to recurse because its arguments contain all the nodes present in the arguments to the previous call. However if we call reverse(xs) on a finite length list xs then the recursive call to rev is missing the first cons cell of xs, hence the set of nodes it has access to is strictly smaller than the previous call so we continue unrolling the recursion and we're able to give a precise type to reverse([an_int, a_string, a_bool]), namely [a_bool, a_string, an_int].

Here is how I think about it, if we have:

F(f) = ... f(...) ...

The modular graph for F has an open slot for f. When we call:

F(F)

it turns out to be something like:

F.f := F

Then rather creating a new instance of F (F'.f := F''), the way we deal with recursion is simply to create a cycle in the graph, so it becomes (F'.f := F'); i.e., their is no new F, we just draw an edge up to the calling F.

I haven't responded because I think that there may be other problems but I would really need to see or work out the algorithm details to be more confident. Here's one question: suppose you want to put a bunch of functions with a common polymorphic signature in a list and use them via that signature. Can you do that? Seems like the nodes would get tangled up and things would break, but I'm not sure I'm thinking about it right. Sean, are you willing to post pseudo-code for the core algorithm?

You don't use functions or any other abstraction by signature, instead you access them directly by their symbol. It makes the language and type system much more weird, for sure, but has different advantages.

I'm writing something up now on the a more primitive language (non-imperative, no abstract functions) and I'm only just beginning to get a handle on a more complete language

I was trying to address Jules' question of whether there are other functions (besides those using polymorphic recursion) that are type-able in a more traditional polymorphic type system, but that would not work as intended in your system.

Position is a direct reference to an abstraction, the language doesn't depend on types to resolve names. The namespace is wiki-like, flat, everything has a unique name even if they share common short names.

So there cannot be any other trait with `Position`?

Is there a possibility inference might be stymied a bit when developers start doing things like:

trait HasPosition { var Position : Point,  ... }
trait CanvasWidget (c:Canvas) : Widget(c), HasPosition { ... }

It seems to me unlikely that you will be able to uniquely infer abstractions from usage (and that the notion of `abstraction` would be somewhat dubious if you could).

I've already run into this very problem in my current implementation. It's necessary to suppress the has position trait (and whatever depends on it) until it is implemented explicitly. This is to prevent the user from accidentally adding position to an object that couldn't support it.

Could you explain what you mean by suppressing the HasPosition trait and its dependents? And by `until implemented explicitly`?

Actually my current implementation is a bit hacky, and I probably have to think about this more. Basically, consider "Position" in HasPosition un-selectable by the user because HasPosition is somehow abstract. When CanvasWidget implements HasPosition, Position suddenly becomes selectable for CanvasWidget, essentially Position has a new full name in CanvasWidget that the user can see/write down. If there are multiple positions from multiple HasPosition implementations, then we are still ok because they all have different full names.

This sort of begs the question of when the programmer will use HasPosition directly. Basically, if they want to add and implement a position, they have to select HasPosition directly, inference isn't useful. In general, inference is geared toward abstraction consumption rather than production.

By what characteristic do you infer HasPosition is "somehow abstract"? Is this based on context - i.e. that another trait inherits HasPosition? Or is there some characteristic of HasPosition itself that clearly distinguishes it as somehow abstract? Why is your CanvasWidget not somehow abstract?

If based on context, I am curious what usability issues might arise from concrete classes retroactively becoming `somehow abstract` as users add specialized modules to the system.

I hope my confusion is proving useful to you...

CanvasWidget doesn't need to be abstract, it implements everything expected of it. HasPosition is definitely abstract, but there is another valid use for the term "abstract" where the abstraction can be inferred and the user is expected to fill in the missing functionality (your second question) because they decided to use it. The user must then go back to the object to define this functionality or choose a trait that implements it, but at least they get a nice error message. The harder problem is if the object in question is created in an encapsulated unit, then becoming abstract is an unsolvable error.

It isn't clear to me that HasPosition fails to "implement everything expected of it". I used `var Position : Point`, just as your CanvasWidget did. Are you assuming that traits with names of the form `HasPosition` are idiomatically partial in their definitions?

Very interesting! To me, abstractness is not merely about unimplemented members, it is also about whether those members are actually used in some architecture. HasPosition is not abstract because the position field lacks allocated space, but because the position member isn't used yet in any interesting way...to place the widget for example. We don't want to infer the has-position because that position ain't going anywhere without further work. So, for CanvasWidget, the position is being used in a meaningful way, so we can let the user assign it.

The semantic intent of an abstraction is important to a consumer, so you would want to assign a new name for different implementations of position even though structurally they are all the same being all the same type.

How is `semantic intent` represented in your language? I.e. how does your IDE know that HasPosition is intended to be abstract in this manner?

Consider:

p = new HasPosition();
p.Position = (10,100);
p.DoSomethingWithCanvas();

AFAICT, your language would just as easily derive this as it would canvas from a widget.

Has position is marks as not inferable right now. An extender has to extend it in a special way so that the extender itself is inferrable. In this case you can't start from has position and goto canvas widget.

Where is it marked as non-inferrable? What does the code look like?

Right now there is simply a keyword NotInferrable in the trait definition. I'm overloading exclusive inheritance to express extension of a non inferable trait by an inferable trait.

How are you to distinguish some uses as `interesting` or otherwise? If code exists of the form:

def PrintPosition(Console c, HasPosition hp)
  c.Print("Position is ");
  c.PrintLn(hp.Position.toString());

Then it seems I could use Position in interesting ways before it is fully specified whether my object is a CanvasWidget or a FooWidget. And this does not seem unreasonable as a potential `semantic intent of the consumer`.

Also, you seem to be implying some temporal semantics - i.e. "used yet in any interesting way". Do you mean to prevent assigning Position until after we've performed some operation that might use it? Or will developers need to write something like `w.RenderCanvasWidget()` then back up in their code to assign position so it renders correctly?

you would want to assign a new name for different implementations of position even though structurally they are all the same being all the same type

Do you mean to rename all methods and variables? Consider instead code of the form:

trait HasPosition {
  var Position : Point;
  GetPosition() : Point { return Position; }
  SetPosition(p : Point) { Position := p; }
}

I doubt simple renaming would scale very well. You'll one day want to add a new method to `trait Foo` and discover you need to search the entire codebase for every trait that extends Foo so you can rename the method. Also, it would seem to hinder any sort of generic programming or reusable abstractions, such as developing a PrintPosition procedural abstraction.

...

Perhaps it would be better to forbid multi-trait inheritance. I.e. you can inherit from one trait, but more than that is based on parameters. This would structurally prevent the problem scenario, albeit at the expense of some redundant abstraction (like a thousand variations of HasPosition). This could be mitigated by simplifying construction of `views` or lenses.

Whether an extension is interesting or not is under the control of the programmer, the language doesnt try to validate what is interesting or not. As for design, the programmer must decide if the functionality is "hooked up." an interface with just a property is a bad example here, since technically assignment is sound even if it's meaningless. I suspect for real interfaces, there will be less of these kinds of problems (but I admit I like the idea of a non inferable has position interface).

There is no execution temporal semantics, no flow-based analysis. Propagation is timeless, the inferred trait is extended from the site where the value is created.

There is no name resolution in the language, names are only used in the UI for selection and presentation. So no renaming mess to worry about.

I thought I had a good idea of what you were proposing from the initial description, but this bit about abstract methods needing to be hidden leaves me completely lost. Can you or someone clue me in?

When CanvasWidget implements HasPosition, Position suddenly becomes selectable for CanvasWidget, essentially Position has a new full name in CanvasWidget that the user can see/write down.

For example, this comment loses me. Isn't the point of abstract methods that you can invoke them without knowing which implementation you're going to get ("virtual dispatch")?

The problem is that there are different kinds of extension that serve different needs. When we always select our classes explicitly in normal languages, the distinction isn't very important and it's just about virtual methods, as you say. But once we start considering inference, we have to distinguish between the two different kinds of extensions otherwise inference leads to meaningless constructions. Has position is a good example of what we don't want to infer, because it is somehow incomplete, and would add a position that noonewa really listening, while canvas widget's position is clearly being observed by the canvas.

I see. David was asking what happens if you move the definition of "position" to a trait, making it abstract. Does use of position still infer Canvas for a Panel?

In my language, it doesn't, and it's a simple consequence of the rules: in the original case, when you use the symbol 'position', it summons the theory of Canvas, where that symbol was defined, and in David's modified example, it summons the theory of HasPosition, where that symbol was defined. In either case, the inference works the same way. Inferring Canvas in the latter case looks like a bug to me, in the absence of some annotation saying "this is the only Panel that will ever derive from HasPosition."

But as I mentioned in another post, there can be two symbols for position, where one is an abstraction implemented by the other. In this case, the Canvas implementation could have a separate position implementing the HasPosition position that, when selected, does summon the theory of Canvas.

Is that a potential solution to this issue for you? Am I still missing something?

Summoning the theory of has position in any case is a bug; there is nothing more frustrating in a PL than a statement tha fails silently in any "typed" language. If we have multiple inferable implementations of has position, then we must somehow select one.

In any case, the position provided by has position is just not directly selectable on anything unknown to already extend has position, inference simply doesn't work that far; if I want to abstract over just positions, I must do so explicity. Inference can then only "skip" position to select an implementation.

Where things break down, say we have some functionality that depends on has position indirectly, and a widget value hits against that trait in a use. Do we go ahead and infer canvas widget at that point, or still disallow the use of has position in an inference. My current thinking is that a case like has position can never really support inference reliably, and so you just get an old fashioned type error at that point.

Even something like a `DoCanvasStuff` method for a CanvasWidget might infer more than one implementation - because there might be multiple traits extending CanvasWidget. Shouldn't we understand your inference in terms of iteratively narrowing a set? (Even `new Widget()` is just an initial narrowing, right?)

So long as there is at least one Widget with HasPosition, we can infer Position for Widget. Doing so doesn't uniquely select an element; it only narrows the options to CanvasWidget and maybe Schellhas's FooWidget.

Summoning the theory of has position in any case is a bug; there is nothing more frustrating in a PL than a statement tha fails silently in any "typed" language. If we have multiple inferable implementations of has position, then we must somehow select one.

Ok, I see your point and agree with what you're getting at, but I wouldn't phrase it that way for my language. The first thing that happens for me is that HasPosition is summoned, because position is defined in the theory of HasPosition. In that theory is a HasPosition type, which can either be a concrete or abstract type, but in this case is probably abstract. If abstract, it will trigger an instance selection mechanism (similar to Haskell type classes'), which will either locally find a unique instance or issue an error. This is a departure from Haskell, BTW, which will just accumulate constraints (HasPosition a => Foo a). I support constrained types, but require that it be explicit -- by default if constraints can't be solved locally, it's an error.

I had no `semantic intention` of making it abstract. I certainly didn't mark the trait as `NonInferable`. I really feel like Sean pulled the rug out from underneath me on that issue, perhaps focusing too much on HasPosition in particular and not on the possibility of similar patterns.

Rather, I moved the Position value to a HasPosition trait to make its use ambiguous.

I don't find this example (or at least the equivalent in my language) very surprising. If position is defined in HasPosition, then I don't see how you can infer Canvas (which may be one of many instances of HasPosition) from use of position.

Sean, are you saying that you would be able to infer Canvas, absent an annotation of NonInference? If so, how would that mechanism work?

Position is defined in has position but is accessible in each of has position's implementations, in so much that we can give each of these positions new "names" for selection and presentation purposes. We are able to infer canvas widget easily because the programmer selected it's position. Whether has position is in the middle is not very relevant if you are selecting canvaswidget.position.

If the programmer selected the specific position, then that would summon the theory of Canvas, where it was defined. Why do we need any annotations there? Are you saying they are make it impossible for them to select the abstract position of HasPosition? Why?

When the type is abstract, you just want to avoid letting the programmer even select the operation. What I do is let them pick the operation and then later (but still at edit time), use the whole context to select the appropriate instance. This lets you get overloading a la Haskell type classes, rather than forcing the programmer to manually select which operator he wants in each instance.

A difference from Haskell, though, is that I do binding at edit time. Once an instance binding has occurred, I remember it as part of the code so that I can bring it to the programmers attention if it changes. I do something similar with name shadowing. Once a symbol is bound, a nonlocal change that steals that binding should be brought to the programmers attention, IMO.

I should note that the editor for this language will also have differentiation between different symbols with the same short names - either color highlighting, or a modified font, or a subscript, so that which version you actually picked can be subtly inferred by just looking at the code.

I should note that the editor for this language will also have differentiation between different symbols with the same short names - either color highlighting, or a modified font, or a subscript, so that which version you actually picked can be subtly inferred by just looking at the code.

Not sure. I was hoping that revealing inference result would be good enough, but those could be non local. A subscript might be interesting, just assign it a 3 letter code computed from the guid (collisions are still possible, but not likely). The you can even type the name straight without going through selection, but it would also be very difficult to remember many of these codes.....

I was actually talking about how my system works. The short name and unique name are both programmer specified and remapped on import. The unique name can use fonts, funny symbols, and sub/super scripts. But there's lots of possibilities here.

What does ambiguous even mean without name resolution? I'm not proposing that the compiler make an intelligent decision about a specific has position implementation, the programmer is just forced to select one themselves. We can disagree what patterns are real and what ones are contrived, property only interfaces are very much in the contrived area, but I agree they have to be dealt with somehow (hence my non inferable hack).

It means (to me) that the resolution of identifier to storage is not able to be determined automatically by the compiler.

I think that our issue is that programmatically inferred subtyping is nifty and powerful. Programmer directed implementation selection that is hidden from the readable source is (imo) far less-so.

The discussion is trying to figure out where we're forced to use the less good solution and how common those scenarios would be.

Your source code is a tree, you can have multiple views of that and augment it with inferred information. It's not hidden so much as it is elided for readability.

I'm not sure if preserving name resolution is viable or useful. The point of my language is to give programmers more power to reuse, as namespaces that go along with naming really get in the way. We could always hack it in as some augmented intellisense, but then all the problems we talk about here get worse not better.

You aren't resolving a name (you know at edit time that Position uniquely refers to HasPosition), but you are resolving a trait (possibly via intersection of HasPosition and Widget). Ambiguity in context would mean that the trait resolution is not unique by the available information.

My point was that there is no trait resolution. The compiler isn't smart enough to compute that intersection reliably while its not really necessary either. Instead, the programmer pulls in canvas rather directly by select the position in canvas widget, not the one in Has position.

It doesn't take any intelligence to compute a simple intersection on extension relationships. But I can understand choosing against that flexibility in the algorithm. I'm still grasping for the consistency in your vision, though.

1. Would programmers similarly be required to "select the DoWidgetStuff in CanvasWidget, not the one in Widget?"
2. Dropping the `NonInferable` hack, does the answer to the prior question change if we start from HasPosition instead of from Widget?

If the answer to the first question is `no`, I would say you still have trait resolution - albeit, less flexible than it would be with intersection.

Non inferable is special, the members that the trait introduces are promoted in inferable extensions, so the answer to (1) is no.

I'm not sure how to answer (2). Without non inferable, has position isn't a viable trait as far as I can tell.

If there are two concepts named 'position', I require disambiguation of which you're referring to. There is edit time help from the IDE, which integrates with the type system, so that when you type (at the keyboard) "myCanvas.position", the context allows implicit disambiguation of which position you wanted.

Also, there can be two top level symbols named 'position' where one is an abstraction implemented by another, but that abstraction certainly isn't inferred. I don't see that Sean is planning to support anything like that either.

[BTW, it's possible that my ideas on this are far enough from Sean's that my comments here are just going to end up hijacking this thread rather than contributing. Sean, one more reply to me along the lines of your last (which I'll paraphrase as "uh, what?") and I'll take the hint ;)]

Edit: And in regards to my work, it was compiling.

I think we are fairly in sync here. Abstraction is a tricky problem, you can't allow inference of anything, that wouldn't be useful. Instead, you have to limit inference in some way; e.g., implemented positions vs. abstract positions that you would have to implement and would not be used by other abstractions in your program.

Sorry, maybe I'm being dense, but I don't grok this.

In my work with structural typing, there's often the case where name collisions occur between mixins. Sometimes you want the field to be reused/shared; sometimes you want a type/compile time error; sometimes you want some sort of disambiguation.

I've been looking at using context and typing to handle the disambiguation and another mechanism to handle sharing. I suspect that there are practical programmer annoyance concerns with resolving the short name (or due to a library change, having to suddenly specify the unique name when it wasn't necessary before).

I'm curious how you're approaching that. And I'm not great with a lot of the terminology, let me know if anything wasn't clear.

There is no name resolution so name collisions aren't very relevant. The user might have many different positions to select from, even possibly defined in the same mixin (given different implementations), but they are only going to select one of those. What you really want is some way of organizing/ranking your choices so you select the most probably choice more quickly, this can feedback into resolving a "name" if you type something at the keyboard and are not going through a menuing system. Really, we've flipped things around: rather than use types to resolve names, we are using (long/unique) names to resolve types :)

Since you are making direct references to the abstraction, whether the abstraction is renamed or not is irrelevant (the code is stored as a tree and not just text to preserve that).

Then I'm missing something fundamental somewhere. Let's be more explicit then...

In w.Position 'position' is an identifier and some magic occurs to pick CanvasWidget. If you also had

trait FooWidget(c : Canvas) : Widget(c) { var Position : Point; }

defined (likely with a different panel) how does the magic pick between them?

As I understand it, Sean has been saying there would only be one such `Position` abstraction in the whole codebase. I.e. once the CanvasWidget defines the `Position` attribute, the FooWidget cannot also do so.

Presumably, a lot of nice names would be taken while the language is young, and developers will spend some of their time inventing LongDisambiguatingNames to avoid conflicts... or refactoring names used in other projects to free up the politically contested namespace. (Java developers will feel right at home. ;)

This led me to structure a question with the same intention as yours, but using a `HasPosition` trait.

trait HasPosition { var Position : Point; }
trait FooWidget(c : Canvas) : Widget(c), HasPosition {}
trait CanvasWidget(c : Canvas) : Widget(c), HasPosition {}

Now it seems to me that Position is ambiguous. However, for a reason I've yet to grasp, Sean claims that the HasPosition trait is `somehow abstract`.

They are different positions, so you have to pick one or the other. You select what you want, the names are just for display/reading/documentation.

So the inference only occurs in those ideal scenarios when there's no ambiguity?

How would that 'picking' look?

There is no ambiguity at the compiler level since there is no name resolution. "picking" is a IDE concern, if you are on a tablet, then you have menus; this is what I have implemented right now. The menus are constructed to show enough of the full name to disambiguate choices on screen.

For keyboard entry, you really want some kind of name resolution; I haven't implemented this yet. I'm assuming we have the tree available, so we know what the context of an edit site is in real time. Then you type the name, and get choices in real time based on partial name matching. Like programming with more autocompletion than usual.

I'm fine with an IDE/autocompletion sort of answer (I'm just curious), though I have reservations about problems a programmer reading the code might have.

I wonder if it would make sense, in case of ambiguity, to throw a compiler error and demand manual specialization i.e. creation of w using CanvasWidget instead of Widget. This can be relaxed as more attributes are used whose access provides more context again.

It's an interesting idea to play with.

I'm thinking perhaps a strong warning (error-like) while selecting the better option (or random if we can't decide what is better). Another idea I'm playing around with is that their are no errors that will stop your code from running so the code is always testable and you have something to look at to make changes (you might not know what you want yet).

Dependency hell (aka DLL hell) is where I want to be :) First we make code easy to find and use, then we create a code wiki where everyone can easily break and then fix each others code, and then we declare a socialist Utopian code paradise! Obviously my ideas on how to handle version conflicts are not conventional.

Refactoring would appear to actually be quite easy given the lack of explicit type annotations combined with tangible symbol reference. That means I can take some arbitrary block of code and just reuse it somewhere else as is.

I've done a lot of idle ruminating about code wikis over the last six years. And while cross-project sharing and refactoring is certainly a big motivation for them, wikis won't miraculously offer paradise of any sort.

Developers will have all sorts of legitimate concerns - especially regarding security, safety, stability, and certification. Just how do you like your spam? I certainly don't like mine compiled deep into my code.

Evolve the vision: rather than one big definitive wiki, I see a graph of wiki-cells that push and pull code in a DVCS manner. There are still de-facto commons wikis where people eventually push most projects and code, but developers are protected by buffers and membranes - intermediate wikis can be better vetted, an implicit ten foot pole to the bleeding edge, protection against premature commits of untested code to the commons, a clear terrain in which to express administrative policies and control propagation of intellectual properties.

We lose the socialist utopia, but still there is much value to be had by interaction, discovery, and refactoring between projects - both within a company and in the broader community.

Anyhow, once we have these cellular wikis, it is clear that the issue becomes: how do you cherry pick some code from one wiki and push it to (or pull it from) another? Namespace entanglement remains a valid concern - can we take the low-hanging fruit without grabbing the whole orchard? Similarly, consistency and versioning will remain relevant issues.

Dependency hell might sound fun, but - like a barrel of monkeys - it can prove quite horrifying to those who encounter it in real life. Socializing code is not a substitute for a good module system.

I want to create the problems first before I can solve them. So first solve the namespace/finding things problem, then that opens up the other problems for analysis. Often the way we plan to solve these problems does not match how they actually manifest in practice. I'm really looking at Ward Cunningham's experience with C2 here, all the problems people thought it would have didn't come out as anyone expected (though the problems definitely exist, the solutions are fairly simple). He built the simplest online database first, and everything else really changed after that point that new thinking was required.

For relevant experiences from C2, I suggest you study the motivating forces behind the development of sister wikis, and the reasons those efforts have utterly failed. You might also study the vast proliferation of wikis and understand what that really means for your socialist utopia. Are you looking forward to a society of independent city-states?

Wiki is a roaring success, but leaves many interesting and relevant problems unsolved. We should recognize its failures - even though they might not be as well advertised as its successes - and learn from them.

I was wondering about this, so you are fine with some foreign code changing the meaning of your own code?

If I understand right, simply using a particular trait can change the implementation of a variable. Even if this variable comes from another module. How does this affect future uses of the variable?

Yes, external code can influence the makeup of the objects an encapsulated unit creates, but at at least the changes are only additive. Since use affects makeup of the value, the question becomes how does use of a variable affect past creation of values bound to it, definitely a weird question and mindset

As for usability, I'm not sure how bad pollution would be in practice, I need to look at some more use cases.

I thought the extension could be destructive, eg. replacing one implementation with another by selection.

Even if it is only additive, this means existence tests (can this duck quack?) depend on use. Not sure it is a problem in practice.

Actually, existence tests are a big out in the language. As soon as you ask if a value is a duck explicitly, and control flow is under that, then you don't need to infer duck on quack. In fact, it's much weirder than that, if I test for duck, then moo on the resulting value, then we get this case where only values that pass the duck test become cows. This necessarily makes our graph more complicated, and things get interesting if we add case matching to the language.

If I understand the design correctly, it seems to suffer from the usual problem of structured editing -- not letting you pass through invalid states on the way to the goal. Though if Sean has mobile in mind, he may be willing to accept bigger inconveniences here than he would for a keyboard interface.

Inference assumes correct states, explicit selection does not. You can still express bad code, we just won't list those options with high precedence. if you are typing you can screw up your code quickly.

Anyways, that is a separate issue. Inference allows us to have cake and eat it too, that the above code is still correct...and inference really opens up the order problem of structured editing.

What? Accessing position has and always will bring in canvas. Has position is not inferrable but canvas widget definitely is, while canvas widget inherits a position from has position that the prgrammer is free to acess with full inference. We seem to be stuck on whether the prgrammer can only accesss position from the has position trait since it is defined there, I'm saying that's not the case; the inherited position is visible and has a unique name that identifies it as a canvas widget position. the programmer might see:

position (canvas)

in there intellisense and select that. Again they aren't exposed to has position at all, as this is an abstraction that isnfor abstraction producers who can refer to it directly.

I know that is weird, we generally think about member declarations as being fixed in space while only their implementations can change during extension. But that just isn't the case here.

Accessing position has and always will bring in canvas.

We might not bring in CanvasWidget (which HasPosition) if FooWidget also HasPosition.

Using some sort of unique names under-the-hood to distinguish the HasPosition options is feasible, but I'm having trouble resolving it with use of other names. Consider a method `DoWidgetStuff` from `Widget`. Do developers also see:

DoWidgetStuff (canvas)

in their intellisense and select that? Under which conditions?

If there are multiple dowidgetstuff methods you'll see some sort of disambiguator. But members of non inferables are special in that they are promoted down to inferable extending traits for selection purposes, so one "declaration" in the inferable trait can lead to multiple choices; such as lots of position choices even though it was only declared once.