Lambda the Ultimate

Give me a Scheme-to-C compiler that (a) is well debugged (b) supports macros (c) comes/integrates with tools e.g. gdb, and let me do DSLs in that. It would cut through several of the problems/concerns they raise at the start of the paper, for me anyway.

My Google-fu has failed me.

I'm working on implementing a somewhat similar approach for the C backend of my Rhope compiler. Essentially I compile the whole program down to a single C function containing a big switch statement. Each function gets a label and a case statement. After each call within the individual function bodies, there is an additional case statement. Calls which can be resolved statically are done with a goto. Calls which are resolved at runtime are handled by sticking the ID of the function (the number that corresponds with its initial case statement) into a certain variable and doing a jump to a label that precedes the switch statement. Returns are handled in a similar manner. Before the call is made, the number that corresponds to the case statement following the call is pushed onto a stack. When it's time to return, that number is pulled off the stack and then used in the same manner as with calls that are resolved at runtime.

Using computed gotos for returns/late-binding would probably be more efficient if you don't mind limiting yourself to C compilers that support them, but I haven't done any testing to see how big of an improvement it makes.

... I haven't done any testing to see how big of an improvement it makes.

But Anton Ertl has... In general, I highly recommend that page if you're interested in a comparison of relatively portable interpreter/VM techniques.

I love Ertl's idea of inline threading, but it's rarely portable from even one gcc version to another. Last I spoke to him, he was working on making gcc more friendly to it.

A single C function as the whole program is a burden for the C compiler having to optimize it.

In practical terms, some versions of gcc with -O2 may show a quadratic (w.r.t. to the C function's size) behavior: you'll need a lot of RAM (4Gb is not enough) and a lot of CPU time to compile a big single 50KLOC function with -O2 optimization

This sounds like the C code produced by the Gambit-C scheme compiler. It avoids the huge function problem by splitting the compiled code into multiple host functions (unless you ask it not to). Gambit will happily consume 4Gb of RAM while compiling with optimizations and the --single-host switch.

Gambit performs well. Here is a simplifed version of the compiler presented by Marc Feely.

Yes, I read that about Gambit. I'm interested to read more, but your link is broken. :-)

I assume this is the desired page :- The 90 Minute Scheme to C compiler.

Unfortunately Michael this will not work due to the inherent inability of most C compilers to optimise large functions. Neither gcc or clang has the faintest hope.

I have adopted Fergus Henderson's solution, used in Mercury, in my Felix compiler, with modifications. Basically you have no choice but to make lots of smaller functions. We then use a trick involving assembler labels to make the target visible globally to calculate a machine address to jump to. The jump to that address is effected by a computed goto at the top of the target function.

In Felix, this is all done with macros such that if assembler labels aren't available, a C switch can be used instead at a possible performance cost. Gcc supports it as far as I know. Clang is broken.

I generate C++ not C. Jumps require flat code, that is, no variables may be on the machine stack under the jump. In C++ non-static member variables are used instead.

Note: do not even think in your wildest dreams of turning optimisation off, gcc/clang unoptimised C/C++ is much slower than optimised code, maybe even 10 times slower.

I cannot speak of other compilers, eg Intel.

Simple answer: portability. All of the features you mention are doable within C, and are not more difficult than in ASM, though the resulting program will definitely be slower. LLVM was a contender at one point, and may still be, but LLVM still isn't ported to enough architectures to satisfy the types of development I'd like to explore.

Compiling to C can be very useful in an environment dominated by C. Currently I'm working on a game written in Python, which is too slow for the critical numeric and graphics routines, so we add a few type declarations and compile to C with Cython (successor to Pyrex). We also interface directly with C libraries instead of using SWIG or ctypes FFI, thus avoiding a whole layer of dependencies.

Messy? You bet. Cython hides a ton of complexity. But it allows us to intermix static and dynamic code quite freely, effectively in the same language. And we stopped searching for "the perfect language"; this is good enough for now.

I agree, though: direct compilation is ideal -- and easy. It would be practical if it was used throughout the system/libraries instead of C and everybody used it. Question is, would it be held together by Lisp, Factor, etc, or some language-independent protocol, or what? There's a reason why TUNES is vaporware after 15 years :-) I suppose LLVM is the next best thing now that it's integrated with GCC and seeing widespread use.

I compile from source code to lambda expressions to combinators to thunks which are trampolined. Not a lot of magic to it, each combinator is a function, and no need for tail call optimization. I don't go for optimal speed, so everything but graph rewriting, like handling integers, is handled through ffi.

If you target gcc, you can just compile your tail calls to ... TaDa! ... tail calls, the compiler will do the elimination for you. Heck, it will even automatically transform a naive recursive faculty function into a proper tail recursive form (i.e. loop with an accumulator), a feat most current functional language compilers fail at, see slide 40 of Felix von Leitners recent talk on compiler optimization.

As far as I can tell, GCC just can do tail recursion, and even that only under certain restrictions.

For the compilation of functional languages you need something much more general. In particular, you need to be able to do tail calls not just to other functions in scope (e.g. for mutual recursion), but even to first-class functions. In C terms, you want to tail-call through arbitrary function pointers where you don't know the callee statically.

Under an old gcc version (3.4.4 that came with cygwin), using -O3 -S, I compile the following:

int bar(int n, int *acc, void (*f)())
{
    if(n == 0) return *acc;
    (*acc) ++;
    int (*rec)(int,int *,void (*)()) = (int (*)(int,int *,void (*)())) f;
    return rec(n - 1, acc, f);
}

It outputs the following:

_bar:
	pushl	%ebp
	movl	%esp, %ebp
	movl	8(%ebp), %edx
	movl	12(%ebp), %eax
	movl	16(%ebp), %ecx
	testl	%edx, %edx
	jne	L5
	popl	%ebp
	movl	(%eax), %eax
	ret
	.p2align 4,,7
L5:
	incl	(%eax)
	leal	-1(%edx), %eax
	movl	%eax, 8(%ebp)
	popl	%ebp
	jmp	*%ecx

Can you give an example of a case it doesn't optimize?

Mh, interesting. I was under the impression that this does not work.

But still, what if you are calling a function that happens to have a different argument list than the caller? And to make it more interesting, one that doesn't fit in registers? Or where the caller's one doesn't?

I haven't checked the other cases you mention, but one thing that I'd guess would be a problem (and have now confirmed as a problem) is this:

void bar(int *);

int foo(int n)
{
    int x;
    bar(&x); // Does bar retain a pointer?  Don't know
    return tc(n); // Can't tail call
}

Edit: Actually, this case can be re-written as:

int foo(int n)
{
    {
        int x;
        bar(&x);
    }
    return tc(n);
}

And this can be generalized to support any tail calls. The only real problem I think is that, since gcc considers this an optimization, it may decide it's more optimal in some cases to grow the stack instead of shuffling data around to allow the tail call. I may play with this more later to see when it makes that decision. It'd be nice if you could just instruct gcc to make a tail call.

It'd be nice if you could just instruct gcc to make a tail call.

I'm seeing a lot of this in the recent discussions about tail calls. Not a bad idea I don't think, for an optional "tail" annotation on calls (like how LLVM and CIL have in their IR). This way the user can be assured a call reduces to a tail call if the compiler does not spit out an error.

Gcc will not attempt TCO for calls needing more argument stack space than the caller, because the caller's stack frame (local slots) are built on top of its arguments, and making room for more arguments would force the caller to rearrange its locals first - and this is typically not an optimisation for C code.

It's less of a restriction for modern platforms where most parameters are passed in registers. (Some ABIs unwisely mandate argument stack space allocation for register arguments.)

As other people have said, it would be nice to have an annotation to enforce TCO.

This is not a trivial change. It looks like it would be pretty trivial to ignore potential aliasing issues, but there are also fifty things that can block tail call optimization from being attempted or cause it to fail if attempted. And most of them look like they'd break the code if removed, rather than just potentially slowing things down.

A much smaller step (and a trivial change) would be to add an annotation of tail calls that makes the compiler produce an error (or warning) if a sibcall is not possible. That would at least guard against surprises when C is used as a back-end.

I compiler to C++, but there are two alternatives given by slava and both are very bad. Compiling to machine code involves implementing a huge amount of stuff and that's just for a single processor, try a single processor with multiple models or multiple processors .. no thanks!

LLVM is a woeful alternative. The instruction set was designed for C and C++ and isn't otherwise useful. It's a pity really, but no modern language should be without coroutines, and LLVM is set up for C functions and has a special call that knows about exceptions in C++ but there is no branch and link instruction.

As does compiling to javascript or Java bytecode. Java bytecode in particular is quite a nice target of you language needs GC.

I am a fan of "portable" languages like Haxe, Shen, and others. But I strongly dislike it when there's no source-level debugging of the original language. Instead I have to look at the "assembly" they produce that is C (or Lisp in the case of Qi/Shen) but twisted to support what they are doing. There's large standard libraries shoved in. There's little or no connection back to the original source. The produced code is potentially optimized which means inscrutable to regular humans. Etc. The litany of valid usbility complaints goes on.

It is ironic that Dr. Tarver posted his story about how Lisp programmers never finish anything properly, and then goes and makes Qi/Shen that doesn't give me source-line debugging of Qi/Shen code.

There are apparently 2 kinds of people in the world: Those who know debugging is important and debugging tools are important; and those who do not.

The article linked from Yossi Kreinin extensively describes how to achieve source-level debugging of Forth while using C as an intermediate language. So your response baffles me a little. What is it that you didn't like?

He might have done it, but most other people have utterly failed to. See Haxe (C/++), Shen (Lisp, Java, Ruby, and others), ATS (C and others), most anything that compiles to javascript (Haxe, etc.), etc. So I feel like this is something people Just Don't Get?

p.s. also? Error messages!

I think almost everyone gets that good source level debugging is better. But providing it has more than one kind of cost. It's a fit-and-finish task, involving a lot of effort, of a sort that does not increase status nearly as much as undertaking hard core compiler-wonk tasks. So it's a terrible opportunity cost, just like writing docs and tests, in a world that's very competitive when it comes to my-chops-are-bigger-than-your-chops kind of wrangling.

Excellent debugging is a great product feature, but not a great source of prestige for individuals. A large majority of folks are driven by how they look as a result of something done, or something said. Generally, anything that looks like cleaning windows or dishes will cause folks to step away, unless there's a really good salary in it, and a person has given up or never cared how they look.

Maybe the C tool-chain kind of sucks for that sort of thing, requiring hideous high density compiler directives, etc. Tool ugliness is really irritating. Certain parts of the ecosystem are really primitive. Getting your hands dirty has to be quite aggravating.

Is there a system that shows it can be better already? K? Oberon? Lisp? I dunno. If it sucks to do it, what if we could have it suck less by having the fundamental approach be more of a right abstraction?

I've worked on the 'stupid/boring stuff' many a time on and off in my life, so I know what you mean. Installers is one of my favourite things to complain about: They all suck whenever I've used them; they are very important to how the end user perceives and gets to use the product if at all; And yet implementing them is an utter nightmare, even on a single "system" type since e.g. versions of {windows,linux,etc.} have different guidelines/requirements/expectations.

My remarks may all be obvious, but I think that's a good question, and a big list of good questions is a fine thing to help seek nice designs. Answers to questions can be backward or forward looking, depending on whether you live with existing tools, or think about replacing them. Both at once also works, but causes confusion when English lacks good terms for multiple concurrent tactics. (What if I live with the old thing in production, but use a new simulation in development? How do I know debugging one is evidence about the other?)

what if we could have it suck less by having the fundamental approach be more of a right abstraction?

Something should be more abstract about source mappings. For example, there could be more than one mapping, not just source S to executable X. Any longer chain A to B to C to S to X could in principle be supported. Then a debugger might show you the layer you want to see when stepping through code. It's very functional, and if you avoid erasure of what was known in each layer, you only need a tool smart enough, that's willing to show you a suitable view you request.

Perhaps suckage is maximized when debugging cores with gdb when source was C, and the compiler only learns about source mappings from compiler directives. To debug source code that's compiled to C, every line of C might need a compiler directive before it (major ick with horrible efficiency).

One problem with abstraction is that there are at least two competing attractors in a chaotic system, pulling toward no abstraction here and too much abstraction there. Jim might like ten times as much abstraction, but Joe wants ten thousand times as much abstraction, both with commensurate performance overheads. Jim thinks Joe is crazy, and vice versa. Watching them argue is like watching two court jesters beat each other with animal bladders: funny but not much happens. (Typical of tech conversations.)

You could probably write an emacs extension that knew how to show a different source code layer than the most immediate layer of C that was compiled at the end, if the layer mappings are around somewhere.

The incumbent has an advantage of being unique. Challengers have a disadvantage of being numerous, thus dividing votes after balkanization of target agendas in forward looking plans. Too many choices can be paralyzing.

I guess the actual division line is experience of working with large code bases of low-quality code, with understanding that it is not a bad luck but just programmers driven to the edge of their competency. In commertial settings every programmer is usually loaded high enough to start writing the code for which it is barely competent.

Debugger is the must for such programs.

Small PL are usually designed by people that solve limited scope tasks and which have a good understanding of what happens. They could actually fit the entire program into the head and work out of implicit assumption that everyone can do the same with their program.

The same is emphasis on data transformation patterns and attempt to represent everything as data transformation task. Surely data-transformation paradigm is ideal for compiler, but webapp manages and provides access to shared persistent state via web UI, so abstractions should naturally and safely relfect that instead of trying to hide it under layers of "pure-functional" frameworks.

Industry is characterized by limited knowledge of the domain, lack of time, and many other charcteristics that academic settings does not have. There is just no time to spend 8 hours to figure out minimal set of type annotations that would give a correct solution to type equation. One would gladly write two times more source code lines for the code that predictably compile to the code that is very tricky to compile but very concise. This is a reason that haskell did not get a serios foothold in industry. Scala on other hand is a better compromise between predictability and consiseness, but it still is not predictable enough to be a serious player.

In short, commertial apps stress congnitive abilities of human to degree that every additional cognitive load from PL and tools has to be well justified. Note, unless it is google or some company like it, the project is usually understuffed or underqualified or both due to continuous cost cutting (bigger companies usually tend to have underqualified IT because of outsourcing). Additional keystrokes is not too heavy cost for predictabiliy and lessening congnitive load. Keystrokes have to be spent once, type inferrence brain-time has to be spent by everyone reading the code. If compiler has a hard time to infer types for the code, the reader might have even harder time in case when code was written by other person. So far, for many developers learning touch-typing looks like a better investment of the time than learning pecularties of haskell. It really helps to get work done faster with any programming language :)

I am interested to hear more specifically why you find Haskell unpredictable, and how Scala improves on it in this respect.

My own project is to use modern typesystems to build a language which is a better engineering tool. One of my main angles has been to remove unnecessary cognitive load -- after all, even if your competence allows you to encompass difficult constructs, your brainpower is probably best spent elsewhere.

I should mention that I am modestly familiar with Haskell, and have looked over Scala but not really programmed in it. With that caveat, I will say that I find Scala noisy compared to Haskell, and my initial reaction classified Scala's type-management boilerplate as "unnecessary cognitive load".

I had to do several iterations just to compile 10-liners in haskell, since inter-dependencies are quite implict and haskell often solves type equations in a bit surprising way. I had to decrypt errors. There are guides like this one, but their existence means that there is a cognitive problem. The haskell errors went beyound problems with C++ templates in hardness. There are even attempts of using Bayesian models to reports errors better.

Also API naming was quite surprising, function "fromInteger" is still being remembered by me as an example of the bad API design (IMHO functions should be named by their intended result rather than by argument type as in Haskell).

Haskell was quite surprising in other places as well, for example what would be a field in other language local to the data structure is a global function. Thus I could not have string id for one type and numeric id for other type within the same module whithout using type classes in a perverse way. I need to be aware of the entire module namespace when defining internals of data types.

Other thing that adds load are monads, it maybe not so complex concept in the core, but it took some time to understand it, and I still do not feel certain that I understood them right, and I'm not sure about my ability to explain them to others. As a hint to the problem one could remember that darcs is written by experienced haskell programmers and they were unable to get performance right. That indicates that performance is not obvious for haskell, otherwise those smart people would have fixed performance problems long time ago. For Java, Scala, and C it is easier to diagnoze performance problems since execution model is more obvious.

Scala has good and bad sides from cognitive point of view. There is a certain overuse of operators on one hand, so code becomes barely readable at some places. On other hand its type equation language is quite simple in most cases, and it is relatively easy to understand error messages. The extra verbosity mgiht be considered as load, but on other hand it provides additional anchors for understanding code in Scala. For Scala, I find that there is much less things to consider than in Haskell when writing the same functionality, because there are good ways to limit scope of consideration when needed.

Note, the two different cognitive load types should be considered: quantity and quality. Too verbose code is a problem, but need to run a compiler in the head is a problem too. For 10-liners one should be able to get a good idea whether it would compile without global program analysis.

Seriously, it's like a one-man hit parade of "why Haskell is not entirely suitable for large-scale engineering projects"!

My main concern is that the unification-based Hindley-Milner style type inference is the primary thing I want to steal from Haskell. So, if there is an inherent difficulty in presenting engineers with a language based on it, I've got a real problem... maybe appropriate attention to detail will help make type errors less surprising? Anyway, thanks for the link to the Bayesian paper.

For type inferrence, I would have restricted its scope to manageable blocks. From engineering point of view, all exported/public members of module/class better carry the explict type information, so the next porgrammer does not spend the time to infer types for them basing on their implementation.

Basically for single funciton it should be sufficient to infer types of all symbols just by knowning intended signature of function and signatures of functions involved into it. The lambdas, local functions might have types optional (but there should be possiblity to explicitly annotate them in complex cases), but for exported members one should not study implementation to understand contract.

I agree with this. I would make module signatures mandatory, but in my opinion module signatures are data-types. Therefore datatypes contain types (obviously) and all functions can have their types inferred.

The question is who would infer the types for functions. The developer would basically need to dive into the implementation to get the contract, otherwise you would have no idea.

Note, that the tool support is not enough here, since code could just fail to compile (for example, signature of other module changed in backward incompatible way or bad merge from VCS).

Basically, the question is contract vs. implementation. The type signature for the functions is a partial contract. If it is not specified, one have to guess it from source. Every such guess is a huge cognitivie effort. In some sense it is reverse engineering for developer that reads the source. In 10 developers team, the write effort is done once, the read effort is done 10 times (and repeated after some time, because memory has limited capacity). I actually sometimes have problem with understanding my code from 5 years ago unless it is well documented.

For large, distributed teams, in different timezones (and with continuous fires and hires) the problem is much more complex as the person who written the function could be already working for other company.

Contracts in real world are also done to save cogntivie efforts. One has to understand only interactions between companies, skipping uninsteresting details how other party would achieve the result.

Ill give an example as I don't see the relevance of your question, I think I did not explain what I mean well enough.

data SetADT x = SetADT {
    type Set x : *
    insert : Set x -> x -> Bool
    find : Set x -> x -> Bool
}

helper1 x = ...
helper2 y = ...

my_set = SetADT {
    type Set x = List x
    insert x = ... helper1 x ... 
    find x = ... helper2 x ...
}

Note the module signature is a datatype (a record type with an associated type - implemented using type-families). In the module implementation the functions don't need type signatures as they are provided in the signature with is the contract. Local functions like helper1 and helper2 can have fully inferred types as they are not exported.

Let's consider the my_set case first. This is an object constructor where insert and find are in fact named parameters. Type annotations are not required here, but might be helpful if object is too big, so the reader does not have to navigate to SetADT definition. Source of information is obvious, you have spend few keystrokes to get the information in a routine way. If there are too much such parameters, things could get really ugly.

The functions helper1 and helper2 are more interesting case. Consider the case when it is 1 hour before release and there is runtime error detected on the specific server in UAT evironment in helper1 and you have only ssh+vi on hand with access to remote server.

If helper1 is not written by you (and this is a normal case in the such environment), you have to find all usages of it and solve type equation in the head to just guess type signature not speaking of actual contract. If you are short on the time (and in comertial environment, you would be almost always short on the time), every second spent on understanding something is the second you are not spending on solving task at hand at the worst possible moment. I would rather spend few keystrokes in advance rather that spend unpredictable hours figuring out things later (this is a basic idea of insurance).

You can ask the compiler what the type is. If what you were saying was true then people would not be able to debug untyped and dynamically typed code so easily. People manage to program Python and JavaScript pretty well.

The idea of type inference is to make a statically typed language feel like a dynamically typed language to program. You write untyped code like Python, JavaScript, Lisp etc, but get the strong type guarantees of languages like C/C++, Ada etc.

I agree with you that types at module boundaries should be recorded so that interfaces are visible and remain consistent. I am not sure I want to write a type signature for every type. In modern C++ you use "auto" a lot because generic type can get pretty long.

The compiler tells about current situation rather than about intention, and it is really hard to ask most compilers about it.

Developers (that I know) are not very fond of creating big systems in JavaScript or Python in enterprise context. For browser programming, most developers (that I personally know) do not like JavaScript, and browser-side part of the application usually is kept as small part of the application as possible, and different kinds of DSLs are often used to minimize plain JavaScript code.

For microservice-style applications dynamic languages might be ok, but bigger context - I have not seen them and doubt that they would stick in enterprise. Open source is a bit different thing because there is lesser deadline presure and there is self-selection bias for technologies (people who join the project like techonology stack of that project or find it acceptable). For Java, I have worked with systems that are more than 10 years old, have many megabytes of code, hunderds of developers, and still evolve.

And in my personal experience, dynamic languages ARE much harder to debug when there is more than 1mb of the code. It is much easier to get Java or Scala code right than JavaScript code right (even for single browser). Groovy is not friendliest language in that respect too, I spend more time diagnosting runtime problems in Groovy (when closures are used) then for plain Java. Good quality Groovy code requires more unit tests than Java code and design should be much more testable (things became easier with Groovy 2.2, but still...).

I have not touched C++ for more than 7 years already (except for tiny programs like calculating arcsin(4)), so I would not argue about it. From past experience, C++ was not most pleasant language to program in, and I had more problems with memory management issues (who is responsible for what) than with writing type signatures. I generally have no problem with type inferrence inside the function for the values and argument types of the local function. External interfaces could affect types of the symbols in the local context. The problem for me is when local usage affects type of the function in the parent namespace like it was in the example above. When there are more than one page of the code, reading the code becomes hard.

Lack of type annotations might look nice for the code that processes list in the obvious way, but for something less obvious like claim processing I wold prefer explict type annotations. Still even for the list processing code, you have either to write annotations once or to infer types every time when you read the code (the type inferrence result could be cached on the neural network, but even caching is not free). Global scope for type inferrence increases the required effort. With explicit type signatures you might stop earlier and smaller scope has to be considered. Brain-time is not free. Actually, it is more expensive than CPU-time for a long time already.

The type constructors in the value level code tell you what you need to know about types. For example:

data Tree x = Branch (Tree x) (Tree x) | Leaf x

sum (Leaf x) = x
sum (Branch x y) = sum x + sum y

data Nat = Z | S Nat

add Z y = y
add (S x) y = S (add x y)

Its easy to see what sum and add are doing because of the type deconstruction.

It is easy to see in this small situation. But does it scale? Note, to understand that (Leaf x) is actually Tree one has to remember definition of Tree. It is good if tree is in the standard library, or there are few types defined. However, it is not always so.

For example, if we consider insurance claim data model, in our model, we have 62 entities and 1491 simple value attributes (attributes for some embedded data structures are counted serveral times here), and this is the smallest sub-domain of the application. And this is only entity model, there is model-level data objects, view-level and so on. Some of objects from different levels have similar names and many of them have similar properties. Normal amount of imports is 20-60 (it includes classes from other subsystems as well). From my experience, this is normal situation for enterprise application. In this particualr project, there are even some savings in the code due to use DSLs and some resue from other projects. I other projects that I have worked for, the situation with domain model is usually somewhat worse. Remembering all types is almost impossible.

Missing type annotations is fine if you could fit the entire project in the head. But any evolving enterprise project will eventually grow beyound your mental capactiy. Nice architecture and good patterns could delay this moment, but it would happen anyway. Type annotations make code analysis much more local and thus allow the project to grow further.

When you have many properties on an object in a library, you need to see the object type from the headers, there is no way you can memorise all the properties and you are not going to copy the object definitions into every piece of code that uses it.

If you have typed module interfaces it allows the project to grow just as much. You don't need types that are only used locally in the same module.

I think you are not considering generic types and polymorphism. For example:

f = x + y

We know that x and y can be any addable type, the type would be something like:

f :: Numeric a => a -> a -> a

It doesn't really tell you anything you can't easily tell from the function definition.

I have also seen plenty of Python enterprise software that is better than Java or C/C++ code. So I don't think the reality is as black and white as your viewpoint. Type inference can give you the best of dynamic and static type systems, so you have compile time static type checking, with clear consice uncluttered code. An example from Java / C++ languages:

Widget x = new Widget();

The type on the variable is totally redundant so modern C++ allows:

auto x = new Widget();

In general if you don't provide a breakdown by constructor cases you intend the function to be generic over all types. For example:

pair x y = (x, y)

x and y can be any type, why do you need a type signature?

IMO, Any is not a legitimate type.

The structure Pair should be as follows:

Structure Pair◅aType▻[_:aType, _:aType]

You have a problem with universal quantification?

pair :: forall a b . a -> b -> (a, b)

I don't have a problem with this at all. It is implicit that a and b range over types, so it is not unconstrained. 'a' and 'b' cannot be kinds for example.

I also don't understand your formulation for pair, as each element should be able to have a different type, so wouldn't you need two type parameters:

Structure Pair◅aType, bType▻[x:aType, y:bType]

Of course the type

Structure Pair◅aType▻[_:aType, _:aType]

is different from the following type:

Structure Pair◅aType, anotherType▻[_:aType, _:anotherType]

However, I don't know what the following is supposed to be:

pair :: forAll a b . a -> b -> (a, b)

because the above does not seem to be a statement of the logical quantification calculus.

Furthermore, logical variables that are universally quantified should always be typed. For example,
∀[σ:Type, x:σ, P:Boolean^σ]→ P[x]⇔(P[x]=True)

Note that σ:Type, P:Boolean^σ means that there are no fixed points for propositions.

So you could write:

pair : forall (a : Type) (b : Type) . a -> b -> (a, b)

But as type variables can only be types there seems little point in putting it in.

So you seem to be saying something like the following:

∀[σ:Type,τ:Type]→ Pair◅σ,τ▻:Pair◅σ,τ▻[σ,τ]

Well probably more like:

forall (x : a) (y : b) . (x, y) : (a, b)

But this is no longer a type signature, as it includes both the value level and the type level. Returning to the original definition:

f : forall a b . a -> b -> (a, b)
f x y = (x, y)

The types and values are split into two separate declarations. The '->' arrow infix type constructor is introduced for application, and the quantifier is dropped from the value level the dot replaced by '='. The arrows correspond to the argument order of the second definition, such that the types in positions "f : ... 1 -> 2 -> 3 -> 4" correspond to the values "f 1 2 3 = 4".

Yes, it is certainly the case that

∀[x:σ,y:τ]→ Pair◅σ,τ▻[x,y]:Pair◅σ,τ▻

However, Pair is not reducible to untyped lists.

Note: since types are Actors, in that respect, there is no fundamental difference between the type Type and the type Integer.

PS. IMO, always Currying detracts from readability :-(

I think you are proposing something like uncurried dependent types, which is not unreasonable. I am not yet convinced about combining types and values into the same language. There are some good reasons for keeping type-level and value-level separate.

Parametrized types (illustrated above) are a good idea.

It is not clear to me why it might not be suitable for Types to be Actors.

Types have equality, whereas functions do not. We can meaningfully ask do these two functions have the same type (type-equality and polymorphism), but we cannot ask if these two programs are equal.

Types should be equal by the criteria of identity of their type names because the use of types in security, e.g., encrypting messages.

Lots of Actors don't have meaningful "equality" apart from identity; e.g. accounts. That two accounts have the same type is more or less irrelevant for the purpose of account "equality."

It seems you have an arbitrary definition of equality. What is the justification for only having 'name' equality for functions (actors).

- Types should be compared structurally with unification.

- Identical programs should produce identical output, but its obvious this is impossible to define simply by considering all the different sorting algorithms that produce the same output, defining a useful equality is not possible.

For me these are two different equational systems that should not be mixed together. How would you justify the consistency and completeness of a system combining objects with such different behaviour under equality?

For security reasons, types should not be considered the same by being compared structurally with unification.

Instead types should be named and considered the same only if they came from the same place.

Comparing types structurally with unification is prone to error and can produce very obscure error messages.

I agree, but that isn't a very popular position in the FP community :)

Surely both structural and nominal have their uses.

By the way, you can easily encode nominal in terms of structural: Just add a tag field to the structure.

But there's clearly uses for additional notions of type equality. GHC, for example, understands a notion of runtime-representation equality for static coercions. Presumably there are other useful notions to be discovered.

They have their uses, sure, but structural typing is overused in the literature and of very limited use in real life. The reason it is so popular in academia is because it has a nice name-free theoretic basis. Everything they hack in afterwards to regain the power of nominal types (e.g. row polymorphism, opaque, etc..), just seem to reinforce their fragility!

Saying we can encode nominal types as structural types is like saying we can encode C programs on a Turing Machine. There is a lot more that goes into a nominal type system than names...as I can tell you right this very moment!

Hacking back limited structural typing using subtyping and genetics seems as much of a hack as the things mentioned above.

I am not sure how row polymorphism is something provided by nominal types, but the ability to give a type for database columns and SQL statements is very useful. How would you do such things with nominal typing?

I don't really see the point in opaque types, its a bad approach to security IMHO, and breaks datatype generic programming.

I'm interested in what people see as the advantages of Nominal typing?

You don't really need row polymorphism if you have nominal subtyping. Nominal types are great for the same reason that they are horrible: because you can just declare arbitrary relationships on names; these are just taken as ground truths and do not need to be shown structurally. Its like arbitrary word usage in English.

Linq required changes to the C# type system, so I don't see evidence than nominal typing provides row polymorphism by default.

Linq did not require changes to the C# type system, it required syntactic sugar to be sure, but nothing in the type system actually changed. Well, they did need to add simple local variable type inference since anonymous types can't be written down, but that was useful in many other ways (as well as being really simple).

I don't know the details, maybe I was thinking of the addition of local inference.

In any case generics are structural types, so I think the argument reduces to:

Nominal types with structural types hacked on top via genetics.

vs

Structural types with opaque types. To me this seems the more consistent implementation, and less hacky.

Generics are structural but can have nominal components. It really isn't that hacky: many programmers are happy with C# and find its type system simpler than similarly expressive ML/Haskell type systems. Let's just not mention scala :).

There are other ways of doing generic programming than with parametric polymorphism, some of them are very nominal (e.g. Virtual classes), but haven't caught in for some reason. It would be interesting to contemplate why but I'm already too off topic as it is.

If "opaque" is what I think (namely the ability to enforce type abstraction by hiding the definition of a type and allowing to rely only on its name for equality; that indeed looks like a way to decompose nominality in more atomic concepts), then I vehemently disagree. I think it is one of the most important developments in programming-languages type theory that is related to deep programming concerns.

Abstract types raise many issues in programming language design (for example there are no worked-out designs for type-classes in presence of type abstraction). But they are good issues to have because (1) in absence of abstract types, they already exist but in a less visible form, and they still cause problems and (2) solving these issues helps building modular programs.

What do opaque types give me beyond just using a naturally encapsulated and abstract named type?

Abstraction in a non-named structural world is difficult, which is why we invented (or evolved to use names) in the first place. Og the Caveman found it difficult to reason about his pre-historic world literally and eventually found he could just create arbitrary words to represent things, which led to language, writing, technology, and everything else. Whose to say Og was wrong?

:)

I think we have a case of the same thing by a different name:

data Type = Type Int Float String

Is equivalent to the following generic type:

template <typename A, typename B, typename C> struct Type
    A const a;
    B const b;
    C const c;
    Type(A&& a, B&& b, C&& c)
    : a(a), b(b), c(c) {}
};

template <> struct Type<Int, Float, String> {}

They will behave identically. An opaque version of the same type is equivalent to this:

class Type {
    Int const a;
    Float const b;
    String const c;

public:
    Type(Int a, Float b, String c)
    : a(a), b(b), c(c) {}
};

All type systems need these features, the structural approach is just the neatest way to implement it. Also with structural type systems the result is an algebra rather than an ad-hoc collection of features.

No, opaque types are about subtyping and encapsulation. It's been a while since I read the Moby papers, so my memory is hazy.

I don't know why you don't see the equivalence, but an opaque type serves the same purpose as object encapsulation. Its about having a type where you cannot see what's in it. For example:

data Test = Test {
   data Opaque
   f :: Opaque -> Opaque -> Opaque
private:
   data Opaque = Opaque [Int]
}

Outside of the container you can only see the first definition of Opaque, so you cannot break the abstraction by looking inside it. Inside the container you see the second, private definition and can use the deconstructor to access the contents of the type (the list). Subtyping is a separate thing.

So this example is like the normal behaviour of nominal types, hence why it maps to a class.

Structural typing (product types) are just like the generic templates. For example:

using t = Map<String, Vector<Tuple<Int, String, Float>>>;

If you want to have opaque generic types in a nominal type system, you may well end up with two mechanisms to achieve the same thing, the base nominal mechanism, and opaque structural types for generics.

Just look at C++ type_traits and function_traits, which become necessary to write generic templates, and effectively add back structural typing, where you can ask things like:

template <typename F> struct test {
    using return_type = typename function_traits<F>::return_type;
}

There are function traits for function arguments and return types, there are type_traits for object properties and methods.

As you can see the mechanics of the nominally typed version are more complex to achieve the same result, and the nominal version separates the concerns less well, mixing meta-programming with parametric types, and value level syntax with type visibility.

The definition of a nominal type in an algebraic type system is much simpler than the mechanisms necessary to add function_traits and type_traits into a nominal type system. As the two converge to the same thing, it should be obvious to choose the one that includes most of the requirements in the core system with the least complex extensions. It makes the implementation of the type system much simpler too.

A further thought is that nominal typing does not work at all without encapsulation. For example consider:

data Test

Test is just a type name, it has no structure, but how do we associate it with a value? In a nominal type system there must exist some operation that binds a hidden type to the name. For example:

struct Test {
    Int a;
    String b;
};

We can consider this a specific instance of the generic:

template <typename A, typename B> struct Test {
    A a;
    B b;
};

template <> struct<int, string> Test {}

Or using more pre-defined template stuff:

tuple<int, string>

Yet to have a nominal type we need a way of associating this with a name that hides the contents like this:

struct nominal {
private:
   using test = tuple<int, string>;
}

So we can have structural types (generics) without any encapsulation using tuples (although C++ is forced to use a struct to internally implement 'tuple' this is not necessary with proper structural types), but to have names requires value encapsulation.

I think the relationship between names and encapsulation is interesting, but building generics (which do not require encapsulation) on top of names (which do) seems to be getting the dependencies the wrong way around. Its seems much simpler to start with generics (parametric polymorphism) and add encapsulation/naming.

I think this clearly demonstrates that building names on top of structural types by adding encapsulation is the right way to do it. Adding generics on top of names forces encapsulation into generics in a way that is complicated, unnecessary, and gets the hierarchy of concepts the wrong way around.

Lack of support for generic programming is a big problem with nominal approaches. You need to ve able to do things like define recursion over sum and product types to facilitate datatype genetic programming.

Indeed, but type systems are an algebra, and without structural equality you cannot do things like ask if a function type is a generalised version if another function type.

Nominal type systems need to introduce all sorts of additional complexity to support generics, which is effectively reintroducing structural equality over the top. It's all much simpler if types have a structural equality to start with. In programing simpler code with less special cases is generally better.

You don't want structural equality with nominal types + generics, you rather want subtyping.

The point was structural equality is a better solution than nominal equality + subtyping, as it provides all you need in less rules. It is a more elegant solution.

Plus how do you deal with datatype genetic
programming with nominal types + subtyping.

Subtyping does introduce a kind of limited structural (in)equality, as you can subtype function types over their arguments in order. This was my point above about introducing an extra layer and extra complexity to add back features missing from the nominal types.

Named types + discriminations are the way to go.

Security and recursion are supported using named types.
Discriminations are much more precise than undiscriminated unions (a la C).
Extension of types should be used instead of subtypes because the addresses of other actors cannot be cast.

I agree about discriminated unions, and I prefer parametric types to subtypes.

I don't really see any reasons to favour nominal types? Is this just a personal preference, or is there some justification for this choice?

Named types enable encryption of messages using types.

As I point out above it makes more sense to add opaque types to structural typing, than to add generics over the top of nominal types, due to the implicit 'encapsulation' in nominal types.

Parameterized types can be named. For example,

Structure Pair◅aType, anotherType▻[_:aType, _:anotherType]

In this way, a Pair can be encrypted.

I thought you said that your types were nominal (when we were discussing equality). Are you now saying that is not the case?

Two named types are distinct types even if they have the same structure. For example, the type Pair is not the same type as Doublet below:

Structure Pair◅aType, anotherType▻[_:aType, _:anotherType]

Structure Doublet◅aType, anotherType▻[_:aType, _:anotherType]

If the structure of the type is visible in the type itself, then this is plain structural typing as:

data Pair x y = Pair x y
data Doublet x y = Doublet x y

Standard Haskell data types behave like that. Nominal types hide their contents like:

template 
struct pair {
    x a;
    y b;
};

In the former case two pairs are not the same if x and y are different, and the types of x and y are recoverable in the type system, whereas in the latter case two pairs are the same type even if x and y are different, although there are trap-doors like 'decltype' in C++ that allow recovery of the types of x and y providing you know the property names (some languages may even provide reflective capabilities to enumerate the properties).

Of course, Pair◅aType, anotherType▻ is never the same as Doublet◅aType, anotherType▻.

Also, named types can be recursive. For example,

Discrimination Tree◅aType▻ between Leaf◅aType▻, Fork◅aType▻

Structure Leaf◅aType▻[_:aType]

Structure Fork◅aType▻[_:Tree◅aType▻, _:Tree◅aType▻]

The question is: is pair<a,b> the same as pair<c,d> ?

Default matching in a programming language of necessity uses a strict equality.

Consequently, Pair◅Type1, Type2▻ is the same as Pair◅Type3, Type4▻ if and only if Type1 is the same as Type3 and Type2 is the same as Type4.

As far as I can tell, what you have is standard structural typing. Add to that, that types are values (IE actors) and it would seem to be a dependently typed language. I suspect somewhere you have the equivalent of Pi and Sigma types but its hard to tell with all the nonstandard terminology. Is your treatment of equality intentional? Its not extensional as you don't have function extentionality.

You're using a very different definition for 'plain structural typing' than I've seen elsewhere. As I understand it, Pair and Doublet above are nominal, at least in Haskell where declaring `Pair a b` in one module creates a different type than the same type descriptor `Pair a b` declared in another.

Though, perhaps your meaning is that Pair is now a new constructor of structural types? We can, of course, model structural types in a nominal type system (and vice versa).

cf. Wikipedia: Structural Type System

My understanding is a structural type is where equality is recursive, so with structural types pair<a, b> is a different type from pair<c,d>, whereas with nominal typing (like in C++) they would both just be instances of the "pair" class and hence have the same type.

Pair defined in different modules is different because the type names are prefixed by the module name for differentiation, and you have to import them. I am not sure how formal the definition of Haskell modules is, I have a feeling it is (was) not in the standard.

In Haskell:

data Pair a b = Pair a b
data Doublet a b = Doublet a b

Are obviously different types, so I am not sure what the point is?

There are many equivalence relations so default equality (used in pattern matching) must be strict. Consider, for example, a financial account with a concurrently changing balance, e.g., Account◅Euro▻.

On the other hand, a common equivalence relation among complex numbers is not structural.

Actor Cartesian[myReal:Float, myImaginary:Float]
   implements Complex using
      realPart[ ]→ myReal
      imaginaryPart[ ]→ myImaginary
      equivalent[z] → myReal=z.realPart[ ] and myImaginary=z.imaginaryPart[ ]

Actor Polar[myAngle:Float, myMagnitude:Float]
   implements Complex using
      realPart[ ]→ myMagnitude*Sine.[myAngle]
      imaginaryPart[ ]→ myMagnitude*Cosine.[myAngle]
      equivalent[z] → ..realPart[ ]=z.realPart[ ] and   ..imaginaryPart[ ]=z.imaginaryPart[ ]

Unfortunately, the following Haskell notation is verbose and redundant:

data Pair a b = Pair a b

data Pair a b = Pair a b

Algebraic datatypes are more general than structs since they express discriminated unions as well. I think Haskell is the gold standard for terse syntax here.

Haskell and most MLs somewhat suffer that they started off as simple tools. They get pretty far in being concise but in both languages you can still see the parsing shortcuts of the original tools.

They're fine, but if you start over you can do better.

Unfortunately, Haskell is both verbose and redundant as illustrated by the example below:

data Pair a b = Pair a b

which would be better expressed as follows:

Structure Pair◅aType, anotherType▻[_:aType,_:anotherType]

I can see how your example is less verbose and doesn't repeat 'aType' or 'anotherType'.

David,

Type parameters are different from structural parameters.

The following is also legal:

Structure TripleUp◅aType, anotherType▻[_:aType,_:anotherType, _:aType]

You mean like:

data TripleUp a b = MkTripleUp a b a

Note the Haskell notation also declares a function that constructs a value of the type as in:

MkTripleUp "abc" 123 "def"

which would have a type something like:

TripleUp String Int

For example, the following cannot be expressed in many type systems (e.g. Java):

Interface Expression◅aType▻ with eval[Environment]↦aType

I have no idea what that means? Evaluate some 'program' in a given environment such that it returns a type "aType"? Personally I would not have 'eval' in any language.

Eval should be a message to an expression of a parameterized type with return type the type parameter.

Interface Expression◅aType▻ with eval[Environment]↦aType

Consequently the above specifies that when an eval message with an argument (which is an Environment) is received by Expression◅aType▻, then the return type is aType.

Type names are different from data constructors.

The following is also legal Haskell:

data TripleUp a b = W a b a

The redundancy in `data Pair a b = Pair a b` of writing 'Pair' twice with different semantics, once on the left as a type name and once on the right as a data constructor, is similar to the redundancy of writing type names once on the left as type parameters and once on the right as structural parameters.

strike again

Programming languages to fit every need.

If types were such a fundamentally right concept, you'd think folks would be able to agree on how they should work.

It seems to me they do agree, just some people are using different terminology and ways of writing what is essentially the same thing.

Well. You have type theory, where people write the most elaborate type systems, and where most except for the trivial probably contain math bugs. Unless formally verified, possibly implemented in a language, I don't read it anymore.

And then you have people who write compilers, who patch up some type system with a strong, sometimes weak, resemblance with a type system, see if the algorithm passes some unit tests, and then throw it out to the public.

And then you have people who invent complete type systems of their own.

Perhaps the winner of syntax, but not the winner of semantics. Ideally the syntax Foo Int | Bar String would be an expression that can stand on its own: a structural type in analogy to structural record types {foo : Int, bar : Int}. Making a nominal type out of it would be a separate construct. Haskell combines both of those operations into one.

I would say Haskell datatypes aren't purely structural since there's no way to forge one without using a constructor to stamp it with the appropriate name. But as you point out, parameterized datatypes are structurally typed in their parameters.

I don't think it means anything for a type to be "structurally typed in its parameters", but then I don't understand much from this discussion.

In my book a type constructor is structural if its semantics is given by simply unfolding its definition (in particular the naming does not matter). A type constructor is nominal when it is not an alias for another valid type constructor, but represents a new atomic constructor that is only equal to itself. This means that declaring a nominal type modifies the space of existing atomic types, and this phenomenon is called "generativity" (a a form of type-checking-time side-effect).

You can structurally encode a constructor in Haskell of this form:

data T x y = C1 (F x y) (G x y) | C2 (H x y) (I x y)

as

T x y = (Name_T, (F x y)*(G x y) + (H x y)*(I x y))

Here Name_T is a pure name encoded at the type level. Uses of C1 or C2 take you to the appropriate branch of the sum.

The point is that `T x y` is not *equal* to this encoding but *isomorphic* to it. `T` is only equal to itself as a type constructor. You can split any `data` declaration in a `type` part that gives the structural definition following your encoding, and a `newtype` or `data` part that generatively produces a distinct type constructor with this represetation.

Yeah, that seems a good characterization for Haskell's situation.

Okay, that makes sense, I was confusing what Haskell does with structural type. Haskell types obviously have a structural component, but are also nominal.

What happens when you introduce datatype generics though like for example:

data Tree x = Leaf x | Branch (Tree x) (Tree x)
data List x = Nil | Cons x (List x)

Where you can de-construct the Tree and List types generically over the sum '|' and products on the right hand side:

map f (x | y) = (map f x) | (map f y)
map f (x * y) = (map f x) * (map f y)

Here we can generically recurs over the structures of Tree and List, even though their constructors have different names.

It seems to me you can regard the same underlying types as nominal or structural depending on the definition of equality you want to use at any given time.

Named types are fundamentally different from structural types mainly in terms of security because the type name can be used for encryption in messages.

For Awelon project, I use structural sealer/unsealer functions to model encryption of messages. E.g. any type `a` may be wrapped as `Sealed key a`. Sealed is just a primitive structural constructor together with pairs, sums, etc.. The key may be discretionary like `foo`, in which case it's acting a lot like a structural newtype wrapper (convenient for modeling nominative types), or it might be cryptographic like `aes$key` or an ECC public key.

This is structural, rather than nominative, because the type ultimately depends on the intrinsic structure of the key, rather than on the origin, name, or other extrinsic properties.

Security is becoming increasingly important and dominant.

However, it should be intuitive, efficient, and invisible. Hiding, encryption inside type names can be very effective.

I agree about the importance and need for security to be intuitive, efficient, and implicit. What evidence have you for the "increasingly dominant" assertion?

I don't understand what you mean, and this doesn't seem consistent with your earlier statements about equality. I am not sure what encryption has to do with type systems either? Are you confusing application domains? If I want encryption I would use elliptic-curve for asymmetric or AES256 for symmetric encryption. How would these algorithms interface with the type system? Encryption is not an area where any ad-hoc algorithm is good enough.

How would these algorithms interface with the type system?

It isn't difficult with dependent types. The key becomes part of the type.

A specialized case for the type system could also do the job, if you don't want general support for dependent types.

You mean the key is in the source code. That's not a good idea where you want security.

I mean the key is in the type. Whether said type parameter is instantiated in the source code is a separate issue. I don't actually allow keys in source code for my AO dictionaries. Though, my motive is less for security reasons than to limit entanglement with specific machines and hence protect portability and reusability of code. Cryptographic sealer/unsealer pairs can only be constructed dynamically. But the whole point of dependent types is to support static typing for flexible runtime constructs.

Security is not a good reason to abandon the algebraic properties of type systems. Hiding information is not a good security model. Personally I would want a capability based security model where access tokens are required to pass messages across process boundaries.

The Java like security mechanism, using (nominal) type checking to prove code secure, before allowing it to run in a privileged environment is just a bad idea, that has been proved insecure by real world exploits.

If the type checker enforces security, then hand generated byte code is going to easily break the system.

Further nobody has yet argued why nominal equality has any valid use with functions.

The thing you call "access tokens" is better known in the PL world as "object references". If I don't know what I'm invoking, it doesn't make all that much sense to invoke it.

Unfortunately it is possible to find objects by searching memory, so just a reference is not an effective security mechanism. You need the kernel to control the memory mapping as well.

Memory snooping can be prevented using VMs (e.g. JVM) & every-word-tagged architecture.

Whilst this is good in theory, without formal verification techniques there are going to be flaws. See: http://www.blackhat.com/presentations/bh-asia-02/LSD/bh-asia-02-lsd.pdf

Besides, once you have a virtual-machine like the JVM the object reference is some kind of objct-handle enforced by "emulated hardware", so is really what I was talking about regarding MMU support, but in a virtual machine rather than the actual machine.

JVM protection works OK as long as there is no JNI.

Providing there are no bugs in the library classes (which don't get verified), no bugs in the byte code verifier (because the VM itself is not secure and can be broken with stack misalignments changing the types on the stack), and of course no bugs in the VM implementation. Given the history of bugs in these things it seems neive to think there are not still other bugs we have not found yet. Without formal verification the JVM has shown that we cannot make something this complex without security compromising flaws.

In practice, JVM protection is OK; but some libraries can be doubtful.

I more or less believe that the only way out is signed code. But I have no idea where current research is, if any.

Not only that, but if module-exported functions need to be declared anyway you open up a lot of freedom without causing the inference algorithm to be potentially non-terminating. Overloading and polymorphic recursion being two examples.

"Local", here, probably shouldn't mean "within a procedure". It's equally good if it means "within a module".

I agree with const. Type inference is a dismal failure, overloading is much more important. I have no idea why academics think it is so important to leave type annotations off function arguments.

My language Felix does not do inference but does have overloading (both open like C++ and using type classes like Haskell). The compiler is written in Ocaml, functions usually without annotations on arguments.

Annotations add clutter but I have to add them anyhow when there's a type error because the error is often entirely incorrect in itself, reporting the correct type is wrong when it was a prior use that was incorrect. The annotation is the only way to force a diagnostic at the actual point of error.

On the other hand the loss of overloading is barely tolerable in Ocaml and would be utterly intolerable in a larger scale system. Felix models C, and makes typedefs like "size_t" abstract so do you know how many integer types that is? Do you really think its in any way shape of form sane to have twenty differently spelled names for addition?

Overloading is possible with type inference, see Haskell type-classes, which is a much cleaner version of what is just now being added to C++ in the form of Concepts. Type-classes (like concepts) solve the dependency injection problem.

C++ now has type inference too, as nobody wants to write:

for (Map<String, Vector<Pair<Int, String>>>::const_reverse_iterator i = thing.crbegin(); ...

instead of:

for (auto i = thing.crbegin() ...

The other thing you are neglecting is generics and polymorphism, I write lot of code like this:

template <typename A> void swap(A& x, A& y) {
    A tmp = x;
    x = y;
    y = tmp;
}

Whereas I could write:

swap(x, y) {
  val tmp = source x;
  sink x = source y;
  sink y = tmp;
}

And have everything inferred with no loss, as the function accepts any reference type, so the type information does not add anything.

When you write code generically, for example a sort function using iterators you almost never want to restrict things to a specific type. Instead you want to write things generically over interfaces, and let overloading sort out what to call. So in the above example, 'source' is overloaded to dereference readable references, and if there is no definition of source, it means it is not a readable reference. 'sink' is overloaded to dereference writable references.

You can create new clever reference types, and as long as they overload 'source' and 'sink' the above definition of swap will work for them. The type inferred for swap would be something like:

swap :: Readable c, Writable c, Readable d, Writeable d => c a -> d a -> {Read c, Write c, Read d, Write d} ()

Where Readable and Writable are type classes, and Read, Write are parametric effects. As the type-classes and effects are cumulative (so function types include all the class constraints and effects of their sub-functions) you probably don't want to ever type these for complete programs.

You may wish to include partial type signatures though, so could allow "type-assertions" that are checked at compile time like this:

swap(x, y) {
  require Readable (typeof x) && Readable (typeof y)
      && Writeable (typeof x) && Writable (typeof y);

  val tmp = source x;
  sink x = source y;
  sink y = tmp;
}

So you can selectively enforce the requirements for a function.

C++ always did type inference. But due to design decisions in C (header files) and templates, they are stuck with compilers which sometimes will reparse header files several thousand times, sometimes orders more, during compiles. I don't understand fully why; it probably is something they can get rid of but it is a major burden.

So auto is there because: A. Relieves the programmer of the burden of writing a complex type and getting it right. B. Relieves the compiler of (extra template instantiations, and) doing an equality check on the intended and inferred type.

Template errors are horrible. Fixing types probably eats away a great many number of man-hours for C++ programmers, and man-centuries globally. Getting rid of the simple equality check probably shaves of at least 10-20% of the running cost of a C++ compiler if auto's are used everywhere.

I have no idea why academics think it is so important to leave type annotations off function arguments.

I've long wondered about that myself. Academics tend to go in for "pure" strategies, where you take something about as fer as it can go — on top of the common human tendency people already have to do things to excess — and having come up with a clever way to do it (Hindley-Milner), maybe they wanted to exploit that cleverness for all it was worth.

There are also plenty of dynamic language users who don't mind leaving types off of their function arguments, they also don't miss static types (for all the supposed trouble they cost for their benefits).

Most of these people aren't academics.

Seemingly, type inference becomes a problem when it's used to implicitly change the behavior of code. A typical Lisp, for example, doesn't do static typing but also doesn't do type inference. If something has a different type than you thought, that's bad; but when that original mistake gets magnified in a runaway fashion by widespread implicit type inference, that's worse.

It would annotate the code as I am writing it. It would show me what it has decided the types are. That way I can see more readily when it goes off the rails. And, I could toggle the visibility of it all, so I can more easily just see the Happy Path of things.

That sounds awesome. Though of course in the abstract we get to just describe the advantages, without the practical problems of a concrete implementation. How to present the annotations without cluttering complicated expressions into unreadability? This is, in a way, the same problem as the one where the programmer puts type annotations on parameters. It's also the same problem as I've encountered when I try to imagine an alternative to a built-in type system, where the programmer explicitly constructs theorem objects using constructors that are, in effect, rules of deduction: where do you put this theorem-proving code? I've been thinking you could attach this customized reasoning-code to individual objects, such as procedures... but then how do you do that so it doesn't just clutter things up? In fact, it seems to me this proving stuff, whether it be in the form of types or of something else, is a <pauses to gather nerve> cross-cutting concern, a sort of aspect.

This is a unfair.

As soon as functions start being used frequently in code (for example in monad code that uses them to replace all let-bindings, but also in callback-heavy code, higher-order library functions, non-specialized syntaxes for set comprehensions, etc.), annotating function arguments becomes a burden.

There is ample evidence that non-academics want type-inference of anonymous functions and local declarations: it was added in recent versions of C++ and Java (only for lambda-expressions I believe; Gilad Bracha refused to implement this for declarations back in 2001), possibly under the pressure of C# (which was partly developped with academics input). Before that you will find many questions from the practitioners of these languages asking why type inference isn't available to them -- they often justify the request by saying something like "static language X that I used before has it, and I really like it".

Well, the criticism was of taking type inference too far, which doesn't necessarily imply criticism of using type inference at all.

I certainly agree that annotating function arguments can be a burden. So there are drawbacks to doing it and drawbacks to not doing it. A principle I like to try to apply — one has to be ready for a serious challenge in order to apply it, though — is that when two strategies appear to require a trade-off beteween them, one ought to look for a third strategy that makes the trade-off evaporate.

Did you hear that from Gilad directly? Anyways, there is a lot of bike shedding that goes into industrial languages that can kill good features.

C# type inference is quite tame compared to classic Generic Java: you have local variable inference, added for LINQ mostly, and that is about it (there is type parameter bound inference, but that is in Java also). I wouldn't think that C# has more or less academic input than Java (just that Microsoft pays the academics more directly).

But type inference is a wonderful thing. We need more of it.

The Request for Enhancement JDK-4459053 : Type inference for variable declarations is publicly available, as well as Gilad's justification for turning it down. Relevant quote:

This is a well reasoned and logical RFE (that's rare enough that I feel the need to call it out). However, I don't expect us to follow this path in Java for the following reason:

The submitter's claim is that the type information in a standard Java variable declaration is redundant. This may be true from the compiler's perspective, but often it will not be true from the programmer's perspective. Consider:

Map m = getMap();

Humans benefit from the redundancy of the type declaration in two ways.
First, the redundant type serves as valuable documentation - readers do not have to search for the declaration of getMap() to find out what type it returns.
Second, the redundancy allows the programmer to declare the intended type, and thereby benefit from a cross check performed by the compiler.

Nice. I wonder what he would say today given that he later pushed forward on optional typing?

Also, smart editors can really help here. The type annotations is known, the programmer just needs to see it somehow. The problem is primarily one of real estate.

I get really skeptical when I hear categorical statements like your last sentence. May be just a knee-jerk reaction, but there is a important advantage of (some) redundance in programs, which is the obvious one of error checking. Just to throw out a strawman: if every sequence of characters was a valid program, then by definition there are no invalid programs, so no error checking is necessary. That's probably going to wind up confusing a lot of users :-)

To be more to the point, too much inference is also bad, since errors manifest themselves in the compiler's inferences--the internal magic. Generally, compilers have been really poor at communicating the actual source of users' errors in these cases and instead tend to dump their problems on programmers. Great user experience for success, poor in the error case.

Then there's C++ which manages to combine mind-bogglingly high amounts of redundancy with even larger, more redundant and ultimately inscrutable error messages. Truly a remarkable accomplishment.

Type inference is pervasive in natural language, why not in our programming languages? Why must programming be some kind of stilted activity.

Redundancy is great when you need it, so why not make it optional rather than mandatory? Ideological inflexibility of static typers is kind of why dynamic languages remain popular.

To be more to the point, too much inference is also bad, since errors manifest themselves in the compiler's inferences--the internal magic.

Two issues here. First, type inference tends to be opaque and the error conditions tend to be ugly, so don't do that. We have plenty of choices, make different ones.

Second, I do agree that the key is good tooling, but then that is my whole research direction. Type inference without a heads up display in the editor is just...horrible, so let's not do that. In the past, programming languages were designed without concern for tooling; today this is changing very rapidly. It is no longer sufficient to poop out a compiler and run-time for a PL and go home; you are designing a programmer experience, not a programming language, so do that.

Then there's C++ which manages to combine mind-bogglingly high amounts of redundancy with even larger, more redundant and ultimately inscrutable error messages. Truly a remarkable accomplishment.

This is quite easy to accomplish actually. C++ is bad in some many ways, that poor realization of a concept in it should not invalidate the concept.

Type inference is pervasive in natural language

Interesting. Why do you think so? I'd think typing itself is artificial.

Not all phrases in natural language that are syntactically correct are semantically correct. Think about it. Natural language understanding is just a big type inference problem (replicating what we can already do in our heads).

Not all phrases in natural language that are syntactically correct are semantically correct.

It seems to me that correctness is not an absolute concept in application to natural language. (I'm also doubtful the distinction between syntax and semantics is absolute there either.)

Natural language understanding is just a big type inference problem (replicating what we can already do in our heads).

I don't see that. I'm honestly not trying to be difficult, but I don't see why you think that. That's separate, btw, from whether or not I would agree with you; I could imagine seeing where you're coming from and simply not agreeing, and that would be interesting (though I suspect we might agree on principles, if not emphasis, once we reached that level of understanding). But I'm just not seeing it.

The flower ate the car in tomorrow.

Syntactically correct, semantically very awkward. (Flowers don't typically eat things, cars are not typically eaten, you can't really be in tomorrow).

Types are pretty common in natural language...well, at least object-oriented ones.

In the past, programming languages were designed without concern for tooling; today this is changing very rapidly. It is no longer sufficient to poop out a compiler and run-time for a PL and go home; you are designing a programmer experience, not a programming language, so do that.

Only if you do so for the right reason. Tooling is great as an aid, but making it a prerequisite for an acceptable user experience isn't. A language is an abstraction and a communication device. Supposedly, a universal means of expression, relative to a given domain. It fails to be a (human-readable) language if understanding is dependent on technical devices.

There are many other places than your editor where you need to read and understand code: in code reviews, in diffs, in VCSs, in debuggers, in crash dumps, in documentation, in tutorials, in books printed on paper. You can try to go on a life-long crusade to make every tool that ever enters the programming work flow "smart" and "integrated", and denounce books and papers as obsolete. But that is going to vastly increase complexity, coupling, and cost of everything, thus slows down progress, and just creates an entangled mess. And in the mean time, every programmer will struggle with the language.

Nothing ideological or academic about that, just common sense.

You have a computer with increasing amounts of power in front of you, use it. Yes, it is completely possible you have to do code reviews on a deserted island with no power, but that isn't the common case.

We need to spin off a new post to start a new debate. :)

You have a computer with increasing amounts of power in front of you, use it.

I have been thinking about that for a while, and the implications for programming languages. As I see it, the time of exponential growth has ended and we're now in the time where microprocessors will shave off some remaining constants, and that will be it. I.e., I fully expect that people in two decades will still be using a ~2Ghz multicore machine with some vertical and horizontal integration.

So programming language designers cannot rely anymore that nonperformance will be fixed some time in the future.

Looks to me, that apart from some constant speedups, we are looking at the endgame of computing. I guess we should be happy with where we ended, but some things will simply remain out of reach.

Forking this. Stay tuned.

I don't think so, graphene transistors http://www.nature.com/nnano/journal/v5/n7/full/nnano.2010.89.html are coming, as are optronics and spintronics, including things like holographic associative memories.

There are still huge performance leaps to come. Normally when people say we are at the limit, it is just prior to one of these game changing breakthroughs. I am reminded of Lord Kelivin saying "There is nothing new to be discovered in physics now, All that remains is more and more precise measurement."

Point taken. Guess I should rephrase it as: What if this is the end of the free-lunch period?

Maybe I'll just address this here. The problem with computing is peak performance, we have plenty of cycles to spare if we don't need them all at once. Having an IDE/editor/debugger that sucks up more cycles isn't that big of a deal (well, as long as IBM doesn't write it). RAM/SSD is also still going up by leaps and bound, so we can save a lot more stuff than we used to be able to.

Oh, that. I agree there's enough horsepower for IDE's, certainly if the language is designed right to support it.

The thing I wonder about is that there are probably languages we will never see. Like the ASF+SDF system. As I gather, it's a system with incorporates the latest in parsing and you can implement a compiler in it through more or less logical expressions which do term rewriting.

I won't touch it but it seems some people like it.

I think I read somewhere it takes 6 minutes for a self-compile. So, in the old days, if I am right, they just would need to wait a few decades, get the same 3500x speedup as we all experienced over the last decades, and *poof* problem solved. A fast purely declarative compiler.

If stuff remains the same, their technology is simply out of reach.

We've have known that handcoded logic-based rules are a dead end at least since the 80s, which is why most of AI has moved away from encoded logic to machine learning (and these days, deep learning). So ya, ASF+SDF looks great on paper just like Prolog and Datalog do, but it simply doesn't scale. Now training a neural net on TB of data is simply a matter of purposing a cluster of machines (optionally with GPUs); the opaque code that comes out runs fairly efficiently at run-time.

The next big leap in non-functional declarative programming will be figuring out how to combined machine learned behavior with programmer encoded intent.

I am sorry but I don't think you get what the ASF+SDF system does.

The next big leap in non-functional declarative programming will be figuring out how to combined machine learned behavior with programmer encoded intent.

As I see it, we could more or less model non-deterministic behavior together with some heuristics for a preferred behavior. Machine-learning algorithms (perhaps together with simulations and test data) could then locate high quality (and high-performance) programs within the space of behaviors indicated by the programmer.

I really hope programming does not become like trying to teach my dog to fetch my slippers (note: I don't really have a dog, nor slippers). Training is an imperfect activity, and frequently results in chewed slippers.

There is room enough for both 'soft' (flexible, adaptive, non-deterministic) and 'hard' (functional, deterministic) components in programming. Soft aspects can include probabilistic models, soft concurrent constraint models, ant clustering/sorting, and machine learning.

I expect it would be easier and more effective to use soft aspects when it comes to recognizing slippers and fetching them, compared to using the hard aspects to do the same. I wouldn't even begin to know where to begin hand-coding a slipper recognition function.

There are definitely many activities where training is better than programming, but you have to write your neural-net / deep-learning code in some language or other.

Certainly we need to write our learning models somewhere, in some language. This isn't so different from needing to write a compiler or interpreter somewhere, in some language. The question is how to make these soft models accessible within our languages, without jumping through a bunch of hoops to construct or use them. Presumably, if they're accessible to humans, they're probably also accessible to the compilers.

I think that non-determinism within programs is an excellent opportunity to apply learning models while still giving developers a high level of control over the resulting models (e.g. by controlling where they introduce non-determinism). Non-determinism doesn't need to be about concurrency, it just means the programmer has allowed multiple outcomes.

Maybe the training sets or simulations, also, should be modeled and represented within the language, and thus training could just be part of long-running compilation (albeit, probably much more heavily cached).

That is why training has to be combined with programmer encoded intent, at least until training can do everything itself.

Editors, debuggers, crash dumps, and type setting in documentation, tutorials and books are already language specific. VC is the exception. Reading plain ASCII text is also dependent on technical devices, it just happens to be (1) already widespread (2) exceptionally poor for code.

A language is an abstraction and a communication device.

The 'language' metaphor for programming, oriented around parsing and readability, is popular. But it certainly isn't essential to programming. Just a few alternative metaphors that are viable bases for programming: circuitry, sculpture, chemical reactions, relationship graphs.

Despite the name, the study of Programming Languages certainly isn't restricted to programming models within the 'language' metaphor.

I have sincere doubts about the language metaphor for programming in general. Reading code does seem useful for understanding small samples of code, but it doesn't scale nicely to common application sizes. Nor is it a great fit for a lot of the work that goes into software development, hence we develop a ton of external file resources.

Tooling is great as an aid, but making it a prerequisite for an acceptable user experience isn't.

Tooling is always a prerequisite for an acceptable experience. Some tools - such as keyboards, monitors, and command lines - are just more widely accessible than others.

This can change over time. E.g. it used to be that printers were widely available, but a lot of homes and offices have gone mostly paperless. In the future, keyboards might be less widely available as people move towards tablets, mobile devices, augmented reality, and the like.

As accessibility of tools change, the programming experience will also need to change to keep it acceptable.

You can try to make every tool that ever enters the programming work flow "smart" and "integrated", and denounce books and papers as obsolete. But that is going to vastly increase complexity, coupling, and cost of everything, thus slows down progress, and just creates an entangled mess.

I'm curious what the actual numbers look like. My expectation: this 'vastly' isn't as vast as you imagine. It must be compared to other language-specific development costs (typecheckers, compilers, linters, emacs modes, Eclipse plugins, etc.). Further, the amount of reuse available for alternative models can still be pretty high, even if not reusing conventional programming tools (e.g. instead reuse the browser and web service architectures).

There is no alternative to reading the code for large projects and developer spend more time reading the code than writing it on large project. For aged project the relationship read lines to written ones could be more than 1000 to 1 on average. For example, I had recently spent full 2 days reading code and debugging (which also counts as reading) just to fix two lines of the code that were the root cause of the bug. All that code was written by other people and some of them were already gone from the company. This is normal state of affairs in software development. With exception of academia, one-man-projects are rare occurence. Also usually mulitiple people work on the project and some of them go to other companies or even die.

There might be changes in the future with technology development. But I have seen no realistic contender to plain text for large scale software development. Right now only plain-text supports development for large distrubuted teams with multiple workstreams. Other artifacts could be used for the projects, but they usually have a limited list of persons resposible for them like images.

Reading code is indeed the normal state of affairs, and that's unlikely to change for conventional PLs and the projects developed around them. To even begin to pursue 'realistic alternatives to plain text' we must step away from conventions.

(edited to add detail and content):

Your inability to easily isolate a two-line bug required you to read code for two days. That's a bad scaling factor, but is typical for reading code in large projects. If we had sacrificed a little plain-text readability or writeability in order to improve locality and the ability isolate bugs quickly using tools, perhaps you'd have saved a day or two.

I believe PL designers should focus on improving our ability to quickly and effectively reason about code without reading many implementation details or simulating machines in our heads. Limiting what we need to know to isolate concerns is already a common theme in the security communities, and I believe we PL designers have a lot we can learn from security concerns (malign and buggy aren't so different in practice). I expect many useful local reasoning properties will come at some cost to plain-text expressiveness or readability. For example, overloading is one issue mentioned recently. Overloading is convenient for plain-text expressiveness and readability, but requires knowing a lot of context to trace which implementation might be invoked, and hence hinders local reasoning about program behavior.

I'm also interested in PL designs that support lots of different visualizations/lenses (and animations) to quickly understand a program. I think having many easy visualizations will be more useful than one tyrannical representation for reading code and simulating it in our human heads. But I think creating tools for alternative visualization is severely hindered by the same designs aimed to improve plain-text readability or expressiveness or integration with content that doesn't nicely fit plain text (sophisticated syntax, overloading, namespaces, ambient authority, effectful entanglement with the environment and dynamic dependencies on external data files, etc.).

Right now only plain-text supports development for large distrubuted teams with multiple workstreams.

Actually, we have a lot of experience with content systems other than plain text for large distributed teams. It's just most of these aren't used for programming systems, or are used only indirectly. Wikis are an example I'm using as inspiration. DVCS systems like git and github are another big inspiration, operating at the level of entire wikis/dictionaries.

There is a difference between local and global scope. Local type inferrence is generally considered ok. Global is hard to implement and actually confuse things greatly for readers. The problem is that contract inferred from usage spread in undefined scope rather than usages checked for contract.

For dynamic languages, one has to communicate contract via non-language means. For the dynamicaly-typed code written by other people, I'm regularly lost because because intention of definition is less clear. I'm have to analyse usages to infer actual contract. For statically typed languages I get a good idea by checking the definition itself.

For class-based language, I think type annotations are MUST for public/protected/exported objects (as types specify intended contract), SHOULD for private (more specificatlly, MUST for definition parameters, SHOULD for results), and OPTIONAL for local scope.

Generally speaking, if the compiler has a hard time understaning the code, the human will likely have even harder time.

I was interested in why Darcs wouldn't perform and followed your link. Of course, performance is not obvious for Haskell, it isn't for any language, but for a functional language it is rather fast and it should be possible to get small to medium sized applications right. Certainly when they are of the data-processing kind.

Darcs doesn't perform because of a design error. What I got from reading the complaints is that it is impossible to get right and therefore Darcs seems to be fundamentally flawed. They didn't think about gigabyte patches, a shame, guess they need to create a new tool.

busy writing code...

Source line and other annotations can go a long way here in enabling good debugger experiences.

The Chicken stack check is very portable in practice if not in theory. To oversimplify slightly: a local variable in or near main() has its address taken before the Chicken program starts up, and then this is compared with the address of a local variable in the current function. The absolute difference of these gives an indication of the stack height. I know of only one implementation of C that doesn't use a contiguous stack, even though ISO C does not technically permit the comparison of pointers that don't point to the same object.

Note that Chicken uses a maximum stack size for this purpose that is fixed at configuration time and is much less than what the OS allows for the stack. This improves the liveness of GC (since a minor GC is run whenever the Chicken stack fills up), and allows recursive C code to be invoked from Chicken code without problems.

As for deeply recursive programs, can you point to this wontfix bug? When I enter (define (foo x) (+ (foo (- x 1)) 0)) in the interpreter (which does not see this as a tail recursion) and run (foo 0) on a 32-bit system, I eventually panic with "out of memory - cannot allocate heap segment - execution terminated", exactly as I would expect. Note that on heap overflow (when a major GC doesn't gain any memory) the heap size is always doubled, which is probably too aggressive with large heaps.

It's a check that, if done, would make overly recursive programs fail safe instead of crashing the process. Proper tail calls still work correctly even without this check.