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"
>>
>>  Meaning... what exactly?
>
>A pattern which is something other than an identifier.

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

>>  Hmmm... This still sounds like nonsensical (as in counterintuitive
>>  and artificial) to me. In a definition like "let g = isNil"
>>  there cannot be any compelling reason to give "g" any type
>>  different 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
> really behave like a constant, but as a function taking a dictionary
> of 'IsNil a' as an implicit argument, so it's recomputed each time
> it 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...

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

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

> Unless the compiler manages to optimize this, but it can't
> in 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 = 7*11*13' would have type 'Num a => 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 = 7*11*13

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

n1 = n
n2 = n

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

   You're talking about the case '(var1, var2) = 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> => (<context1> => TypeOfVar1, <context2> => TypeOfVar2)

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

> It's not ambiguous with monomorphic restriction, where all uses of
> all variables contribute to finding the single type to perform the
> computation in.

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

> Even with a single variable it can happen that some uses will
> constrain the type enough to determine the instance, and some will
> not. Without monomorphic restrictions some uses are OK, but others
> will stop the compilation. With monomorphic restriction all uses
> contribute to a single type and typing might succeed.

   So it is. I just tried, with Hugs:

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

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

h :: Num a => a
h = 4

g = h

f = (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 = 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
> and make it or its components available through variables (pattern
> binding).
>
>2. Define a possibly polymorphic function and perform the given
> computation 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] -> Bool, and
>>
>>  Choosing an explicit instance of IsNil. But this sounds
>>  nonsensical to me, too. No instance should be choosing unless the
>>  specific instance type is forced by the definition. Otherwise,
>>  if 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 => a'
>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 => 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 => a
g = 0

main = 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 => a
h = 0

g = h
---

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

   Same with functions:

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

g = h
---

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

   That's what I call "too early".

   Thanx a bunch.

   Salutaciones,
                        JCAB
email: [EMAIL PROTECTED]
ICQ: 101728263
The Rumblings are back: http://www.JCABs-Rumblings.com




_______________________________________________
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Reply via email to