Lambda the Ultimate

No actually, conjunctive type != polymorphic variant though they are related.
After reading some of the paper I linked above, it's clear that a conjunctive type "e: s & t" means that e could be an s or a t but we're not making a commitment as to which one yet. So it's a way of approximating types (ie. "we don't know the type exactly but we do know that it will be one of these ..."). In any concrete program, type inferencing will eventually narrow the type down to a specific case.

After reading some of the paper I linked above, it's clear that a conjunctive type "e: s & t" means that e could be an s or a t but we're not making a commitment as to which one yet.

Not sure, why leemarks changed his guess from intersection types to polymorphic variants? Am I missing something obvious?

I agree with Andris that this looks very much like intersection types. A lot of important research that you'll want to look at is at the FLINT project page. Also ask Google about refinement types which are related and fairly cool themselves.

Incidentally, I believe Philip Wadler said once that John Reynolds tends to be about 10 years ahead of time in research. This is yet another example; one of the earlier examples of intersection types was in a language called Forsythe, that you also should look at.

I was under the impression that an intersection type contained only those features of both its component types that they had in common, instead of literally being both types at once -- is this wrong?

Treating types as sets of values (naively) the intersection type is the intersection of the sets. I.e. it's values are the values of that are both types. So, yes, an element of a /\ b is an element of a and an element of b.

[on edit: fixed a bug, so the statement was not trivial afterall]

I was thinking, if something like the following were legal:

name :: T -> String
name :: V -> Name

first :: Name -> String
middle :: Name -> Char
last :: Name -> String

then you'd have
name :: T & V
and
first . name :: V -> String
and
putStr . name :: T -> IO ()

(As in the dual of intersection types)
So it would make more sense to say T | V rather than T & V. But regardless of the syntax, as you've illustrated, inferencing narrows the type based on usage constraints.

I don't see why this couldn't work but I do see one problem:
If I were to add a third name function, eg:

name :: X -> Name

then the typing of first . name would change to (X | V) -> String
I believe the fact that merely adding a new function can cause the types of previously existing functions to change shows the system lacks principal types.

Ok please don't shoot me for such an ultra-newbie question, but, so long as it doesn't invalidate other code-paths, why would not having principal types be a bad thing? At the risk of sounding like a troll, why do you care what the principal type is so long as the type you express works?

All implementations of type inferencing I've seen rely on either prinicpal types (or the related idea of principal typings). I guess there are reasons why that's the case but I'm not sufficiently clued up to really know why.
But I agree, if you can make it work, that would be great.

why do you care what the principal type is so long as the type you express works?

Both papers are more focused on "why principal typings", but you can find also arguments for "why principal typings".

I still suggest reading the papers I mentioned, as my interpretation might be quite wrong.

Simplifying Andris Birkmanis's remarks further: A principal type is the most general type that properly captures the type of the expression (in the given type system). Thus, in a nutshell, not having principal types means you need to make an arbitrary decision/cutoff. I should not have to spell out why this is less than desirable.

Meta note: Attempting to post this reply, I get "terminated request because of suspicious input data". After a bit of experimenting, apparently from writing expression followed by parentheses (which I got around with <span>). A more informative error message or less restrictive filter would probably be helpful.

I was thinking, if something like the following were legal:

{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}

module J where

import Prelude hiding (last)

data Name = Name{first :: String, middle :: Char, last :: String}

data T = T
data V = V

class Naming f t | t -> f where
    name :: f -> t

instance Naming T String where
    name _ = "Name of T"

instance Naming V Name where
    name _ = Name{first="V1", middle = 'X', last = "VLast"}

f1 = first . name
f2 = putStr . name

We can check that the inferred type for f1 and f2

*J> :t f1
f1 :: V -> String
*J> :t f2
f2 :: T -> IO ()

This also gets around the principal type issue I mentioned above by requiring that each instance of the name function target a unique type. So we allow overlaps on the domain but require disjointness on the codomain.

My Haskell isn't that strong: what is the purpose of the "| t -> f" in the Naming class?

See the Haskell Wiki: FunDeps along with
Fun with Functional Dependencies

Exactly like with OCaml's polymorphic variants:

# let f = function `Orange n -> (string_of_int n)^" oranges" | `Apple -> "some apples" ;;
val f : [< `Apple | `Orange of int ] -> string = <fun>
# let g = function `Orange s -> s^" oranges" | `Apple -> "apples" ;;
val g : [< `Apple | `Orange of string ] -> string = <fun>
# let h x = f x, g x ;;
val h : [> `Apple | `Orange of string & int ] -> string * string = <fun>

Sorry. Done.

int and string are disjoint so interpreting that as an intersection didn't seem right.

I suspect that if we are only interested in how they walk and quack, they don't need to be disjoint. In fact, even structural typing is not necessary: e.g., if Integer and String were interfaces in Java (instead of final classes), then it would be possible to have a class implementing them both.