Lambda the Ultimate

This conversion is completely unsound for mutable collections. If we pass a MutableSet<Int> to a procedure expecting a MutableSet<Int|Float>, then it will feel free to add a Float to it, which violates its original invariant.

But for immutable collections, it is always sound. A procedure that is prepared to accept either ints or floats in the set it receives should be fine with a set that is all ints or all floats. I see no reason not to permit this conversion always.

By the same token, it should be possible to pass either an ImmutableSet<Int> or an ImmutableSet<Float> where an ImmutableSet<Int|Float> is allowed. This coercion is what Algol 68 called uniting (it was the first language to introduce the word "union" for alternative types).

This is the set situation in my language, if it helps. This would be a set definition:

/*
  An existence of '@' denotes existing variables. Its absence
  denotes new variables. I write the function operator backwards
  (<-) to achieve data centric solution. Existing variables are
  expected to be applied later as parameters through pattern 
  matching. New variables don't require application and
  automatically lift one level up on application of their children.
  I introduced meta sections to be filled between '<' and
  '>' that accept only valid types.
*/

Set <- (
    (
        Item <- <@T>,
        Next <- (@Set @T | ())
    ) <- (T <- @Type)
)

Now if we want to instantiate a set we can do it by first providing a type as the first parameter:

UnmutableSet <- @Set @Int,
MutableSet   <- @Set (@Int | @Float)

Then we can provide elements by pattern matching:

X <- @UnmutableSet (1, 2, 4)

Now it would be perfectly safe to appply elements of the unmutable set X to construct a mutable set with the same elements:

Y <- @MutableSet @X

In this case the implicit conversion works.

Let's see the other side by redefining our unmutable set:

UnmutableSet <- (@Set @Int | @Set @Float)

now we can write:

X <- @UnmutableSet (1, 2, 4)

or

X <- @UnmutableSet (0.1, 0.2, 0.4)

but in niether case X can contain both elements of Int and Float. I think that I am dealing only with unmutable sets in this example also, so the situation is again safe, it is either a set of ints or a set of floats, it is never mixed up. Again, I can do the following, no matter what X is, a set of ints or a set of floats:

Y <- @MutableSet @X

I hope I didn't miss the point :/

I propose a general principal which is that almost all conversions should be explicit initially. Then, very carefully add implicit conversions to simplify concrete syntax, but only when you have use cases to add to the regression test suite, and only when the implicit conversions act together soundly. (1)

As a guide, favour isomorphisms and natural transforms for implicit conversions.

What you make implicit is, to quite some degree, what distinguishes your language from others. Providing explicit conversions even if not commonly elaborated has useful consequences: there is a way to make a complex combination more explicit, and, for value conversions, the explicit form may sometimes usefully be promoted to a function.

However there are some implicit conversions which are hard not to build into a language. One of these is the conversion of functions to closures and the corresponding application operators. Its quite common to implicitly convert a function in the function position of an application to a closure, and use the closure application operation in the concrete syntax, and to convert a function used in the argument position to a closure as well.

Another common implicit conversion is eta-expansion. Some languages such as Felix implicitly convert type constructors to function closures this way. Ocaml, for example, does not.

Almost universally, specialisation is implicit when applying a function to an argument, the parameter type of the function is specialised to match the argument. however this is not always possible, especially if you have type inference. A good example is Ocaml polymorphic variants, which sometimes require explicit conversions as well as explicit type annotations.

So again, as a general rule, start with as much as you can explicit, if only to ensure there is in fact an explicit way of explaining what you intend to make implicit. I think you may be surprised how much is already implicit and finding explicit representations is often quite challenging.

(1) By "soundly" I mean that if the conversions are ambiguous, the semantics are the same. Often several compositions of conversions could be expected when omitted, but the choice has no consequences. Indeed in languages with overloading (such as C++) implicit choices abound and are actually the basis of apparently generic behaviour. One finds quickly this is only apparent when trying to generalise it, and it can certainly be confusing.

This actually leads to another principle: if the program is modified or the programmer just made a mistake, and an error is found, the diagnostic can pinpoint and explain the source of the problem. C++ template errors and HM-type inference are two examples of very bad design choices according to this principle, since it is impossible to explain the errors well in both cases.

There is no better example of very bad design choices than C++. It supports overloading, implicit conversions between numeric types, implicit conversion to bool of both integers and pointers, implicit conversion of 0 to NULL pointers, implicitly applied explicitly defined operator conversion, implicit overloads of function templates, implicit specialisation, implicit conversion of references of references to references, implicit conversion of non-const to const pointers and references, implicit constructor conversions, implicit overloading of function on assignment, implicit use of the "this" pointer in methods, implicit type variables inside template classes, implicit qualification of names in classes and namespaces, introduction of implicit qualification with using declarations, implicit conversions of arrays to pointers, implicit conversion of functions to function pointers, implicit conversion of function pointers to function closures, implicit class-nominal subtyping, sporadic silently lazy name binding (dependent name lookup), implicit disambiguation of ambiguous parsing of some constructions as definitions or declarations, implicit conversions of pointers to void* ... er .. did I leave anything out?

Some of these implicit conversions actually lead to unsoundness in the type system, the most well known being the implicit conversion of an array to a pointer, and implicit subtyping of pointers, together make the type system unsound (an array of derived converts to an pointer to a base which if increment moves the wrong distance in the pointed at array). This in turn shows that the underlying C language is fragile and badly designed, because it is hard to generalise.

Another, less well known unsoundness is the implicit conversion of the type of a class under construction to the non-const pointer "this" even if the value being constructed is bound by a const reference: if the this pointer is allowed to escape the object becomes mutable, despite being declared const.

Yet another issue, this time also well known, is the implicit slicing of a value of a derived type on assignment to a variable of base type. The problem is that the variance is wrong, the assignment is unsound. Be wary of this if you have a language with mutable objects (as already mentioned in a previous post). Assignment is invariant, you cannot "subtype" either the LHS or RHS.

I didn't say commutativity was required of operators, just for implicit conversions. The reason I think it is a sane requirement in that case if that you cannot "see" the actual operations chosen, it had better not make any difference.

The issue is not type soundness, but semantic soundness. Obviously we can have two pairs of functions for which

    f . g != h . k

even though the types agree (the comparison is type safe!). I'm saying you should not model f.g,h,k as implicit operations. In C++ this problem does in fact arise, and one has to very very carefully try to decipher disambiguation rules in the C++ Standard to discover what actually happens.

Type checking reduces the possible class of errors in a program, it doesn't stop the program going wrong. More expressive type systems reduce the class more in theory, but in practice this may not be realised unless the typing is intuitive because programmers can always bypass the type system one way or another (by casts or by simulation).

I think it is also incorrect to say that in a sound type system you cannot make unsound rules. The rules of the type system are not governed by the type system, they're outside the type system by definition. If you wish to catch errors in the introduction of new type rules you need a kinding system for those rules. It will not catch all errors, so it will not stop you making your type system unsound, but it will help.