Lambda the Ultimate

I think the expression problem seems to present a simple, clear-cut benchmark where the user has to write a lot to please the typechecker, while what he wants to achieve is both pretty clear-cut, and a frequent, natural evolution of his code model over time.

I rather see it as a natural consequence of closed algebraic types, which are simply the typical semantics of sums and products in typed languages. I don't think it's specific to types, though typing makes the problem harder.

The definitive solution is on the front page of LtU: Extensible Programming with First-Class Cases. It requires extensible records, although Oleg pointed out in that thread that you can achieve this sort extensibility in Haskell now using a finally tagless encoding.

Right, since we just had a related discussion recently, it's worth reiterating that: The expression problem is not specific to types.

Broadly speaking, it's the problem of allowing extensibility along two orthogonal axes (data and operations), in a way that enables combining all possible extensions freely, without having to modify either of them, or requiring whole-program compilation. (IOW it is the problem of overcoming the modularity dualism of function-oriented vs object-oriented design, each of which only supports one axis directly.)

No existing language has direct support for this, but they vary in how hard (or impossible) they make it to construct suitable abstractions manually, using the "natural" mechanisms available (especially, the preferred dispatch mechanism of the language).

When Wadler says the expression problem is "an old name for a new problem", he is referring to John Reynolds' paper available as re-print in Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design, eds. Gunter and Mitchell. In that paper, Reynolds gives the canonical example re-used by William Cook in his three papers on OO vs. ADTs: abstraction of integers.

Reynolds refers to the problem as about data abstraction. Wadler refers to the problem as about typing the data abstraction incrementally and iteratively. Reynolds contribution is the canonical example used to understand data abstraction, and loose principles suggesting the example demonstrates a fundamental abstraction problem. The contribution by Wadler thus seems to be a formal method for evaluating how we can "have our cake and eat it too": rather than questioning whether it can or can't be done, provide a system where it is or isn't okay as judged by a type system. Furthermore, once the type system has checked a modular piece of the solution, it must never go back and re-check. For example, old constraints should never be invalidated by new ones, so why should the algorithm revisit checking old constraints? Only if the constraints themselves pose modularity problems (can't be composed), which seems unacceptable since we might not have control over that. This guarantees extensions are type safe and modular.

In other words, since Wadler introduced the notion of using a type system to evaluate solutions, it is a modularity problem for type systems.

I hope that is clear.

I believe the expression problem is also synonymous with the extensibility problem, which might actually predate or at least is concurrent with Wadler's description (see Flatt and Findler's Modular Object-Oriented Programming with Units and Mixins in ICFP '98).

After Martin Odersky chided me last year for saying the two problems are essentially the same, I'd rather deal with the two as separate problems. I am aware that some, such as Mads Torgersen, feel they are identical problems and Mads has expressed this sentiment in a peer reviewed paper. The two general problems are:

1. Expression Problem as statically typing extending data abstractions with both operations and data.
2. Extensibility Problem as dynamically extending data abstractions with both operations and data.

Furthermore, the Extensible Visitor problem posed in the link above motivates both with a datatype-generic programming language puzzle. In other words, both problems share the same test cases, but not requirements. The words necessary condition and sufficient come to mind, both for comparing the two problems and within each problem.

It is obvious from Odersky's extra Expression Problem criteria that the sufficient bar is raised for type systems, but it is less obvious how to raise that bar for dynamic languages. Recently, Gilad Bracha wrote a blog post that Types Are Anti-Modular where Wadler suggested two forms of modularity are necessary to understand the difference, and then asked Gilad, "I would claim that the additional checking offered by S-modularity is more important to separation of concerns than the independence offered by I-modularity. What is your argument against my claim?"

Note that I replied to Phil. (Personally, I love Phil's framing of the argument, since it jives with my viewpoint that type systems are partitioning barriers, and that programs are nodes in a distributed network.)

We can also consider the Inheritance Anomaly problem in concurrent object-oriented languages as being a separate challenge for objects rather than datatypes, with its own criteria necessary for hidden state:

1. History-sensitiveness of acceptable states.
2. Partitioning of states.
3. Modification of acceptable states.

Disclaimer, I'm inherently biased given that I worked closely with Matthew on this. Jiazzi is completely statically typed and solves the extensibility problem in a modular way via the open class pattern, which involves mixin composition and recursive linking (i.e., static modular type checking). I don't think Matthew ever made a distinction between static and dynamic typing, just because you promote the problem in a dynamic typing context doesn't mean it does not apply to static typing as well.

We completely solved the problem given Wadler's generic criteria, I remember trying to explain this to Wadler a long time ago when he gave a talk at our school, but I don't think he was very interested in our solution; probably because we weren't using his preferred method of functional case-based dispatch, rather we were using OO method dispatch. You can't just define a problem generically and reject solutions that don't use your preferred form of dispatch. And this is really the crux of the differences between the extensibility and expression problems: formally they have the same solution requirements, just that the expression problem has the hidden requirement that only case-based dispatch is acceptable.

I've come to the conclusion that the expression and extensibility problems are really red herrings. Yes, its a nice type puzzle, but when you add that operation to an existing super-type, you've broken all your sub-types anyways, whether you can detect the breaks in a modular way or not. The usability problem is already much greater than whatever type problems we might have. In some sense Gilad is right.

You call it a hidden requirement, but it is pretty clearly stated.

I realize practical people find it profoundly stupid to differentiate, but it might actually be a useful thought tool.

Ah, then that explains a lot: the expression problem is just a special case of the extensibility problem with constraints of interest to a certain style of programming.

Well that was a great link. And a terrific summary as well. Just to repeat here in case the blog discussion goes away:

Philip Wadler
S-modular: supports separate compilation. Every module has an interface and a source. Compiling a module requires access to the interface, but not the source, of every module the compiled module depends upon.

Your motto becomes 'Types are anti-I-modular', which is unarguable.

Z-Bo:
The Expression Problem deals with the fact that I-modular is impossible in typed languages, so S-modular is the best we can do when extending both functions and/or data.

We are used to type systems where a type can be inferred for a term in a given context. Everything that belongs to the context have to be given beforehand, including the interface of external modules.

This is not the case of all type systems, however: there are I-modular type systems. This is the case of the simply-typed λ-calculus for example: given a term M without any environment you can infer an environment Î" and a type Ï„ such that M has type Ï„ in environment Î". This is actually relatively natural: when you encounter a free name (or a reference to a value of an outer module), you can make a general assumption on its type (an unconstrained type variable), then refine this assumption according to the uses of the name throughout the term.

This property is lesser-known because it doesn't hold for type system using universal quantification â€" Hindley-Milner, System F and the like â€" you cannot guess polymorphism in a most general (principal) way, so you need to be given a type environment for at least all polymorphically-used free names.

There is a family of type system that preserve the "guessability of the environment" and is more powerful than simply typed λ-calculus : intersection types. The community working on intersection types (in particular J. B. Wells) attach a lot of importance to this property. They say that those type systems have principal typings (couples environment,type can be inferrend), while HM and derived only have principal types. However, those intersection type systems haven't found much practical use yet, because they can be less natural, more complicated, and there are theoretical reasons they may be impractical.

Summing up: there are I-modular type systems, but it's difficult and doesn't work well yet.

This is not the case of all type systems, however: there are I-modular type systems. This is the case of the simply-typed λ-calculus for example: given a term M without any environment you can infer an environment Î" and a type Ï„ such that M has type Ï„ in environment Î". This is actually relatively natural: when you encounter a free name (or a reference to a value of an outer module), you can make a general assumption on its type (an unconstrained type variable), then refine this assumption according to the uses of the name throughout the term.

Indeed, this is what I (perhaps obtusely) suggested on Bracha's blog by pointing to the paper on inference for first-class messaging. I-modularity is simply an inference pass which automatically parameterizes a module by objects with the given signature. Matching types then occurs at a configurable link time.

However, Bracha's actual point was: I-modularity and types, or encapsulation, pick any one. He complained that inference "leaked" too much information about the implementation. I'm not sure this is a legitimate complaint though, because programs that don't leak the information required for a successful evaluation, may not run at all.

I agree with you. The whole thing seems to define the notion of module.

The purpose of a module is to be a bunch of code that does a list of stuff (A module is a self-contained component of a system which has a well-defined interface to other components of the system). The point of the module is to allow you to use the list without needing to know the bunch of code. Needing to know the list is fundamental to the module. A module "leaks" exactly what is exporting, the leaks are the point of the module.

What does it even mean to say I want to use modules without knowing what's in them. What is the compiler supposed to do? There is a call for function X in module Y. I could imagine some sort of heavy runtime linking that might be able to handle these calls generically, but I'm unsure what advantage it would have.

It's not uncommon to implement plug-in functionality via modules that are loaded dynamically, at runtime. What it means to "use modules without knowing what's in them", in this case, is that the program using the plug-in module may use the facilities provided by the module without knowing how the module was implemented, in much the same way as an OO program can use a subclass via an interface defined by one of its superclass without caring about the specifics of the subclass.

For example, imagine a file browser; it might want to handle network shares transparently in a similar way to how it handles the local file system. So it might define a module interface with a list of required functions, and some data structures for communication. But the browser program does not need to know how the module is implemented, and shouldn't need to know; the maker of the file browser is not able to predict the future to implement all user requirements, so using this technique lets third parties fill in the feature gaps.

The above file browser example is concretely implemented by Windows Explorer - which can browse any "namespace" provided by a set of COM interfaces - but the notion of the module boundary is relatively ad-hoc with COM, relying on documentation and experimentation for successful implementations. It could be a lot better with a well-defined module interface.

As to inadvertent exposure of implementation details, this is a problem common to most definitions of abstraction boundaries. If too many implementation details are exposed, then the module interface is too specific to the initial set of implementations, and its very modularity is at risk.

may use the facilities provided by the module without knowing how the module was implemented

I agree it is fundamental to understand how to use the module without knowing how they are implemented. This S-module independence seems to be aiming for using the module without knowing precisely what it is abstracting away. In most (all?) languages people are given header files or type definitions which tell them what's in the module without them knowing how to implement those functions.

Being a bit C biased here:
The compiler needs to know what the module is going to do.
The linker needs to know how the module is going to to do it.
And allowing for knowing what but not how is essentially the advantages of modular compiles.

I don't think header files tell you the how, for example the very first QT object (i.e. first file is Q3 Accel) in the header file is:
Q3Accel ( QWidget * parent, const char * name = 0 )
Q3Accel ( QWidget * watch, QObject * parent, const char * name = 0 )

Which is the constructor of keyboard shortcuts. Knowing how to compile it in, doesn't tell you much of anything about how it was implemented just how to use it. For example of an implementation detail. I don't know if after having received a command event which requires blocking standard keyboard input if the system looks ahead in the stream of key data to see if it can grab more commands / events or does them asynchronously.

So it might define a module interface with a list of required functions, and some data structures for communication

Exactly! That's a header file. The way I'm reading S-module is that the language operates without a specified list of required functions nor a specified data structure, because that is implementation leakage. It is hard to imagine even what something like that would look like.

The way I'm reading S-module is that the language operates without a specified list of required functions nor a specified data structure, because that is implementation leakage. It is hard to imagine even what something like that would look like.

Would it look like Java? I thought each .java source file was compiling independently without regard to its dependencies and then things are wired up at load time. If it turns out your code is using a type incorrectly you get a class load exception. I'm not a JVM expert though, so maybe I'm getting it wrong.

At compile time, .java source files with their dependencies are loaded by the compiler for static type checking. At run time, .class files with their dependencies are loaded by the JVM for execution. The class load exception results when the .class file dependencies loaded were not compiled from the .java file dependencies originally checked against. The problem is known as one of binary compatibility. You still need the dependencies at both phases, even if they eventually don't agree.

I could imagine some sort of heavy runtime linking that might be able to handle these calls generically, but I'm unsure what advantage it would have.

Indeed, that's exactly what many languages try to do, for instance, via multiple dispatch and predicate dispatch. Gilad prefers single-receiver methods though, so what he wants is something that infers the messaging signature of a module, without tying it to any specific types unless they are specifically declared.

So a program:

module Bar =
 let x = Foo.create() in
 let y = x.baz "foo!";;

would infer something like:

module Bar(Foo<'a> : { create : unit -> { baz : string -> 'a } })

Basically, every name used in a term implicitly parameterizes the parent with a value containing a path dependency for that name. The concrete values satisfying dependencies are resolved only at top-level, perhaps via constraint search, dependency injection, etc.

No typed language that I know of has taken this sort of highly abstract approach, but it looks doable given current inference techniques. The inference for first-class messaging I linked to on Gilad's post looks like it could do it, for instance. I expect the properties you could infer would probably be much weaker than current typed languages though.

What Are Principal Typings and What Are They Good For?, Trevor Jim, 1995.

Thanks, that makes some sense about the inference. I'm not sure I understand the point though.

1) As you mention the inferences about Foo don't do anything. The type inferences are still weak. If I use Foo a lot maybe they catch a type error via. conflict but if the language allows for polymorphic functions they can't even do that.

2) I'm still hard pressed to see the advantage over just telling the compiler what Foo's type is. Because in the end presumably for that code to do anything I need to link with the actual Foo which has actual restrictions.

I might be being ignorant or thick here, but I'm hard pressed to even see a possible advantage.

As you mention the inferences about Foo don't do anything. The type inferences are still weak. If I use Foo a lot maybe they catch a type error via. conflict but if the language allows for polymorphic functions they can't even do that.

Really, it eliminates nominal typing by default and just infers and matches everything structurally, unless explicitly told otherwise. So it kind of inverts the approach taken by most typed languages.

I'm still hard pressed to see the advantage over just telling the compiler what Foo's type is. Because in the end presumably for that code to do anything I need to link with the actual Foo which has actual restrictions.

Think of it like this: by default, this language makes everything a structural interface. That means even if you developed mutually recursive modules A(B) and B(A) together, they are not actually dependent on each other(unless you declare this explicitly), and you can replace A or B at any future time with modules that satisfy the interface. That's sort of compelling, and you can see why Gilad would like that coming from a dynamically typed language.

I think his first point is: this kind of type inference doesn't catch the errors you want to catch. For example it won't even catch a typo in "create".

His second point: nominal types aren't just there for ensuring that the method arguments and return types match up. They also convey semantic meaning and restrictions on what you should do with the data beyond the structural types. For example if you pass a Person with a name to something that expects a Car which also has a name, then that is an error you don't catch.

For example it won't even catch a typo in "create".

It would catch it at link/instantiation time. When that is exactly, is up to the developer. Could be at runtime for dynamically loaded plugins, or could be at compile-time.

nominal types [...] also convey semantic meaning and restrictions on what you should do with the data beyond the structural types. For example if you pass a Person with a name to something that expects a Car which also has a name, then that is an error.

I agree, which is why I said the typing is kind of weak as a result.

Then again, an argument can be made that whatever code you have that expects a car but requires only a name is itself improperly classified. Clearly it's more general than a function just operating on cars, since it's well-defined on any object that has a name.

Edit: and you can imagine how this might facilitate more reuse by forcing developers to classify objects very abstractly.

As always, it's a trade-off between catching more errors earlier and disallowing more valid programs.

Anyway, I think a modification can eliminate both problems at the cost of having to declare more types. Structural types make method names important in much the same way that languages like Ruby and Python make method names important. In a way they remove lexical scoping and have methods be globally scoped by name.

If instead you made method names module scoped, you could catch both typos and errors where you pass another object that happens to have a method with the same name. So the module that has Car in it will have a different name method than the module that defines Person. Sometimes you do want to have classes from different modules to have the same method. In that case you'd have to have a parent module that defines the method that the child modules implement. It's like defining a separate interface for each method:

 interface HasFooMethod<A,B,C> {
 C Foo(A a, B b);
 }

So if you had vehicles Truck and Car and a different module with Person, you'd have two different interfaces containing the same Foo method, but because they are different interfaces the type system won't let you mix up a Person's name with a Car's name.

If you're within a module, the compiler would automatically define an interface for you. But when you call methods from different modules, then you have to explicitly declare e.g. "method Foo" in that module. This way you'll still catch all typos (because the possible set of methods you can call is statically known at each module) and methods can't be accidentally mixed up across modules. On the other hand, you have to explicitly declare methods when two modules inter-operate, but perhaps that's not such a bad thing.

Bad idea, or could this work?

As always, it's a trade-off between catching more errors earlier and disallowing more valid programs.

I don't think the approach I described avoids catching errors early. At worst, it just redefines what it considers an error to allow all compositions that structurally match; basically, all name-equivalent isomorphisms come for free, and all other isomorphisms are simply a name remapping.

Your proposal seems to break this advantage. I'm not clear on whether it would allow ad-hoc rewiring after the fact either.

In any case, I'm not convinced this approach is necessarily bad. At worst, it seems to approach Cook's distinction between ADTs and OO, with this proposal falling on the OO side. This is exactly where Gilad falls too IIRC.

If you redefine "error", then sure. Most times we have some idea of error beyond "there exists an input that doesn't make this function segfault" though, which is what you get if you take this approach to the extreme. We hope that the errors signaled by whatever type system we have somehow correlate with what we consider an error, so that we can get things done with lower costs.

I agree that's what we generally want with types, but I'm not convinced that current approaches strike the right balance either. Something like this inference does have certain reuse and composition advantages which you have to try really hard to achieve in Haskell and ML.

Furthermore, dynamic typing enthusiasts don't agree with your argument. Perhaps a language like this would be a good gateway drug to static typing. ;-)

Well defined may not be enough. The question is also one of useful and tested.

Lets take a simple example of a trig library written for a real numbers in a dynamic language and then applied to complex numbers. It may very well be that the functions run without crashing, but do they produce correct results? Do they have all sorts of new bugs? Are the answers meaningful or right.

For example in a real number library I might see absolute value implemented like:
abs x = if x < 0 then neg x else x

which obviously doesn't work for complex valued x even if x < 0 doesn't throw errors, it might just always be false (i.e. complex < is defined in terms of modulus which is never less than 0).

I'm not sure what plus I see to forcing data into a module that very little is known about that the module is not equipped to handle. What is the upside?

It may very well be that the functions run without crashing, but do they produce correct results? Do they have all sorts of new bugs? Are the answers meaningful or right.

I think a better question is whether we should be using names to distinguish well-defined from meaningful answers. Can the inference algorithm infer enough properties that the signatures required are guaranteed to be "meaningful"? I don't know the answer.

As for "abs", it is a well-defined operation for any object that implements "<", "neg" and "0" methods:

abs('a { (<) : 'a -> 'a -> bool, neg : 'a -> 'a, (0) : 'a }) : 'a -> 'a

But comparison operations are not defined for complex numbers, so this wouldn't actually compile when providing a complex number. I think you were assuming another signature would be inferred, perhaps something like:

abs('a { (<) : 'a -> real -> bool, neg : 'a -> 'a }) : 'a -> 'a

I'm not sure this would compile either, unless you explicitly defined a "<" with that signature. That seems unlikely though. I wouldn't say the first signature to type the implementation you provided isn't meaningful.

I think looking at William Cook's work on OO would be illuminating (see the link in my other post). It very well could be that you can't express certain meaningful operations without absolute knowledge of the representation, which means they must be provided as a private methods and/or must be explicitly tied to a nominal type. I'm not convinced that's been definitively proven though.

Edit: in case I wasn't clear, re:meaningful and tested, I don't really know the answer. I don't know that this has really been explored either though. Cook's papers on OO are the closest work I could think of to this approach.

Edit 2: actually, to make it even more abstract, the signature for abs could be:

abs('a 'b { (<) : 'a -> 'b -> bool, neg : 'a -> 'a, (0) : 'b }) : 'a -> 'a

Can the inference algorithm infer enough properties that the signatures required are guaranteed to be "meaningful"?

Probably not. But the documentation can, and if the module has to provide documentation then it might as well provide type signatures for the functions.

As for the specific case, there is a standard partial ordering on the complex numbers:
x+iy < u+iv if and only if x < u or (x = u and y < v)

there is also magnitude partial order
x+iy < u+iv if and only if x^2 + y^2 < u ^2 + v^2.

The problem I was giving is not neither one of them works in the definition of absolute value, designed to degenerate for non reals. The one you are giving that depends on neg, < and 0 won't work either. Use either of those definitions above and check for yourself you still don't have an absolute value.

___

I don't want to get too caught up in this example. My point was that I don't see much advantage to pushing into a module that is not designed to handle it and expecting desirable things to come out. You have to know a lot about a module (essentially white box) to know how it is going to handle new data types and if you know white box information, you know the black information that Gilad seems to be trying to avoid.

I'm still hard pressed to think of how something like what he wants would even be possible.

The one you are giving that depends on neg, < and 0 won't work either. Use either of those definitions above and check for yourself you still don't have an absolute value.

I agree, but only because there isn't a total order on complex numbers. Trying to call this implementation of abs with a complex number will fail, which is what we want.

I think a better example that we can all agree is wrong would demonstrate the real problem, if any. Consider:

foo('a { (+) : 'a -> 'a -> 'a,
 (>=) : 'a -> 'a -> bool } )
let alwaysTrue x y : 'a -> 'a -> bool = y + x >= x

This would always be true for standard numbers. Now consider an orderable type 'a where <= and >= are swapped such that 'alwaysTrue' is false (or consider 'a=string, (+)=concat, (>=)=alphanum_gt_or_eq -- note, if y + x is reversed to x + y, then >= is true again). This is an example of a program where assumptions about ordering are violated, but those assumptions are not captured in the inference or reflected in the signature.

1. What kinds of errors could result from this? For instance, would we accidentally launch nuclear missiles, or crash a stock market? That seems possible.
2. Does making abstraction the default, the reverse of the current status quo, make these errors more likely than the status quo's defaults? You're vulnerable to this problem if you use type classes or functors, but in that context you're explicitly abstracting so perhaps you're more aware of these problems. It seems reasonable to believe that these errors will be more likely.
3. Is there a way to mitigate this problem in abstraction-by-default? For instance, could you infer a relation between (+) and (>=) and display that in the signature as well?
   

   foo('a { (+) : j:'a -> i:'a -> 'a,
    (>=) : 'a -> 'a -> bool } where i + j >= i )

   This would certainly address your concerns, but I expect checking such constraints to be undecidable in general. I'm not well versed in dependent typing state of the art, so I'm not sure how difficult that would be to infer at this level, or in the modules which define 'a and its operations.

I agree, but only because there isn't a total order on complex numbers. Trying to call this implementation of abs with a complex number will fail, which is what we want.

No that was my point it wouldn't fail, it would return garbage. Lets use the magnitude partial order for < and x = -3 + 4i. Remember the correct answer (i.e the standard definition of absolute value for complex numbers) is 5.


abs x = if x < zero(x) # zero(x) = 0 + 0i so this is never true.
then neg(x) else x # returns -3 + 4i


Now lets use the standard partial order

abs x = if x < zero(x) # zero(x) = 0 + 0i, and -3 < 0 so this time it's true
then neg(x) else x # returns 3 - 4i


So not only are both answers wrong, they are both different i.e. the implementation does leak through, but they both compute fine. They don't fail, they appear to work, they just return the wrong answer. From the code's perspective GIGO but from the user's perspective it may not be so clear.

What I still have trouble seeing is where this S-module produces upside. What is the upside of creating these sorts of bugs casually?

No that was my point it wouldn't fail, it would return garbage.

No, it would fail because < does not exist for complex numbers. The ordering relations you specify are very specific partial orders, as you yourself have noted. Any complex number package that provides by default a < implementation based on such a partial order is incorrect.

For this example to succeed, the developer calling abs would have to explicitly remap magnitude_lt to <, and he would have evaluate whether that partial order is appropriate for his domain.

The example I provided is less objectionable IMO.

What I still have trouble seeing is where this S-module produces upside. What is the upside of creating these sorts of bugs casually?

Because it approaches the expressiveness of dynamically typed languages with its lack of type annotations. Even module interfaces aren't needed.

Any complex number package that provides by default a

Those are both standard meanings of < in that context. It is the sort of polymorphism does when dealing with complex number. Further the 2nd example is a full ordering on the complex numbers, not a partial ordering. Not that that matters, < is defined in terms of a arbitrary relations having certain transitive properties that partial orderings fulfill.

But there's no natural ordering on the complex numbers that preserve its properties in all contexts, like the ordering on naturals. You can see this in every complex number package you'd care to name. This is why Haskell's, C++'s, OCaml's and Python's [1] complex number packages have no default comparison operations. It's simply a mistake to provide such a default, so the sample you provide wouldn't compile out of the box.

You could provide your own comparison function which compares complex numbers as you state via projection into a domain with a natural ordering, but the appropriateness of this projection is domain-specific, and you can do this in Haskell as well. This is the danger of overloading, period. The inference approach discussed here simply allows overloading by default. I agree there are some additional dangers, but there are benefits as well in code reuse and abstraction.

[1] "The <, <=, > and >= operators will raise a TypeError exception when any operand is a complex number."

Where are the actual methods coming from in your example? Do you call 0 as a method on the argument? abs(x) = if x < zero(x) then neg(x) else x

Or are you thinking about some kind of multiple dispatch/type class mechanism? How can structural typing be combined with multiple dispatch?

Yes, literals are transformed by the compiler into a method call on something like a type class dictionary, the signature of which is provided between the brackets of "abs". The dictionary is resolved the caller's context. Whatever and however 'a and 'b are resolved in the calling context, they must have neg(x), (0)/zero() and (<) methods defined.

How do you reconcile that with dynamic dispatch? How would you define a (<) method? Or are you doing static dispatch (possibly with explicit existentials for dynamic dispatch) a la type classes?

Also, wouldn't this result in extremely complicated inferred types for any real world size code?

How would you define a (

I'm imagining something like type classes, but the specific dependency resolution doesn't really matter; the specific functions/methods invoked are dispatched through a vtable/dictionary. I wouldn't classify type classes as static dispatch any more than interfaces in C# are statically dispatched, so I'm not sure if that answers your question.

And yes, the signatures would be rather elaborate. Creating a syntax to make this readable would be challenging. Gilad wanted independent compilation, so all type information to be generated locally; I don't think there's a way around it.

interface Show { string Show(); }
...
List<Show> x = ...;
list[0].Show();

If you want to do that with type classes you need to use an existential.

abs('a { (<) : 'a -> 'a -> bool, neg : 'a -> 'a, (0) : 'a }) : 'a -> 'a

Would translate as:

class AbsReq a where
 (<) :: a -> a -> bool
 neg :: a -> a
 zero :: a
abs :: AbsReq a => a -> a

And as interfaces in C#:

interfave IAbs<T>
{
 bool LessThan(T lhs, T rhs);
 T Neg(T value);
 T Zero { get; }
}
static T Abs<T>(IAbs<T> dict, T value) { ... }

You could require T to implement such an interface, but that limits ad-hoc extensions. The most general canonical pattern is the explicit dictionary passing, like IComparer, IEqualityComparer, etc.

Are you going to have dynamic dispatch? Subtyping?

For example, in OO with structural types you can map Abs over a list of heterogeneous objects if each of the objects has a method Abs. Another example is a binary tree with OO: you have a Node(left,right) class and a Leaf(value) class, and these have methods that dispatch on them, like Leaf(value).map(f) = Leaf(f(value)) and Node(left,right).map(f) = Node(left.map(f),right.map(f)).

I'm not sure what you're after. All these issues seem orthogonal to this thread on inference.

Unless you're asking whether the inference can or should be inferring existentials? I can see answers either way, so I don't have anything definitive to say on that.

Certainly if you have an OO language something like existentials would be required, or you'd take Cook's approach and eschew existentials entirely (if I'm remembering his approach correctly).

Perhaps I'm not understanding your approach. Do you intend for the programmer to write abs like this:

 abs(dict,x) = if dict.lessthan(x,dict.zero) 
 then dict.neg(x) else x

Or like this:

 abs(x) = if lessthan(x,zero) 
 then neg(x) else x

And infer the dictionary passing? If the latter, then you'd have to use existentials in code that uses dynamic dispatch. For example how would you write a function that calls ToString on all elements in a list? Does inference produce the type ToStringReq a => [a] -> [string], or "[exists a. ToStringReq a => a] -> [string]" where the type a can vary in the list? OO programmers expect to be able to do that.

And infer the dictionary passing? If the latter, then you'd have to use existentials in code that uses dynamic dispatch.

The dictionary is inferred, but existentials aren't needed here, you just need a type param (in my examples reified as 'a). I agree an existential must be inferred in cases where they are needed, but that's kind of tautological. I don't know what specifically would be inferred though when trying to pack two different types into a structure, because it's all hypothetical at the moment.

Perhaps an HList would be inferred and not an ordinary list, in which case an existential is not needed.

However, Bracha's actual point was: I-modularity and types, or encapsulation, pick any one. He complained that inference "leaked" too much information about the implementation. I'm not sure this is a legitimate complaint though

IMHO this is a ridiculous complaint in this context, where Bracha uses it as an argument against types -- certainly, having no type information at all leaks at least as much information.

See also the previous discussion.

I think Gilad's concern is the type system implementation has a bug in it, and so takes power away from the programmer and pushes the power into the implementation. And it's not necessarily that it infers the wrong type, but perhaps it disallows valid type definitions as compared with the spec. We know these sorts of problems exist in the real world. naasking recently filed an interesting one with the CLR folks. In the worst case, fixing the bug is a breaking change and so prior code is dependent on the bug to work correctly.

And you might say, "Well, we'll just prove the type system correct and generate an implementation". Well, that has a trade-off, too. This isn't a zero sum game. Some type systems have remarkably long proofs as compared with their implementations.

The reason I am guessing Gilad's concern is "What's easiest to implement and gives power to the programmer?" is from reading his blog posts over the years, and listening to his talks.

Postscript: Do you think that concern is illegitimate? Even if I am putting words in Gilad's mouth, it is something I think about... It's a real trade-off I am curious about.

"What's easiest to implement and gives power to the programmer?"

What power does he see this giving programmers? The power to do what. If he wants the power to just ram data into routines without any kind of type checking... use void pointers in C or program in Forth. Other languages allow this through more or less direct mechanisms. I agree that is power, but generally there is no abstraction about what is going on, the programmer just admits they are bypassing the type system and breaking the abstractions and protections. What is the power of doing this automatically without being ultra aware you are doing it?

Even your naasking/Microsoft example points this out, Microsoft says "we can't add it". Which seems to be Microsoft telling naasking that their code doesn't support what he wants to to. Maybe it should, it seems like it should, but getting that error seems like a lot better than not getting an error and having the compiler silently produce not working code.

It does seem to me that Gilad is asking for the type safety of a no/weak typing language with the performance of a high level language. And yes that concern seems illegitimate so far. Maybe I'm being thick but I'm not seeing it.

If you can't do something that in theory you should be able to do, then you are going to still do it (or not get paid or not publish papers), but you will use a different (suboptimal) technique.

For example, the Git port to Java is an unholy mess of non-idiomatic Java code, because the porters felt the abstraction with the best fidelity of representation would be slower due to incidental run-time overhead.

In the case of type systems, if the implementation does not allow composition where it seems like it should, then you have to resort to an encoding instead. This encoding likely leaks implementation details relative to what the type system is designed to abstract away. The encoding may also not jive well with the optimizing compiler as compared with a straight-forward direct specification of the problem with types.

If you always had to implement something in the most non-pragmatic way possible, I hope you would find a better tool than "void pointers in C".

Further, I see Gilad's idea as potentially complementary to the social process of certifying programs are proved correct. Nobody has made any comments that rule out pursuing what they like alongside what Gilad likes. What I see is a lot of "You are stealing my lollipop, give it back" feedback. Gilad is not the candy man; he is a designer exploring an area of the design space nobody else is. What he is exploring might converge later on with radically different ideas.

Can you give me a link to an online discussion of Git? I'd love to see a real example where these S-modules would be helpful and if the port of Git to Java is one... that's a real example. That would be really useful.

if the implementation does not allow composition where it seems like it should, then you have to resort to an encoding instead

Agreed, casting being a quick encoding. And that's a good thing. It makes the whole "ram it through" process quite explicit. If you want f(g(x)) where g(x) is the wrong type you need to be taking responsibility for f. It is whitebox not blackbox, you need to know a lot about f. As I see it a need to cast like this is:
a) specific to the data types involved
b) specific to the uses (functions) involved
c) fully generic in which case the object structure should support it generically.

Look at the discussion naasking and I are having about absolute value and complex numbers. Two reasonable people can't even agree on what < should do, in a very well understood situation.

Of course the encoding leaks implementation details, unless you are in situation (c) you need to know a lot about both functions. If you are going to use code in a way it wasn't intended to be used, you need to know implementation.

Computers programs are loaded with bugs when the inputs are well understood.

I hope you would find a better tool than "void pointers in C".

Why? At least if I'm using void pointers we aren't kidding ourselves about what's happening behind the scenes. I'll use Pierce's definition, a tractable syntactic framework for classifying phrases according to the kinds of values they compute. If I want to use a module whose designer has limited it certain types of input and I want to ram another type of input in because I think it will work, then I'm completely walking away from the abstract into the highly specific. Essentially for that call I really don't want a type system, I'm doing a manual over ride of the safety mechanism, a void pointer essentially.

This is not like the dynamic case where you have modules designed for runtime type checking. These are modules designed for one type of data being forced fed another. I'd love to see the Git example if this is a real example of where Gilad's theory would actual work on a real problem.

Notes on making JGit (Java Git) fast. Also, this isn't meant as an example of how to apply Gilad's ideas, but rather the more general idea from Burstall and Goguen that a specification should be separate from its optimization, since that too affects a programmer's decision to use composition where possible.

As for void pointers in C, I think I misstated my thoughts. I was relating the experience that programmers will ultimately seek out better tools when the majority of their problems are not easily solved by what they know. Programmers that don't seek out better tools usually know very little, and have thought very little about how best to solve their problems, and so they tend to possess very weak understanding of even the problem domain requirements. ;-)

However, those intersection type systems haven't found much practical use yet, because they can be less natural, more complicated, and there are theoretical reasons they may be impractical.

Can you be more precise here?

For example, provide an example of how they can be (a) less natural, (b) more complicated, (c) theoretical reasons for impracticality.

I first heard of principal typings from the comments in Gilad's blog post, and read about them thereafter. I understand that type systems with principal typings have an important property that all type inference is compositional. Indeed, Gilad's viewpoint is rooted in his belief that composition is the most important criteria in language design (PLATEAU 2010 keynote). All his other arguments aside, composition is what every last one of Gilad's arguments boil down to.

Doing transformations on types, such as simply typed lambda calculus to Hindley-Milner, etc. or even using intersection types is a completely secondary concern to Gilad. His idea is that you use those static analysis concepts to aid in understanding, rather than defining the understanding. This allows later binding of static analysis with program text, so that it might be possible to systematically build up meaning using plug-ins like typing algorithms and the largely orthogonal concern of good type error messages for a given typing algorithm.

But, as an aside, I reject to associating I-Modular with any type system. By its very idea it needs no type system, just source, to work. It's about encapsulation.

There are actually concepts in control theory like this, where you actually don't have to care (mostly) what environmental constraints are - your only concern is if you can get acceptable performance with your practical model as compared with your idealized model. Control theorists call this concern "robust performance" in the face of uncertainty (or, constancy of amplification). But robust performance is extremely hard to achieve and there are limits on stability and performance. The naive approach is to say "two systems are close if their open loop responses are close". But if our goal is simply to close a feedback loop, then we may get very misleading results since the open loop responses for large numbers of responses might be very similar, but not an accurate gauge of how similar two models are. (A famous metric used to aid this problem is the Vinnicombe metric.) And then there are also follow-up questions, When can we prove the system is robust in the face of process variations? For example, let's say we try to implement our idealized model but there is a chance we might implement it with "bugs" that contribute small inaccuracies (or hardware "errors" that contribute those inaccuracies, such as unreliable sensors); is overall performance still going to be robust?

Anyway, sorry for the long-winded reply, but I think these are the sorts of problems we might want to try tackling. It's really just a brain dump. Gilad makes me think hard about the consequences of my actions, perhaps too hard.

For example, provide an example of how they can be (a) less natural, (b) more complicated, (c) theoretical reasons for impracticality.

Disclaimer: I'm not an expert on intersection types, so someone knowing better will probably correct me here.

The type inferred for `id` in `let id = fun x -> x in (id 3, id true)` is `∀α.α→α` in the HM type system, and `(int→int)∧(bool→bool)` with only intersection types. You can already see the difference in modularity in that you can type it only from the `(id 3, id true)` part, without having typed `id = fun x -> x` beforehand (which you need in HM). I would however consider this type slightly less natural (a), as `∀α.α→α` seems a more expressive type to describe the identity function.

For complications (b) with intersection type system, see the abstract of J. B. Well's Expansion: the crucial mechanism for type inference with intersection types: A survey and explanation. :

The operation of expansion on typings was introduced at the end of the 1970s by Coppo, Dezani, and Venneri for reasoning about the possible typings of a term when using intersection types. Until recently, it has remained somewhat mysterious and unfamiliar, even though it is essential for carrying out compositional type inference. [..] Recently, we have improved on this by introducing expansion variables (E-variables), which make the calculation straightforward and understandable.

Finally, regarding theoretical complications (c), there are various results â€" That I don't know well, only from hearsay â€" that type-checking in un-limited intersection types systems is actually equivalent to strongly normalizing the checked term. This makes such type systems very expressive but also undecidable and potentially unpratical even on well-behaved term, because very slow. It's unclear such type system even qualify as "static" verification systems; but maybe this restriction can be lifted somehow.