Lambda the Ultimate

It seems to me that Haskell imitates subtyping for numeric types by implicitly passing number literals to the coercion functions fromInteger or fromRational. Is it possible to give subtyping and overloading a more elegant/complete way to coexist?

If I understood Haskell semantics right all number literals are instances of a type class (Num probably). Can't you give an example of what you found and what you want?

[I forgot to mention the "Typing Haskell in Haskell" paper by Jones. You might want to read that if you're interested in Haskell's type system.]

[You might want to notice that Haskell's type classes are different from, say Miranda-like, overloading. Overloading implies that type information is used to pick the right function from a collection of functions with the same name. The type class mechanism instantiates a well-known member of a class with a specific function. Water and whiskey are both fluids, but they are not the same (or solutions to the same problems).]

If, for example, the literal "1" has type int, what needs to be added to an ML-like type system so that "1 + 0.3" will be typed as a float?

If I assume a system without subtyping, then the simplest solution would be overloading (or overloading on type class members). (Which is hairy, since you'll end up with two options: A. Always determine the right + operator at compile-time (statically), and disallow the use of + in general definitions. Or, B., allow binding at run-time and live with the fact that sometimes there is no definition to be found for a specific +.)

Haskell's type classes allow some restricted form of subtyping on the classes so that expression will probably be in the real-number type class, which actually is something different than having type float.

To really type that expression [correctly] as having type float, and to allow different implementations for + [to always be typed correctly], you'll need subtyping on the type level and overloading. There is no easy fix, as far as I know.

[BTW: I don't really use all features of ML, so I'll leave signatures out of the solution space (that's in ML, right?).]

Section 6.4.1 of the Haskell Report states that numeric literals are passed through fromInteger or fromRational automatically. That allows code like the following to type-check:

Prelude> 1 + 2.5
3.5

Whereas the following won't (on interactive prompt anyway):

Prelude> let x = 1
Prelude> let y = 2.5
Prelude> x + y
<interactive>:1:4:
    Couldn't match expected type `Integer'
           against inferred type `Double'
    In the second argument of `(+)', namely `y'
    In the expression: x + y
    In the definition of `it': it = x + y

Good, so I fired up ghci too.

GHCi, version 6.8.2: http://www.haskell.org/ghc/  :? for help
Loading package base ... linking ... done.
Prelude> let x = 1
Prelude> let y = 2.5
Prelude> :type 1
1 :: (Num t) => t
Prelude> :type 2.5
2.5 :: (Fractional t) => t
Prelude> :type x
x :: Integer
Prelude> :type y
y :: Double
Prelude> :type 1 + 2.5
1 + 2.5 :: (Fractional t) => t
Prelude> :type x + 2.5

:1:4:
    No instance for (Fractional Integer)
      arising from the literal `2.5' at :1:4-6
    Possible fix: add an instance declaration for (Fractional Integer)
    In the second argument of `(+)', namely `2.5'
Prelude> 

I see your point. Hmpf, it's a feature, not a bug?

[There is no + to add an integer and a float. So my best guess is that ghci inserts (widening) coercions for literals when typechecking. Why it wouldn't do that for variables I don't understand.]

[Forget it, I don't get Haskell here. Both x and y are in class Num, but x and y have different types. 1 + 2.5 shouldn't type-check.]

In the first unification problem, the goal is to find a type [a] so that [Num a] (for the 1), [Num a] (for the (+)) and [Fractional a] (for 2.5). Such constraints reduce to a single constraint [Fractional a] resulting in the type of [1 + 2.5], and both literals are injected into the same type [a]. In the second case [a] is instantiated to [Integer] because of the type of x. The constraints are then [Num Integer] for (+) whish is solvable and [Fractional Integer] for 2.5 which isn't.

Dude, I get the type derivations. You're injection is actually a widening coercion so we agree. It remains weird though.

Is there anything wrong with the derivations then? Maybe that's just the monomorphism restriction that's bugging you as Andreas point out?

In the first unification problem, the goal is to find a type [a] so that [Num a] (for the 1), [Num a] (for the (+)) and [Fractional a] (for 2.5). Such constraints reduce to a single constraint [Fractional a] resulting in the type of [1 + 2.5], and both literals are injected into the same type [a]. In the second case [a] is instantiated to [Integer] because of the type of x. The constraints are then [Num Integer] for (+) whish is solvable and [Fractional Integer] for 2.5 which isn't.

Is there anything wrong with the derivations then?

Well, I am not sure, but the first derivation is wrong I think. Both 'alpha-s' [for the literals] are [or should be?] universally quantified, they should introduce skolem constants and then fail on the equality of (+) which has type 'a -> a -> a', as far as I understand it.

The second derivation is correct, and fails therefore.

Maybe that's just the monomorphism restriction that's bugging you as Andreas point out?

I don't understand the monomorphism restriction. As far as I know it is a hack in ML. I don't think Haskell has the monomorphism restriction. [I didn't read the post below, so Haskell has the monomorphism restriction. Will maybe respond on that.]

The only way I can understand the typing here is if, somehow, magically, unknowns are introduced [in the types] for literals, and the unification ends up into coercing the literal 1 to type float.

[Hmpf, sadly, I think I now found a bug in my own type-system ;=(]

[There is no bug ;-)]

You seem to be confusing Haskell's "monomorphism restriction" with SML's "value restriction." They're different, and exist for different reasons. Luckily, the monomorphism restriction is a bit easier to understand than the value restriction, IMHO.

SML's value restriction arises because of the impurity of the language (see here, for example, for details).

Haskell's monomorphism restriction exists basically to avoid surprising the programmer by doing more evaluation than is apparently needed. The example in this thread actually shows that nicely: when we turn off the monomorphism restriction, a value like:

let x = 3

will turn into an expression like fromInteger 3 which, instead of being evaluated just once (as the source code implies), will be evaluated potentially many times, depending on which instance of Num is finally required.

I hope that very terse explanation helps more than it hurts... Better information, of course, is available elsewhere.

Whether it's fair to call either of them a "hack," I won't say.

You seem to be confusing Haskell's "monomorphism restriction" with SML's "value restriction." They're different, and exist for different reasons. Luckily, the monomorphism restriction is a bit easier to understand than the value restriction, IMHO.

True, thanks for pointing that out.

Haskell's monomorphism restriction exists basically to avoid surprising the programmer by doing more evaluation than is apparently needed. The example in this thread actually shows that nicely: when we turn off the monomorphism restriction, a value like:

will turn into an expression like fromInteger 3 which, instead of being evaluated just once (as the source code implies), will be evaluated potentially many times, depending on which instance of Num is finally required.

Ok, I am starting to see what is going on here. But the added conversion is still no 'real' reason to add this restriction. I would suppose a 'cleaner' semantics would be if it would reduce the argument once, and the conversion multiple times. That's weird also [from an operational perspective], but at least the programmer wouldn't be bothered with this restriction.

[Ok, don't bother. I can see it might? not work if it doesn't only involve coercions, but also functions which get passed type dictionaries. See the examples in the posts below.]

Coercions require dictionaries too. I can add a new Num instance for any new type at any time, so "fromInteger" can't be assumed to be a "simple" coercion.

Matt: ... Haskell's "monomorphism restriction" with SML's "value restriction." They're different, and exist for different reasons. Luckily, the monomorphism restriction is a bit easier to understand than the value restriction, IMHO.

They exist for different reasons, but actually, they are not different at all. The MR basically is just a relaxed version of the VR. In fact, that makes it (slightly) more complicated:

VR = any definition that is not syntactically binding a value can never be polymorphic

MR = any definition that is not syntactically a function binding can only be polymorphic if it needs no constraint

(The precise form of the syntactic condition is rather secondary, the meat is in the form of polymorphism disallowed.)

Good point. I never thought about it too hard, and I guess I was distracted by the addition of type classes and the different "precise form of the syntactic condition." Thanks!

It's not an implicit coercion, rather it's a desugaring. No type information is needed to expand it, though of course type information is eventually needed to resolve the expansion.

Haskell completely lacks a notion of subtyping.

However, to answer the original poster's question: adding subtyping to polymorphic lambda calculi is well studied. In particular Luca Cardelli's (earlier) work is the place to look, and in particular from that the work on System F_sub. Type classes can be elaborated into System F, they can at least be put side-by-side.

Cardelli looks like a good starting point, thanks. It's unfortunate that every time I have a basic P/L question I end up adding 4 or 5 new papers to my Should-Read stack.

Actually, there is a bit more going on here. In Haskell, literals are polymorphic ("overloaded"). Consequently, the bindings x and y should be polymorphic too, which would make x+y well-typed. But unfortunately, the dreaded monomorphism restriction kicks in here.

However, you can disable it by giving explicit type annotations for the bindings:

Prelude> let x :: Num a => a; x = 1
Prelude> :t x
x :: (Num a) => a
Prelude> let y :: Fractional a => a; y = 2.5
Prelude> x + y
3.5

Edit: In fact, you can make the result polymorphic, too:

Prelude> let z :: Fractional a => a; z = x + y
Prelude> :t z
z :: (Fractional a) => a
Prelude> z :: Float
3.5
Prelude> z :: Rational
7%2

Prelude> :set -fno-monomorphism-restriction
Prelude> let x = 1
Prelude> let y = 2.5
Prelude> x + y
3.5
Prelude> let z = x + y
Prelude> z :: Double
3.5
Prelude> z :: Rational
7%2

I notice that this only seems to be a problem in certain situations. E.g., the following works fine:

Prelude> let x = 1 in let y = 2.5 in x + y
3.5

In the original case, isn't referential transparency violated to some extent? I.e., I cannot freely replace 1 with x as they have different interpretations/types. Getting back to nearer the OP's original question: are there languages that lift the monomorphism restriction?

[Edit: Ah, I see Matt Hellige answered my question.]

They don't generalize the types of x and y here? I don't get it.

In "let x = 1; y = 2.5 in x + y" the compiler has enough information to infer the type of x and y to be equal.
In "let x = 1", if the monomorphism restriction is active, x must be given a single type and we don't have much information on its future use... That's when "defaulting" kicks in : as x is an integral literal, it will be given the Integer type (or Int if the default is changed beforehand).

If you deactivate the monomorphism restriction, the behaviour is a little bit more regular as x has type "(Num a) => a" and can be used wherever 1 can.

It is true that Haskell does this, but in BitC we used what are basically Haskell mechanisms to avoid this. We initially type integer literals as being of type 'a\(IntLit 'a), where IntLit is a type class containing all of the integral types that have literals. In fact, we can even get this right in the presence of mutation, assigning a value-restricted type when required. The mutability support, clearly, goes beyond Haskell. All I'm trying to say here is that there do exist other approaches to this sort of problem.

As far as I can tell, Num and IntLit are pretty much equivalent in that regard - the problem in Haskell, as is often the case, is the monomorphism restriction. There was no small amount of discussion about getting rid of it in Haskell'!

God, I guess the assumption is that you can check the unique occurrence of a term by checking the unique occurrence of its corresponding type in a type table. It's a hack, I think, they should check on the unique occurrence of a term...

[It seems I wrote over my own post, somehow?? The original post:]

    An example, from A History of Haskell: Consider the genericLength function, from Data.List 

    genericLength :: Num a => [b] -> a

    And consider the function: 

f xs = (len,len)
     where
       len = genericLength xs

    len has type Num a => a and, without the monomorphism restriction, it could be computed twice. --ARG 

I failed to see what types have to do with the operational semantics.

Clearly len has to be recomputed if it occurs at two different types. If f xs :: (Int, Double), you're certainly not going to be able to use the same value for both.

An easy way to see this is to insert the implicit type lambdas which will turn genericLength xs into a function, namely Λa.genericLength{a} xs which implies recomputation just like a value-level lambda would.

Nothing about types makes them inherently unrelated to the semantics. Type classes are an extreme example of semantics depending on types.

Clearly len has to be recomputed if it occurs at two different types.

Why? [To elaborate, under graph rewrite semantics, len is a node, and if it reduces, it's reduction will be placed in the tuple (whether those parts of a tuple will receive different, or even the same types, is irrelevant, IMHO). ]

Well let me use more accurate language, it is genericLength xs that needs to be recomputed, len is still shared as normal, but it's effectively holding a function. Each different type is a different application of that function. For genericLength xs, if the result of that expression is shared then it has only one value. It's either an Int or a Double (or an Integer or an ExpressionTree or a Complex CReal or a NumMod4 or...). It can't be all of these things at the same time.

The type of f, if no signature is given, then the compiler doesn't
know that the two elements of the returned pair are of the same type.
It's return value will be:

f::(Num a, Num b) => [x] -> (a, b)

Yeah, yeah. 'len' gets a type, that type is generalized [once, and instantiated twice], and therefore, f will be passed two type dictionaries, and len will [make that: might?] be executed twice. (Still, it is obvious from the example that len will be executed once.)

Hmpf [ Hehe, my language doesn't have this restriction. I made sure the operational semantics are orthogonal to the type system, so I never ran into this problem. ;-) (Actually, I made sure it also compiles without type-checking.)]

[I guess, under the hood, len is copied twice in the tuple.]

[Hmpf, I knew this. That's one reason I stayed away from type-classes Haskell style. I forget as easily as I learn. Ah well.]

marco: [I guess, under the hood, len is copied twice in the tuple.]

Unless the compiler does whole program compilation, again no. What Derek was getting at is that somebody might call this function, in another module, as follows:

data Weird = Weird Int

instance Num Weird where
  Weird n + Weird m = Weird (n * m `mod`  666)

p = f [3,4,5] :: (Int, Weird)

So clearly, len has to be evaluated twice, because the two evaluations potentially do entirely different things for different types.

When someone says 'clearly' in a proof, you normally assume that it is a statement the person found no proof for, but found it evident that it must be true. [And, then, normally, it ain't.]

... I assume the same is going on here ...

What, according to you, is the result of that statement? [Notice, that I am not saying the monomorphism restriction doesn't hold in Haskell. I just fail to see why it should.]

I guess the assumption is that you can check the unique occurrence of a term by checking the unique occurrence of its corresponding type [...].

I am sorry, it just depends on whether you want the above to hold in a language. I find the monomorphism restriction weird. The terms should be leading, not the types. I.e., two different types don't imply two different terms.

...that's what it is all about. The MR does not change the situation either way.

Pretty sarcastic. I'm not sure what your question is either. Are you asking what the value of p would be? The example does not make a hell lot of sense, but assuming you add the canonical definition for fromInteger, it'd be (3, Weird 0). Clearly even. ;-) For slightly more pepper, define fromInteger n = Weird (n + 5), and you'll probably get (3, Weird 414).

...

Yeah, you were right ;-). Or were you?

This result would actually be equally ok: (3, Weird 3). It depends on where you place the coercion.

[I would assume it should be placed in the tuple [given the structure of the term], but then, of course, that would be strange too, since you wouldn't know what type to give 'len'.]

Weirdness.

[Btw. It wasn't sarcasm ;-). I found it to be true in a large number of places.]

[Sorry for the heavy editing]

That result wouldn't be OK. There is no coercion. I think you are misunderstanding the semantics of Haskell.

[Sorry for the heavy editing]

Not to get too off-topic, but since you mentioned it... I find that the heavy after-the-fact editing makes your posts hard to read and hard to understand, and also makes the overall discussion very difficult to follow. I can't state it as a matter of policy, and I'm sorry if it offends you, but I do encourage you to stop editing your posts so much.

Will do. Lost the preview button ;-)

The monomorphism restriction is not something that "holds" or "doesn't hold" of a language. It's a restriction placed upon the language. In the case of Haskell, there is no logical necessity for the monomorphism restriction. It is there by fiat of the Report (though most implementations allow you to turn it off and NHC never even implemented it.)

To underscore what Andreas has said elsewhere. There are no implicit coercions in Haskell at all. There is not even any language-recognized notion of coercion, so there aren't even explicit coercions. Haskell will never, ever implicitly turn a value from one type into a value of another. This is related to my earlier comment that Haskell completely lacks subtyping. Without a subtyping relationship the language has no way of knowing which types are safely convertible to others, let alone knowing a canonical choice of conversion.

Finally, even subtyping doesn't change the picture here. There is no guarantee that one of the two types for len is a subtype of the other, so again, it would be impossible to insert coercions even if we had them.

To be a bit more formal, there is nothing at all that requires that fromInteger . genericLength = genericLength, so it is not safe to calculate once and then just apply fromInteger to get different values, and anyway, there is no requirement that fromInteger be total or injective, the latter, at least, is something that you would want for a coercion.

Or rather, I found it counter-intuitive, and I still find it counter-intuitive. And I don't like that in a language. It's okay that pretty smart people understand it directly, but I want a semantics which pretty stupid people understand directly.

The monomorphism restriction is there to fix a problem, I understand that.

Haskell will never, ever implicitly turn a value from one type into a value of another.

Except for literals, which was where I got side-tracked. (I never programmed in Haskell a lot)

I don't like it though. I know type-classes are a pretty good feature to have. I know (knew, I guess) of the down-sides: (1) was that unless the restriction is set, you're stuck with multiple evaluations, (2) sometimes it isn't obvious from the source code what type-class will be instantiated, so sometimes you get strange behavior from inauspicious code. (This is why I chose another implementation. I never had this experience in Haskell myself.)

I find it counter-intuitive that in the addition example the types of the literals even unify. Given the explanation, and the types given for the literals, I even find it more counter-intuitive that the (+) for the 'float' type (or arguments) is instantiated; why not 'int'? Why is the result in the Fractional class, when only one of the arguments lives in it? Or should I assume they both live in the same type? I see no reason from the example to choose one above the other. I find it a mess.

(Pleasy note that the 'why'-s above should be read retorically. I am not asking what types they have; for that I can start Haskell. I am troubled by those design decisions.)

I am starting to like the type-class mechanism of Haskell less and less. Choosing a semantics which acts like what programmers expect, except in corner cases, is just not how a language should be build.

(Or I am a complete idiot, who fails to grok easy semantics. Which might be true in any case ;=) )

The type of, say, 1 + 0.4 is (Num a, Fractional a) => a or, equivalently, just (Fractional a) => a since Fractional implies Num. If you write: print (1 + 0.4) you should get an ambiguous class constraint error because it shouldn't know which instance of Fractional to use. You don't get an error however due to a completely ad-hoc hack in Haskell that is completely unrelated to the core notion of type classes. This hack is defaulting. Basically, Haskell 98 specifies that if an ambiguous class constraint case comes up, and it involves only standard classes, then a list of types, specified in a default declaration, should be tried in order until the expression type checks (or you run out of types). The default default list is Integer, Double.

So in the above example: print (1 + 0.4) you have the ambiguous class constraint (Show a, Fractional a) => IO (). If you have not specified otherwise, Haskell will try Integer (which fails the Fractional constraint, unless you are evil) and then will try Double which type checks.

Yeah, I know of the defaulting rule but failed to see it applied here.

Dunno, I guess these are all design decisions one can make (like defaulting an unknown kind to *), but, nah, it really bugs me.

What if you change the defaulting rule or add a class, do the semantics of other modules change then too?? Can I default addition to type 'Weird'?

Of course, you never know how a rule like that turns out unless you try it in a language, and I guess this is what a research project like Haskell is all about. But, hmm, predictability is really important in a language, that is one lesson learned from many languages.

[Of course, it's not like I don't make many mistakes. Like my language has a O(n^2) type checker. O(n^2) algorithms are strictly forbidden in GCC, and well, I found out why the hard way ;-).]

[Ah well, I guess it's just Haskell and probably it's not a biggy and just works for them.]

[BTW: I/we did it again. I understand the type derivations. I just find it rather strange that, for example, the numeric literals are not universally quantified, as one would expect.]

Defaulting's local to the module it's defined in. No worries there. And numeric literals /are/ universally quantified initially - the monomorphism restriction and the defaulting rule can affect that, though.

When in doubt, read the report - it didn't take me long to confirm that defaulting's strictly module-local just now, and I'm not especially familiar with it.

Hmm, yeah, one can default skolem constants under certain assumptions, but, I'll take your advise and read the report on whether they do that ;-).

(Allthough I have to admit I don't like to read language reports because of expedient language decisions ;-). But I will also gladly admit I am no where as smart as Peyton-Jones or Wadler.)

[There is, of course, also the matter of what intuition exactly is. Maybe what is counter-intuitive to me is normal to a lot of Haskell users.]

Tsss, after some trauma, some bad medication, and subsequent more trauma it seems I have now an IQ of 13 +/- 2.

Today is a good day, I think it is +3 ;-).

I was thinking HOL, not type theory, on the addition example and forgot that normally in type-theory the meaning of the modalities seem to be reversed. (The existentials introduce the skolem constants.)

So I expected existential quantification because in other languages the types of the literals would be known, then hidden. [Or rather, if you hide a known type, it should introduce an existential]

I find it counter-intuitive that in the addition example the types of the literals even unify. Given the explanation, and the types given for the literals, I even find it more counter-intuitive that the (+) for the 'float' type (or arguments) is instantiated; why not 'int'? Why is the result in the Fractional class, when only one of the arguments lives in it? Or should I assume they both live in the same type? I see no reason from the example to choose one above the other. I find it a mess.

Type inference is all about finding the most general type that works for a given term, here I fail to see how it is unintuitive that Fractional is chosen since 1 can be a Fractional (without loss) whereas 2.5 obviously can't be an Integral (or only with a lossy conversion). Then the fact that Double is chosen rather than Rational or Float is due to the defaulting mechanism (which might be more controversial but is still what one mostly wish in this situation and can easily be overridden).

Look at the options for the literal '2.5'.

1. You can give it type 'float'.
2. You can give it type 'Exists t. Rational t => t'
3. You can give it type 'Forall t. Rational t => t'

(1) Is the most straightforward, (2) is already a bit strange, but ok, you abstract from the real type and introduce an unknown constant for that, (3) well, it unifies with any other Rational type. [..?]

I think 3 is the most straightforward because
looking a 2.5, all the information you have is that it is a value in any possible fractional type (the typing constraints might force it then or some other rules).
If you had 2.5f (or 2.5 :: Float) then 1 applies.
2) Existential generalization just seems like a weird idea :) In the term 2.5 + 1 you would have to unpack things automatically? Has it been implemented in any language?

Implicit generalization has its problems, esp. with type classes, as you have to run HM in your head.

looking a 2.5, all the information you have is that it is a value in any possible fractional type (the typing constraints might force it then or some other rules).

I like it when a literal exposes its type and I don't like it when you need to guess the type from the environment. That's just me I guess.

If you had 2.5f (or 2.5 :: Float) then 1 applies.

Yeah, that's what I mean. [When I read '2.5' I assume it is a 'float']

2) Existential generalization just seems like a weird idea :) In the term 2.5 + 1 you would have to unpack things automatically? Has it been implemented in any language?

'2.5 + 1' wouldn't type-check unless through overloading [on classes]. Note that it is Haskell which packs/unpacks literals into different types through the injection mechanism.

Implicit generalization has its problems, esp. with type classes, as you have to run HM in your head.

Good point, so we agree? ;-) Programs are not always enjoyable puzzles. A lot of programs just need to be clean and easily readable. Running HM through your head is not an option for a lot of languages. [Or rather, I don't like it in a modern language.]

[Another note: one thing I noticed from writing a language. You can be clever, but you can't be smart ;=). In the sense that straightforward smart solutions (generalizing and trivializing) are most of the time good ideas; any other smart solution usually backfires.]

'2.5 + 1' wouldn't type-check unless through overloading [on classes]. Note that it is Haskell which packs/unpacks literals into different types through the injection mechanism.

It does no such thing: there's no existential type involved, just a fromInteger/fromRational for each literal. Nor will Haskell do any automatic conversions for you. Pack and unpack mean specific things, no?

Packing was a misnomer, I agree.

I think we're getting a little confused between metavariables and variables here. Your typical Haskell implementation doesn't have a forall around the type of 2.5 when it first encounters it: it's a monotype, and t is a metavariable. It only gets the forall if t isn't constrained to a single monotype.

I'd consider option 2 plain silly, because 2.5 + 3.5 couldn't type. Unless what you mean by the existential is something like the metavariables which are existentially quantified but aren't part of the language itself as opposed to the typechecker.

FWIW, I consider this something of a wart in presentations of Hindley-Milner-style inference that don't make the distinction: life is much, much easier with it.

For something trivial. Now we can explain to silly programmers: monotypes, metavariables, monomorphism restrictions, defaulting and injections. (Anything I forgot?)

All that to type 1 + 2.5?

I agree that option 2 is silly and shouldn't type check. But I think it is the most natural next choice for the type of '2.5', hiding the real type 'float'.

Thankfully it's a little easier than that: the injections aren't relevant to the typing at all. That leaves you with monotypes, metavariables, defaulting and the MR.

The funny thing there is that you need monotypes and metavariables to cover hindley-milner inference at all - and so long as you use words like 'thingy', an awful lot of people already get the idea of metavariables. Which makes defaulting pretty easy: sometimes (like when you're typing into a REPL) you need to know which thingy the thingy is in order to run something, so if you don't specify then it'll guess.

The MR's the odd one out, and it's a major wart. But if you can explain it at all, remembering to point out that it'll force defaulting isn't such a big deal. It also doesn't apply in typing 1 + 2.5.

What doesn't work is trying to cobble a bunch of stuff together: you're getting confused because you're not piecing together a single coherent presentation of the type system, so every new piece makes makes you WTF spectacularly because you never had a sound understanding of any of the others.

As for your most natural next choice, it sounds like you have a pretty big problem with Hindley-Milner as a whole rather than just Haskell and type classes (consider typing map id). That, or you're too busy trying to map type classes onto OO classes and end up with an existential that way? And if you don't get the most fundamental parts of the type system, it's not surprising that you can't make sense of the rest.

God no, the type system I have for my language is a pretty straightforward simplification of Haskell type classes, it seems to do just fine. I am not trying to invent new stuff there, that would be stupid. But it always interesting to see if other stuff works. And, sorry, I still don't like what I've seen from Haskell, although I have to admit that I now have that eerie feeling that I'll need a monomorphism restriction myself.

Uh, subtyping has nothing inherently to do with representation (unless you want it to). In fact, Cardelli's semantics for System F_sub is just a bunch of coercions. The language inserts the appropriate coercions implicitly so representational details are moot. The coercions can, of course, be trivial and also the implementation doesn't actually have to work this way, this is just one way of understanding whatever the implementation actually does. Subtyping is purely an interface notion. Representation is irrelevant unless you make details of the representation part of the interface.

To take your original example, let's say I have two implementations of my language. One stores integers as floating point numbers and one stores them as machine words. Does the subtyping relation differ between those two implementations? Why should an implementation detail affect semantics?

Type != representation.

In a language without mutation you can't necessarily (denotationally) tell the difference between reusing the same object in a new context vs using an implicit coercion to do so.

In Scala, Int is a subtype of Any, but underneath the hood Scala has to box Ints in order to use them in an Any context.

To further illustrate, in Java, List<Object> and List<String> have no subtype relationship with each other, yet they share the same representation.

I said Haskell *imitates* subtyping.
The type of (+) is Num a => a -> a -> a. The only reason a mixed expression like "1 + 0.3" type checks is that a Haskell compiler implicitly passes all number literals through coercion functions. So the expression "1 + 0.3" is actually rewritten as "(fromInteger 1) + (fromIntegral 0.3)".

Yeah, somehow + is bound to the + from the float instantiation inherited by the Fractional class instead of the + from the int instantiation of the Num class. That's a form of subtyping. [Or is it overloading, now I am confused again ;-)]

Subtyping is the work of the devil. Overloading isn't.

Or is it the other way around? :-)