- Haskell - Haskell.org

Re: Monomorphism, monomorphism...
by Marcin 'Qrczak' Kowalczyk 08 Oct '01

08 Oct '01

Sat, 6 Oct 2001 22:22:24 -0700, Juan Carlos Arévalo Baeza <jcab(a)roningames.com> pisze: >>A pattern which is something other than an identifier. > > Like defining a function, as opposed to defining a constant? No: a pattern, e.g. (x,y), Just y, (x:_) etc. A function definition looks like an identifier applied to patterns, which usually doesn't look like a pattern. These are two forms of lhs of =. These yntaxes collide only for identifiers alone. They could be treated like degenerate patterns (which match anything) or like functions with no arguments. >>- 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... The difference is visible for the programmer not only in speed, but also by typing rules: pattern bindings are monomorphic, functions can be polymorphic. With monomorphic restriction a lhs looking like an identifier is treated as something between pattern and function: type variables with class constraints are monomorphic, type variables without conatraints are polymorphic. And it can be promoted to a fully polymorphic version by giving a type signature. > Shouldn't the compiler be able to limit the recomputations to > one per instance of the class? It would require very unusual implementation. Currently the compiler doesn't need to build dictionaries indexed by types at runtime and even doesn't need to recognize which types are "the same" at runtime. > 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. C++ templates require having source available in each place a template is used. I agree that it would be useful for Haskell compilers to compile some instances that way when optimization is turned on, but the traditional way to implement classes uses a single compiled version which is passed various dictionaries at runtime. It works because Haskell's rules of overloading are defined more "semantically". C++ templates are closer to syntactic macros. The C++ way wouldn't work for Haskell in general because sometimes the depth of instances created is not bounded statically, unlike C++ templates which are instantiated at compile time. And it doesn't work with extensions like existential quantification, where types which differ in instance dictionaries can be packed into values of a single type, so the instance to use *must* be chosen dynamically (data flow can't be statically determined in general). It can be only an optimization (and perhaps it's sometimes more code bloat than optimization), it doesn't fit as the primary model IMHO. > 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 It will probably recognize that the same instance is needed in both places. But it will almost certainly recompute when n1 and n2 are defined in separate modules. It can't perform the multiplication until the type is known. >>- 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? They can, caused by different sets of type variables present in types of var1 and var2: (x, y) = let z = read "[10,20]" in (z, show z) Here x :: Read a => a, y :: String. It makes no sense to give y yhe type 'Read a => String'. This type would be ambiguous because 'a' is absent in the main part of the type. With monomorphism restriction uses of x determine the way y is computed. Without monomorphism restriction all uses of x and y have individually instantiated types, so there is no way to compute y at all: you don't know on which type it should be done, as in show (read "[10,20]") which is ambiguous. > So it is. I just tried, with Hugs: Hugs implements this incorrectly. AFAIK it doesn't let usages of global variables contribute to disambiguation of their types. >>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? Yes. Functions are defined one at a time, not by matching patterns; and their recomputation is expected. >>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? Not quite: the Karl's example is more subtle. Even if the overloading is resolved by the surrounding code, choosing an instance early may give extra opportunities to instantiate the resulting type several times with slightly different types. -- __("< Marcin Kowalczyk * qrczak(a)knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK

2 1

Your Bid 4 Placement Account
by unknown＠example.com 07 Oct '01

07 Oct '01

1 0

Re: Monomorphism, monomorphism...
by Marcin 'Qrczak' Kowalczyk 07 Oct '01

07 Oct '01

Fri, 5 Oct 2001 19:02:50 -0700, Juan Carlos Arévalo Baeza <jcab(a)roningames.com> pisze: >>"If a declaration group" > > Meaning something like "let g = isNil" up there? Yes, a group of mutually recursive bindings or a single non-recursive binding (equations inside let or where or at module toplevel). >>"contains a pattern binding with a nonvariable pattern" > > Meaning... what exactly? A pattern which is something other than an identifier. >>"or one [pattern binding] where there is no type signature for >>the variable" > > Meaning "g = isNil" above, without type signature for "g"? Yes. >>"then the context parts of the type schemes derived for the bound >>variables must be empty" > > Meaning that in "let g = ...", "g" cannot be > "g :: <context> => <type>" unless the context is explicitly given? Yes. > 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... 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. Unless the compiler manages to optimize this, but it can't in all cases (n can be used with different types in various places). - 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. It's not ambiguous with monomorphic restriction, where all uses of all variables contribute to finding the single type to perform the computation in. 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. 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). Degenerate forms of these cases look the same in Haskell: a single identifier is on the left. It's not clear which one the programmer meant. Often it doesn't matter. It really matters only when classes are involved: either to determine where to apply implicit arguments of class dictionaries or to disambiguate instances by making some types more concrete. Clean uses three forms of equal sign: => defined a function, := binds a single lazily evaluated object, and = means => on the toplevel and := locally (if I remember the syntax). ML doesn't have this problem because it doesn't have classes. >>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! 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. >>- a -> Bool (without quantification and with "IsNil a" among the >> predicates). > > This is something I didn't understand either. Which predicates? I think "isNil a" goes to the context of the whole expression containing the "let g = ..." (I'm not sure if Karl meant that). Generally for an expression the compiler determines a type and a set of collected class constraints, resulting from using identifiers having polymorphic types with constraints. A polymorphic type of an identifier which is used is instantiated using fresh type variables and constraints apply to these type variables. A let binding usually "eats" all constraints and puts them in the declaration. The constraints will reappear outside when the declared identifier is used, but they can appear in different configurations when the identifier is used polymorphically: instantiated to various types. But in a monomorphic let binding the same type variables can be used for both the body of the declaration and its usages: the variable is not polymorphic, all usages have the same type. So it makes sense to float the context out to the expression containing the whole let. It will be determined once for the whole body of f. -- __("< Marcin Kowalczyk * qrczak(a)knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK

2 1

Import Chasing Problems - hello.lhs
by John Heron 06 Oct '01

06 Oct '01

I just installed ghc 5.02 on my NT 4.0 machine, and I'm wondering if the import chasing is broken for ghc-5.02 on Windows NT? Or perhaps there is yet another thing I don't understand about Haskell's environment or modules? I got the following complaints when trying to compile Sigborn Finne's Win32 example hello.lhs (http://www.dcs.gla.ac.uk/~sof/hello.lhs) F:\stuff>ghc -o hello hello.lhs hello.lhs:14: failed to load interface for `Win32': Could not find interface file for `Win32' hello.lhs:15: failed to load interface for `Addr': Could not find interface file for `Addr' F:\stuff>ghc -ic:\ghc-5.02\imports\ -o hello hello.lhs hello.lhs:14: failed to load interface for `Win32': Could not find interface file for `Win32' hello.lhs:15: failed to load interface for `Addr': Could not find interface file for `Addr' F:\stuff>ghc -ic:\ghc-5.02\imports\lang;d:\ghc-5.02\imports\win32 -o hello hello.lhs hello.lhs:14: Module `Win32' is located in package `Main' but its interface file claims it is part of package `win32' hello.lhs:15: Module `Addr' is located in package `Main' but its interface file claims it is part of package `lang' Or perhaps there's an environment variable I should have set that I didn't? I did btw check the docs. Regards, John Heron

1 0

Re: Haskell and principal types
by John Hughes 06 Oct '01

06 Oct '01

So here is the offending program: class IsNil a where isNil :: a -> Bool instance IsNil [b] where isNil [] = True isNil _ = False f x y = let g = isNil in (g x, g y) The monomorphism restriction applies to the binding of "g" since there is no type signature. Thus it is not legal to derive "forall a . IsNil a => a -> Bool", but two legal possibilities are - forall b . [b] -> Bool, and - a -> Bool (without quantification and with "IsNil a" among the predicates). These two choices lead to different types for "f": - forall a b . [a] -> [b] -> (Bool,Bool), and - forall a . IsNil a => a -> a -> (Bool,Bool) Interesting. Every now and then I propagate for replacing the MR by two forms of binding: pat = expr -- call by NAME binding, fully polymorphic and overloaded pat := expr -- call by NEED binding, completely monomorphic The point is to make the programmer aware of when monomorphism applies, so its consequences are not surprising, and also aware (with an = binding) that there is a risk of recomputation. It sounds as though Clean has adopted a similar idea. With "g = isNil", the type of f becomes forall a b. (IsNil a, IsNil b) -> a -> b -> (Bool, Bool) With "g := isNil", it becomes forall a. IsNil a => a -> a -> (Bool, Bool) The two incomparable types for f become types of two different programs; problem solved (in this example at least). Karl-Filip, would this idea restore the principal type property in general? John Hughes

1 0

Re: Monomorphism, monomorphism...
by Karl-Filip Faxen 06 Oct '01

06 Oct '01

Hi! Marcin wrote: > Juan Carlos Arévalo Baeza wrote: >> Karl-Filip wrote: >>>- a -> Bool (without quantification and with "IsNil a" among the >>> predicates). >> >> This is something I didn't understand either. Which predicates? > >I think "isNil a" goes to the context of the whole expression >containing the "let g = ..." (I'm not sure if Karl meant that). Exactly what I meant! Then it goes into the context of "f" because "f" is defined using function syntax (formal parameters to the left of "=") so everybody knows it's a function so it doesn't hurt if it gets some extra arguments after dictionary insertion. /kff

1 0

Haskell and principal types
by Karl-Filip Faxen 06 Oct '01

06 Oct '01

Hi all! I've been spending some time the last year writing up a formalization of the Haskell type system (actually, most of the static semantics). In doing so, I've come across an oddity. It seems that Haskell does not have the principal type property, ie there are Haskell expressions which, in a given typing environment, can be assigned at least two types that are not generic instances of each other but can not be assigned any type more generic that the two. The culprit is the monomorphism restriction. I was kind of surprised, thinking that principal types were likely to hold for Haskell, but it seems not. The monomorphism restriction goes like this in my inference rules: If a declaration group contains a pattern binding with a nonvariable pattern or one where there is no type signature for the variable, then the context parts of the type schemes derived for the bound variables must be empty. The difference to for instance "Typing Haskell in Haskell" is that my formalization is a set of inference rules (starting from the draft static semantics by Peyton Jones and Wadler), so many different types can be derived for the same typing environment and expression, wheras THIH is a program which computes a single type. So here is the offending program: class IsNil a where isNil :: a -> Bool instance IsNil [b] where isNil [] = True isNil _ = False f x y = let g = isNil in (g x, g y) The monomorphism restriction applies to the binding of "g" since there is no type signature. Thus it is not legal to derive "forall a . IsNil a => a -> Bool", but two legal possibilities are - forall b . [b] -> Bool, and - a -> Bool (without quantification and with "IsNil a" among the predicates). These two choices lead to different types for "f": - forall a b . [a] -> [b] -> (Bool,Bool), and - forall a . IsNil a => a -> a -> (Bool,Bool) These two are incomparable (neither is a generic instance of the other). I can not see that it is legal to derive a type for "g" which will allow some type for "f" that is more general than both of these. As far as I can see, the inference algorithm from "Typing Haskell in Haskell" would give the second type, which is also what GHC derives. The trick here is the instance declaration for "IsNil [a]" which has an empty instance context, ie it is not important what the element type is. So, is this already well known in the Haskell community, or is it a new result? Of course, it is not a result until one has *proved* that *no* type more general than the two above is derivable, but it is a strong conjecture. In the "Type Classes in Haskell" paper from TOPLAS, the smaller system without the monomorphism restriction was conjectured to have principal types. Also, the Haskell Report (section 4.1.4) states: "Haskell 's extended Hindley-Milner type system can infer the principal type of all expressions, including the proper use of overloaded class methods (although certain ambiguous overloadings could arise, as described in Section 4.3.4)." But there is no ambiguity involved here. Cheers, /kff Jones: Typing Haskell in Haskell, in Proceedings of the Third Haskell Workshop Hall et al: Type Classes in Haskell, TOPLAS vol 18 no 2 Peyton Jones and Wadler: A Static Semantics for Haskell, draft paper, Glasgow

2 1

Report with lots of hyperlinks
by Ian Lynagh 05 Oct '01

05 Oct '01

Hi I've rewritten the syntax section (appendix B) in docbook, slightly hacked the nwalsh style sheets and produced http://c93.keble.ox.ac.uk/~ian/report/html/ The lexical Structure section is also just started more as proof-of-concept for linking back into the rest of the report. As well as adding hyperlinks between the nonterminals I've tried to distinguish between terminals and the operators better, but I don't think I've been very successful. Don't know if anyone else will be interested in this, but if you are then there you go :-) Ian

1 0

Re: Strange error in show for datatype
by Jan-Willem Maessen 05 Oct '01

05 Oct '01

Dylan Thurston <dpt(a)math.harvard.edu> points out my mistake: > > Strictness alas matters. Here's the witness: > > > > class Num a => ZeroList a where > > consZero :: a -> [a] > > consZero _ = 0:xs > > Err, "Num a" is already a bad context by Simon's criterion because of > "fromInteger", which is what ultimately causes the problem in this > case. Quite right. I overlooked the fact that the superclass constraint "Num a" implicitly includes all the methods of Num in ZeroList for these purposes. Olaf Chitil <olaf(a)cs.york.ac.uk> gives an example along the lines I was attempting (which I've corrected slightly): > instance Show MyType where > shows _ = ("element of my type" ++ ) The important thing here is that the non-strict shows method can make up any result it likes. I do think some sort of extended defaulting mechanism as suggested by Thomas Hallgren would be useful. Yes, we will occasionally choose confusing interpretations of e.g. "" vs []. On the other hand, I'm sure we can warn when defaulting in this way. But its not the magic bullet against the monomorphism restriction one might have hoped for... -Jan-Willem Maessen

1 0

PLI 2002-Call for workshop proposals
by Carsten Schuermann 05 Oct '01

05 Oct '01

CALL FOR WORKSHOP PROPOSALS Principles, Logics, and Implementations of high-level programming languages (PLI 2002) Pittsburgh, USA October 3 - 8, 2002 Carsten Schuermann http://pli2002.cs.brown.edu/workshops PLI 2002, a federation of colloquia which includes ICFP 2002 (ACM-SIGPLAN International Conference on Functional Programming) and PPDP 2002 (ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming), will be held in Pittsburgh, USA, October 3-8 2002. Affiliated workshops will be scheduled from October 3 through October 8. Researchers and practitioners are invited to submit workshop proposals, that may be sent to the PLI 2002 Workshop Chair Carsten Schuermann, carsten(a)cs.yale.edu by e-mail (Postscript, Pdf, ASCII) with "PLI02 Workshop Submission" in the subject header. Following SIGPLAN's sponsorship procedures, proposals should include: 1. Name of the workshop, name of the sponsoring conference (ICFP/PPDP) Workshops associated with ICFP may be scheduled during PPDP, workshops associated with PPDP may be scheduled during ICFP. 2. The goals of the workshop 3. Names and addresses of organizers 4. Names of potential participants, such as program committee members 5. Plans for call for participation (e.g., call for papers) 6. Expected number of attendees 7. Plans for publicity 8. Plans for a proceedings 9. Description of past versions of the workshop including date, organizers, paper submission/acceptance counts, attendance, site, registration fees and summary budget information 10. Url address of the workshop description Proposals will be evaluated by the PLI 2002 Workshop Chair, the ICFP, and PPDP Program and Conference Chairs, and by the SIGPLAN Executive Committee. Be advised that workshops must be sponsored by SIGPLAN and require therefore SIGPLAN approval (see http://www.acm.org/sigplan/sigplan_workshop_proposal.htm for more information.) THE DEADLINE FOR RECEIPT OF PROPOSALS IS DECEMBER 7, 2001. Notification of acceptance will be made by February 1, 2002. Workshop selection committee: Claude Kirchner : Program Chair of PPDP 2002 Simon Peyton Jones : Program Chair of ICFP 2002 Frank Pfenning : Chair of PPDP 2002 Carsten Schuermann : Workshop Chair of PLI 2002 Mitch Wand : General Chair of ICFP 2002

1 0