Lambda the Ultimate

Despite some of my past statements in disagreement with many Rust design decisions, I'd like to say: They are quite clearly doing excellent language research. But even more importantly, they are doing stellar community management. I hope this ergonomics initiative is wildly successful because as much as I'd myself rather write low level code with Terra, I'd also much rather debug colleagues' Rust than C/C++.

At least a sub-part of the question "what to make implicit?" must deal with whether a particular isomorphism be dealt with implicitly of explicitly. I contend this issue is not merely one of ergonomics, but involves mathematics too.

For example in Felix the type isomorphism T * T * T = T ^ 3 is implicit. A tuple of three values of the same type is an array. It's not merely isomorphic to an array. It IS an array. This choice has consequences. Is the choice even sound?

If we carry this through we require T = T ^ 1, and 1 = T ^ 0. This may seem reasonable but the consequences are dire. Consider a function operating on an array, T ^ N, and set T = U ^ M. This raises the issue is (U ^ M) ^ N = U ^ (M * N)? Or should that be U ^ (N * M)? And conversely, if you see a function f: T^N where N=1 and T=U^M, does it iterate once over a single U^M or over U many times?

Its clear, that even though A * B is isomorphic to B * A you'd never make such an isomorphism implicit. On the other hand, almost all functional programming languages make the lift of a function to a function value implicit to the point where most programmers are unaware of the difference, and some compilers appear to throw the difference out too early (Ocaml I suspect).

So before we even ask about ergonomics, we have to ask if making an isomorphism implicit is sustainable.

For Felix arrays I don't know the answer. However at least part of the failsafe is that for a polymorphic function you can, and sometimes *must* explicitly specialise the type variable. Clearly the implicit isomorphism raises issues which suggests it is a bad idea. But in common case is its significant simplification. So perhaps it is OK, if an implicit operation has ambiguous corner cases, provided there is a way to resolve the ambiguity?

[More examples next post]

This is another example. In C you can implicitly convert in both directions between a T* and a void*. In C++ the conversion from a void* to a T* requires an explicit cast:

void *pv;
int *pi = (int*)pv;

As you can see, this make some code much more verbose, and I once spent several days converting a C library to C++ just adding these casts so it compiled. Was the removal of the implicit conversion a good idea?

But it isn't just a matter of ergonomics. Stroustrup introduce a more refined collection of casts in an attempt to make it easier to reason about a particular conversion. I had a huge argument with him about his choices because the alebgra just doesn't work. For example you have to write this:

int const *pic;
void * pv = const_cast<void*>(reinterpret_cast<void const*>(pic));

which is stupid IMHO. The idea is that you have to use a const cast to cast away const, separately from changing the pointed at base type with a reinterpret cast, but this makes no sense at all if you're casting away the base type entirely, indeed the idea of a void const* is nuts because you cannot do anything with it without casting it.

C has implicit conversions which make reasoning difficult. C++ takes this to an extreme: one argument "normal" constructors specify implicit conversions. Derivation specifies implicit conversions. You can even define operator methods to specify an implicit conversion. The situation is so unreasonable C++ has an "explicit" keyword for constructors to disable the implicit conversion. Throw in overloading and the mess deepens .. and now add templates and all hope is lost. Zero (literal 0) is so ambiguous a specific nulptr was introduced.

There are rules. They're hard to follow. But implicit operations in C++ can never be eliminated because templates depend on them. Some here might criticise the type system as being unsound .. that is a minor issue which rarely has any consequences compared to the difficulty of reasoning in the presence of so many implicit conversions.

So there is another dimension to the arguments about what should be implicit: one must not only consider the underlying algebra of the existing language but ALSO the algebra of possible extensions. Almost ALL implicit operations collapse under some extension.

I have to write one of these in Felix:

for i in 0uz ..< a.len ..
for i in 0.size ..< a.len ..
for i in 0 ..< a.len.int ..

because there are no implicit integral conversions (and the type of the length of an array given by the len function is size, not int). Its a real pain compared to C/C++, and the pain gets worse in more complex expressions. It isn't just a burden figuring out the types involved, one must choose where to do the conversions. Worse, if some types change, the expression has to be edited. I chose to disallow implicit conversions so that overloading would be easier: overloads require an exact match up to type variables precisely so the implicit deduction of the type variables can work directly by unification. But the choice has consequences.

A way figure out context dependence is to look at whole program transformations from the whole language to a restricted dialect of the language in which the implicitness is not there.