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 :)

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...

By marco at Sat, 2004-12-18 16:23 | login or register to post comments

Don't understand your comment.

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...

By ihamsa at Sat, 2004-12-18 20:55 | login or register to post comments

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 ;-)

By marco at Sat, 2004-12-18 22:01 | login or register to post comments

This seems relevant

SYSTEM CT: Constrained Types for Overloading.
It's an extension to HM type inference supporting overloaded definitions.

By Daniel Yokomizo at Sat, 2004-12-18 17:02 | login or register to post comments

The larch

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

By marco at Sat, 2004-12-18 18:35 | login or register to post comments

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?

By ihamsa at Sat, 2004-12-18 21:00 | login or register to post comments

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.

By fab13n at Sun, 2004-12-19 01:46 | login or register to post comments

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/
http://homepages.cwi.nl/~ralf/OOHaskell/

Ralf

By rlaemmel at Wed, 2004-12-22 15:20 | login or register to post comments

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?

By ihamsa at Fri, 2004-12-24 08:25 | login or register to post comments

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.

By rlaemmel at Sat, 2005-01-01 17:17 | login or register to post comments

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...

By ihamsa at Mon, 2005-01-03 13:19 | login or register to post comments

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:

http://homepages.cwi.nl/~ralf/OOHaskell/src/List.hs

That is, if you want to make type distinctions, you can just use good old newtypes as in normal Haskell. Accidentally, you need such nominal classes in case you are facing recursive classes. (That's indeed the point of the linked example.) This is because Haskell does not have recursive types. Of course, we can easily encode iso-recursive types, as exercised in the example. BTW, we probably don't want plain recursive types in Haskell (as defended by Hughes, as referred to in the paper).

Making type distinctions implies some coding efforts. That is, one needs to perform injections/projections at times. However, it is not difficult to hide this. Most notably, projections can be hidden by a silly instance for the Hash operation ("#"); see the example. One could again argue that this instance should be provided as part of a syntactic sugar extension.

(Eventually, the narrow operation, which encodes OOHaskell's subtyping would need to be extended to
perform injections and projections as well, at times.
The narrow operation in the current source distribution is very _simple_ anyhow, but see the CovariantReturn.hs example for an illustrative sophistication. It should be clear that narrow can peel off nominal tags just as the special narrow in the example is readily aware of "->".)

Ralf

(P.S.: Yes, we will provide more details on the unfinished TwoTable stuff soon. This is just _yet another_ approach.)

By rlaemmel at Tue, 2005-01-18 18:04 | login or register to post comments

Lambda the Ultimate

User login

Navigation