## HM-style type inference with non-unique selectors?

I figure this is the best place to squeeze my question in, so here goes.

A selector is either data constructor or a record field. In HM-style languages those are largely required to have unique names across entire program. Is there any way to lift this requirement and still have (partial) type inference? The hypothesis here is that unresolvable name clashes should be rare. When they do occur, the programmer should give an explicit type annotation.

Consider this:

data D1 = Foo Int | Bar Double
data D2 = Foo | Baz -- name clash, but not fatal yet

f1 (Foo x) = x
f1 (Bar y) = round y
f2 Foo = "Foo"
f2 Baz = "Baz"
-- The inference algorithm should be able to figure out the type for f1 and f2
-- f1 :: D1 -> Int
-- f2 :: D2 -> [Char]

f3 (Foo x) = x
f3 _ = 42
f4 Foo = "Foo"
f4 _ = "Error"
-- Still should be possible to figure out types for f3 and f4, because
-- Foo in D1 and Foo in D2 have different arities
-- f3 :: D1 -> Int
-- f4 :: D2 -> [Char]

f5 = Foo
-- ambiguity: Int->D1 or D2?
-- the compiler should signal an error

Is there an inference algorithm that does just that? If such questions are inappropriate for this forum, please feel free to delete my account and ban my IP :)

## Comment viewing options

### Don't understand the problem

Does HM not apply because two different proofs of type correctness in HM give rise to ambiguity? (i.e. two different unifications proof ambiguity?)

I mean, that is a known pitfall of type theory, right?

Or is it because the language implementors were just lazy?

Hmm, just trying to grasp the problem here...

Do you mean that the inferencer should simply eliminate tuping assumptions (I hope this is the right term) for which unification fails, and report ambiguity if some term remains with more than one type? I'm sorry if this sounds stupid, my type theory is severily lacking...

### Relax, we understand j00

Well, your comment sounds like a solution what I thought of from the top of my head. I guess that during identification you could add a constraint type_of_Foo == (Int->D1 | D2) and check whether all terms have unique types after inferencing.

Don't know about time and space requirements of such an inferencer though; but if it is impossible to derive a unique type in time you can always blame the programmer ;-)

### This seems relevant

It's an extension to HM type inference supporting overloaded definitions.

### The larch

Ah well, for something completely different, Constraint Based Type Inferencing in Helium

### Thanks, I'll look at it.

Though it seems to me that System CT would just give f5 a constrained type (same as Foo), whereas I want it reported as ambiguous. Hm, maybe all terms with constrained types (except the selectors themselves) should be reported as ambiguous?

### Still better, you might consi

Still better, you might consider:

- open variants, from Garrigue, included in Ocaml>2.99 Basically, you can compose your sum types atomically.

For instance, this has type [B of 'a] -> 'a:

function B x -> x

You can declare partially overlapping types, e.g.:

type t0 = [A | B of int] and t1 = [C | B of int] and t2 = [`B of string]

The type system allows fancy stuff like upper-bounds [< ...], lower bounds [> ...] and combinations [<...>...]... This is quite an impressive job, very handy, although so much agility has a price: principal types are usually much more complex and less readable than intended types, so you tend to put much more type annotions although they are generaly not mandatory, esp. when you try to spot a typing error.

- the corresponding stuff for record is based on row variables (check Didier Remy's papers). Objects in Ocaml are based on this theory, although they are not as handy as records IMHO.

### HM + multi-parameter classes with fundeps

I know that your question seems to focus on Hindley/Milner, but your code reminds me of Haskell, which makes me wonder whether you are also interested in solutions that involve some of the extensions that Haskell has to offer, and if this is the case, then I would like to mention that you can get first-class labels (that are reusable and all that) once you combine HM + multi-parameter classes + functional dependencies.

Since this is perhaps not obvious, let me shamelessly plug one or two links:

http://homepages.cwi.nl/~ralf/HList/

Ralf

### Most interesting, thanks!

If I understand these papers correctly, you implement extensible records similar to TREX where type equivalence and subtyping are structural. I'm more interested in name equivalence. Though OOHaskell is fascinating. You mention an upcoming paper where you separate instance variables and methods in two different tables; is that available somewhere?

### OOHaskell vs. TREX and structural vs. nominal type equivalence

Thanks for the comment and the questions.

Let me emphasise that the comparison with TREX should not be taken to mean that we provide any language extension. By contrast, we exploit the existing type system.

As for name equivalence, the type-level type equality functions and friends (e.g., type case or cast) ... in fact they *do* implement nominal equivalence. You are right that at least the Subtype predicate is really defined structurally (because we basically perform a projection feasibility test). But given the fact that we have nominal type equivalence as well, it is clear that we could constrain subtyping by extra nominal tests again. We shall illustrate that in a next version. If you have any benchmark in mind that you would like to see covered, please let us know.

Regarding your question about separation of instance variables and methods in two different tables ... the source code distribution contains a sketchy example doing this, but we shall put more work into the description of these ideas. We expect to work out a full journal version of the paper in the foreseable future, or perhaps an extra paper on functional objects.

### I understand the difference.

As for nominal vs structural (in)equivalence, my understanding is that type inference relies on the latter. E.g. in a program fragment like p # foo the type of p is "a record that has a field named foo", howewer it is expressed in the language. If field labels are reusable, I don't see how it's possible to go from here to name (in)equivalence.

I've looked at TwoTables.hs and it doesn't seem finished, the interesting parts are commented out and uncommenting them causes errors. I'll try to come up with an example of my own when I have time for that, sigh...

### nominal vs. structural

I am not sure that I completely understand your line of arguments. Let me just mention that there is no problem with introducing nominal types into our system. Here is a helpful example, perhaps: