Monomorphism, monomorphism...

[Juan Carlos Arévalo Baeza]

On 6 Oct 2001 09:31:54 GMT, Marcin 'Qrczak' Kowalczyk wrote:

   First of all, thanks a lot for the detailed response.

>Yes, ... yes ... yes

   Well, I'm glad I got some of it right. Gives me hope :)

>>>"contains a pattern binding with a nonvariable pattern"
>>
>>=A0=A0Meaning... what exactly?
>
>A pattern which is something other than an identifier.

   Like defining a function, as opposed to defining a constant?

>>=A0=A0Hmmm... This still sounds like nonsensical (as in=
 counterintuitive
>>=A0=A0and artificial) to me. In a definition like "let g =3D isNil"
>>=A0=A0there cannot be any compelling reason to give "g" any type
>>=A0=A0different than the type of "isNil".
>
>There are two reasons for the monomorphism restriction:
>
>- isNil (or any value with a non-empty context in its type)=
 doesn't
>=A0really behave like a constant, but as a function taking a=
 dictionary
>=A0of 'IsNil a' as an implicit argument, so it's recomputed each=
 time
>=A0it it used...

   Ok... This is an angle I hadn't even approached yet. We're=
 talking about the internal implementation of the compiler here.=
 Hmmm...

   Shouldn't the compiler be able to limit the recomputations to=
 one per instance of the class? That sounds perfectly appropriate=
 to me, and it would solve this particular problem. Unless I'm=
 missing something here...

>=A0This point is silly in this case, because it is already a=
 function
>=A0with an explicit argument! It makes more sense however when the=
 type
>=A0is not of the form a->b. For example in 'n =3D 7*11*13' letting n=
 have
>=A0the type 'Num a =3D>=A0a' implies that it is recomputed each time=
 it
>=A0is used.

   Again, what about recomputing it once per instance of Num?

> Unless the compiler manages to optimize this, but it can't
>=A0in all cases (n can be used with different types in various=
 places).

   I guess I'm biased here by my knowledge of templates in C++,=
 which can be used to implement something very similar to type=
 classes in Haskell. This would be akin to different=
 instantiations of a single template, which should not present=
 any problems for the compiler.

   So, 'n =3D 7*11*13' would have type 'Num a =3D> a', which would=
 mean that it has a different value for each instantiation of the=
 context 'Num a'. So, where's the problem? It's not as if Haskell=
 didn't already have this functionality in the members of a type=
 class:

class Num a where
  n :: a
  n =3D 7*11*13

   'n' here has that type 'Num a =3D> a', doesn't it? Don't tell me=
 compilers will compute it twice if we use it twice, as in:

n1 =3D n
n2 =3D n

>- When a pattern binds several variables, it can happen that=
 their
>=A0types need different sets of class constraints. Using such a=
 variable
>=A0doesn't fully determine the type to perform the computation=
 in.
>=A0It's thus ambiguous and an error.

   You're talking about the case '(var1, var2) =3D expr', right?=
 That's because var1 and var2 cannot have different contexts?=
 That still sounds unnecessary to me. I mean, the tuple result=
 should have its own context, necessary to resolve the tuple=
 itself, and each of its elements should acquire its own context=
 as appropriate. Then all contexts should be unambiguous. In this=
 case, 'expr' should be able to have type:

expr:: <context0> =3D> (<context1> =3D> TypeOfVar1, <context2> =3D>=
 TypeOfVar2)

   I'm guessing from what I learn that this is not possible in=
 Haskell, right?

>=A0It's not ambiguous with monomorphic restriction, where all uses=
 of
>=A0all variables contribute to finding the single type to perform=
 the
>=A0computation in.

   Exactly. I think I'm starting to get a reasonable handle on=
 this.

>=A0Even with a single variable it can happen that some uses will
>=A0constrain the type enough to determine the instance, and some=
 will
>=A0not. Without monomorphic restrictions some uses are OK, but=
 others
>=A0will stop the compilation. With monomorphic restriction all=
 uses
>=A0contribute to a single type and typing might succeed.

   So it is. I just tried, with Hugs:

---
intToBool :: Int -> Bool
intToBool a =3D a =3D=3D 0

numToBool :: Num a =3D> a -> Bool
numToBool a =3D a =3D=3D 0

h :: Num a =3D> a
h =3D 4

g =3D h

f =3D (intToBool g) && (numToBool g)
---

   It complained with:

---
ERROR E:\JCAB\Haskell\TestMonomorphic.hs:14 - Type error in=
 application
*** Expression     : intToBool g
*** Term           : g
*** Type           : Integer
*** Does not match : Int
---

   You're saying that this is because, when seeing the line 'g =3D=
 h', the compiler immediately and arbitrarily picks a type for=
 'g', right? In this case, it's 'Integer'. Arbitrarily but not=
 randomly, right? What rules does it follow?

>The general trouble with monomorphic restriction is that let=
 bindings
>can mean two similar things:
>
>1. Create a single lazily evaluated object with the given=
 definition
>=A0and make it or its components available through variables=
 (pattern
>=A0binding).
>
>2. Define a possibly polymorphic function and perform the given
>=A0computation when it is applied (function binding).

   In case 2 we wouldn't need the restriction, right?

   I guess the only benefit from all this is efficiency, then. I=
 think I see it. Back to the dictionaries... the dictionary for a=
 type class is closed as soon as the definition of that class is=
 closed. You can't add any new free functions to that dictionary.=
 Therefore, the lookup for those functions would need to follow a=
 much slower path. Is this accurate? I can see ways to overcome=
 this limitation in a compiler, but it would need to make use of=
 some deferred compilation, just like "export"ed templates in=
 C++, where the linker has to be able to compile instances of=
 templates. And support for "export" in most current C++=
 compilers is far from ideal. And if C++, with all its extensive=
 use doesn't have it, how could possibly Haskell have it?

>>>but two legal possibilities are
>>>- forall b . [b] ->=A0Bool, and
>>
>>=A0=A0Choosing an explicit instance of IsNil. But this sounds
>>=A0=A0nonsensical to me, too. No instance should be choosing unless=
 the
>>=A0=A0specific instance type is forced by the definition.=
 Otherwise,
>>=A0=A0if there are two insances, which one would it choose?
>
>Type inference defined in the traditional way is=
 non-deterministic
>in nature.
>
>A good property of a type system is that it should not matter=
 when
>various choices are made: as long as we succeed in deriving a=
 type
>of the whole program, the overall meaning should be=
 unambiguous.
>This property has a name - sorry, I forgot which.
>
>When we choose an instance too early, we might not succeed at=
 all (if
>another instance happens to be needed). Unfortunately in this=
 case we
>may fail in either case: no choice is sure to be better than the=
 other.
>
>It might happen that by choosing this instance now it will be OK=
 when
>f is used. The other possibility of the type for f would take=
 away
>some freedom: we can't use this instance later with different=
 choices
>for types of list elements, because both uses of g must make the=
 same
>choices for type variables with class constraints. It's not=
 visible yet
>(before choosing the instance) that the single type 'IsNil a=
 =3D>=A0a'
>will expand into something containing quantified type variables=
 without
>class constraints which can be instantiated independently!

   Hmmm... As in typing '2+2' in Hugs and having it say=
 'ambiguous type: Num a =3D> a'? Is this the kind of problem that=
 you're talking about?

   Hmmm... I begin to see the real problem. If we have a program=
 such as:

---
g :: Num a =3D> a
g =3D 0

main =3D print g
---

   The compiler MUST choose an instance for the overloaded=
 'print' (must choose a concrete type for 'g'), because the=
 program is ambiguously typed otherwise.

>Of course it may also happen that completely different instances=
 will
>be needed when f is used, so choosing the instance now is bad.=
 That's
>the point: there is no universal choice. The property of=
 principal
>types would allow us to derive some most general type of f, such=
 that
>any other type is its instance. Unfortunately it doesn't hold.=
 This
>case was not expected.

   The thing is that in some instances, the compiler chooses a=
 bit too early. For example:

---
h :: Num a =3D> a
h =3D 0

g =3D h
---

   Now 'g' is of type 'Integer' in Hugs, even though it doesn't=
 need to. 'Num a =3D> a' would be more correct.

   Same with functions:

---
h :: Num a =3D> a -> a
h t =3D t

g =3D h
---

   Now 'g' is of type 'Integer -> Integer', instead of 'Num a =3D>=
 a -> a'.

   That's what I call "too early".

   Thanx a bunch.

   Salutaciones,
                        JCAB
email: jcab@roningames.com
ICQ: 101728263
The Rumblings are back: http://www.JCABs-Rumblings.com