Lambda the Ultimate

At the time of type checking we may freely propogate information about the type of a union without worrying about what its compiled representation will be, so it doesn't make sense to me to say that the inference algorithm can not cope with untagged union types.

Perhaps what they mean is that compilers are often unable to prove which variant of a type an element of a union type is, and so the compiler is unable to remove type tags. This interpretation seems to make more sense.

Gavin

As I see it, the problem with untagged unions and just having the type inferencer generalize as it goes is that you end up with an inferred type which doesn't actually prove anything useful about your program. In other words it may be possible, but it's certainly completely useless.

Type inference with untagged unions is not neccessarily completely useless. If a program contains any explicit annotations, then the inferred type can be compared with the explicit type in order to check well-typedness of a phrase.

I'm just too used to type inferece without any annotations... Still, I think a weaker version of my statement still applies: You may end up diluting the static guarantees to a point where their value is dubious :).

The way I see it, union types mess up the type lattice. If you consider the union of a bool and a real (bool|real), then this is an artificial least upper bound in the type lattice. Bool and real would never usually have a common least upper bound, other than the TOP type. In this way, any two (or more) types can effectively get a new artificial LUB. In principal the inference algorithm can keep inferring new union types, eventually approaching the TOP type since the union could include all the types in the type system.

Is this interpretation way off ?

"Most type inference algorithms cannot cope with untagged union types."

I am curious as to why this is the case.

Well is it really the case? Which type inference algorithms can or can not cope with untagged unions? Is it really "most"? How many type inference algorithms did they survey? That's the problem with Wikipedia, you should never trust what they say, because they don't cite their references.

I suggest you use Citeseer to get your facts from reputable sources.

Alternatively, my programming language research engine revealed several interesting papers which seem to contradict the wikipedia article when I fed it the terms type inference untagged union. I hope this is helpful.

That's the problem with Wikipedia, you should never trust what they say, because they don't cite their references.

Untagged unions make type inference combinatorically explode, because you can never unify two type informations - they may always be unioned instead of being equal.

However, the real problem is that untagged unions do not mix well with polymorphism - independent from type inference. And most type inferenced languages value polymorphism pretty high.

Just consider:

f [T] (x : String+T) = case x of
  x1:T -> ...
  x2:String -> ...

What is the meaning of f if you instantiate T with type String? Or with String+something? Any answer will be like a hack.

I don't think this is a typing problem, just say A + A = A.

The behavior of your example depends on how case is implemented. Either you require the cases to be disjoint, then this is an error, or either the first or the last match wins.

You may loose a few nice properties simpler type-systems may have, but that doesn't mean it is a hack imho.

It seems to me undesirable to allow a computation to ask if a value is of a particular type, and that with sufficiently expressive types such a question will often be undecidable or intractable. So from my viewpoint, branching should be done on 'tags' and not on types (and algebraic types are 'tagged').

(If I've mis-used terminology, or if there is a better way of expressing this viewpoint, please correct me - I'm still working my way through the literature. Also, this is my first post. Hello.)

[Also meant as an answer to Thomas_C]

The behavior of your example depends on how case is implemented. Either you require the cases to be disjoint, then this is an error,

Which basically means that you cannot have polymorphic sums, and the type language is not compositional.

or either the first or the last match wins.

Which means that polymorphic abstractions might silently break if you instantiate them with the "wrong" type.

On a related note, untagged unions are less expressive than tagged ones, because you cannot have alternatives with the same type - which is often needed (just consider abstract syntax trees).

You can work around the latter problems by using auxiliary (nominal) types in which you wrap the alternatives. But then you have just implemented tagged unions the tedious way, without all the nice additional checks from the compiler you get with the real thing.

You may loose a few nice properties simpler type-systems may have

Indeed, in particular the type language is no longer algebraic. That can break quite a few things. Effective type inference is one of them.

Branching on (polymorphic) types is also likely to be vastly more expensive.

Has anyone come across anything similar ?

These would present somewhat of a problem for a type inference algorithm, since the invariants may be of arbitrary complexity and thus cannot necessarily be evaluated at compile time.

The name for this idea in its most general form is "dependent types", in which types can include arbitrary computations, possibly involving run-time values. You're right in noting that it presents a problem not just for type inference, but for type checking as well. There are a number of problems that can occur, the most obvious of which are:

• Compile-time type checking might not terminate, since the type language can express non-termination.
• The phase distinction between compile- and run-time may be blurred or lost completely, since some values needed for type checking may not be available until run-time.

There are a number of possible ways to deal with these. We might restrict the language of types in some way that allows us to guarantee termination and a traditional phase distinction.

Alternatively, we might sacrifice the phase distinction completely and treat types more like assertions, and possibly attempt to recover some static checking through, for example, partial evaluation. The problem with this approach is that it's hard for the programmer to understand and predict what guarantees the compiler can make about a particular program, and what checks will need to be deferred until run-time. The partial evaluation techniques required are also an active area of research.

This is only my own off-the-cuff survey of the state of the art here, and I'm sure there are omissions and mistakes. I hope someone more knowledgeable will correct them.

You got it backwards, actually.

Having a phase separation means that you never need to evaluate a program term in order to decide whether a program is well-typed.

If the language lacks a phase distinction, then typechecking may require evaluating some program expressions at compile-time. For example, consider a program (in a made up language) like:

(* This is a program *) 

fact :: Nat -> Nat

fact 0     = 1
fact n + 1 = (n + 1) * fact(n)  

(* This is a type declaration that uses the fact function. 
If fact of the argument is large, it returns a string, and 
if it's small it returns a boolean. *)

foo :: m:Nat -> (if fact(m) > 1000 then String else Bool)

foo n = 
  if fact(n) > 1000 then 
    "a string" 
  else 
    true

But running the program at run time still might not require keeping any type information around.

I thought that was what I meant to say, unless I'm misunderstanding you. Thanks for the clarification and example!