Haskell and principal types
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
On Fri, 05 Oct 2001 21:25:57 +0200, Karl-Filip Faxen wrote:
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.
class IsNil a where isNil :: a -> Bool
f x y = let g = isNil in (g x, g y)
I'm still having a lot of trouble grasping and comprehending this "monomorphism restriction". It just doesn't feel right, and I keep having a lot of trouble juggling all the descriptions I found on the web. So, I'll don my newbie hat and start asking all the obvious questions. I hope I don't annoy too much. I know there are people tired of discussing this, but the thing is that this monomorphism restriction is something very easy to bump into (I have), but all the definitions out there seem to be unable to seep in. Especially the one in the Haskell Report, BTW.
"If a declaration group"
Meaning something like "let g = isNil" up there?
"contains a pattern binding with a nonvariable pattern"
Meaning... what exactly?
"or one [pattern binding] where there is no type signature for the variable"
Meaning "g = isNil" above, without type signature for "g"?
"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? 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".
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",
Ok... This is probably the one explanation that has begun to make an impact in my mind.
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?
- a -> Bool (without quantification and with "IsNil a" among the predicates).
This is something I didn't understand either. Which predicates? Thanx for your patience O:-) Salutaciones, JCAB email: jcab@roningames.com ICQ: 101728263 The Rumblings are back: http://www.JCABs-Rumblings.com
participants (2)
-
Juan Carlos Ar�valo Baeza -
Karl-Filip Faxen