Re: Implict parameters and monomorphism
> Except, of course, for top level bindings which is where the > monomorphism restriction is usually most noticable. Right, but an explicit monomorphic type signature would ensure that it's computed once. Type signatures on toplevel bindings are a good idea anyway, and there is no ambiguity for implicit parameters which must yield a function-like binding. This is a matter of taste, and Haskell deliberately supports both a style with and without type signatures on top-level bindings. I'd be sorry to see that change. One good reason for NOT giving inferrable type signatures is that including them makes programs less modifiable: a small local change, such as adding a parameter to a type, may force a large number of consequential changes to type signatures. I've seen cases where programmers refrained from a significant improvement, because of the labour required to update type signatures (which had been included, ironically, to disable the monomorphism restriction!). I'm not saying it's bad to give type signatures, just that there are arguments for both styles, and the language ought not to make either one difficult to use. John
Fri, 4 May 2001 09:27:51 +0200 (MET DST), John Hughes <rjmh@cs.chalmers.se> pisze:
One good reason for NOT giving inferrable type signatures is that including them makes programs less modifiable: a small local change, such as adding a parameter to a type, may force a large number of consequential changes to type signatures.
Type synonyms should make this easier. Maybe the language should be improved somewhere here: class context synonyms? unbound type variables on the rhs of type synonyms? specifying parts of a type leaving the rest inferred? These problems shouldn't arise for ensuring evaluation once, where the type is usually monomorphic! It's the other way around which can cause trouble (e.g. there are no class context synonyms). -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK
I have thought about this too. omission of type signatures seems to be an effective catalyst for code re-use yet this benefit is rarely emphasised. I was thinking about ways to make it easier and toyed around with allowing 'unkowns' in type declarations to allow you to specify only the important part of what you want in a type signature without having to over-specify the types. My idea was to allow '_' to be used in type signatures and represent any type. foo s = 4 foo :: _ foo :: _ -> Int foo :: String -> _ foo :: String -> Int would all be valid types (with different meanings) for 'foo'. This would be useful if say, you had to specify a function returned a plain Int to resolve ambiguity but you didn't want to specify the type of the input argument, perhaps because you are in the process of writing/debugging code and know the type will change. this has the nice generalization that all undeclared types are taken to be ':: _' note that this is not universal quantification because that would imply any type will work, where in actuality we just want to use the specific type infered via standard type inference for part of the declaration and specify exactly another part. The reason I didn't make the proposal was because I am not sure how useful such a thing would be in production code, even though there have been many times during the development/discovery process when such a feature would have signifigantly eased incremental development. John On Fri, May 04, 2001 at 10:40:34AM +0000, Marcin 'Qrczak' Kowalczyk wrote:
Fri, 4 May 2001 09:27:51 +0200 (MET DST), John Hughes <rjmh@cs.chalmers.se> pisze:
One good reason for NOT giving inferrable type signatures is that including them makes programs less modifiable: a small local change, such as adding a parameter to a type, may force a large number of consequential changes to type signatures.
Type synonyms should make this easier. Maybe the language should be improved somewhere here: class context synonyms? unbound type variables on the rhs of type synonyms? specifying parts of a type leaving the rest inferred?
These problems shouldn't arise for ensuring evaluation once, where the type is usually monomorphic! It's the other way around which can cause trouble (e.g. there are no class context synonyms).
-- -------------------------------------------------------------- John Meacham http://www.ugcs.caltech.edu/~john/ California Institute of Technology, Alum. john@foo.net --------------------------------------------------------------
Fri, 4 May 2001 11:27:07 -0700, John Meacham <john@foo.net> pisze:
My idea was to allow '_' to be used in type signatures and represent any type.
I like it. There were also proposals for '..'. It would be useful in cases analogous to this: import IArray import MArray f:: (IArray a e, Ix i) => a i e -> a i e f arr = runST (do marr <- thaw arr do some stateful operations on marr freeze marr) where the type of thaw and freeze make the mutable array type ambiguous. A type signature to disambiguate it would have to mention element and index types, which are type variables bound outside, and the state token, which is eaten by runST. So you have to either use a ghc/Hugs extension of pattern or result type signatures, to bind all these types to names, and move the body to a separate function, so the state token is visible - or specify a polymorphic function type signature on freeze alone or use a specialized variant of freeze. It would be nice to write just (marr :: STArray _ _ _) without having to invent types for the state, index and element. -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK
4 May 2001 18:50:30 GMT, Marcin 'Qrczak' Kowalczyk <qrczak@knm.org.pl> pisze:
f :: (IArray a e, Ix i) => a i e -> a i e f arr = runST (do marr <- thaw arr do some stateful operations on marr freeze marr)
Actually using pattern type signatures alone is almost enough here: f:: (IArray a e, Ix i) => a i e -> a i e f arr = runST (do (marr :: STArray s i e) <- thaw arr do some stateful operations on marr freeze marr) except that ghc has a small bug: pattern type signatures don't introduce type variables in the 'do' notation, as they do in lambda arguments. Rewriting it to use '>>=' and lambdas instead of 'do' helps: f:: (IArray a e, Ix i) => a i e -> a i e f arr = runST ( thaw arr >>= \(marr :: STArray s i e) -> do some stateful operations on marr >> freeze marr) But doesn't solve completely. There is a strange error message "Could not deduce `MArray (STArray s1) e (ST s)' from the context (IArray a e, Ix i)" with two suggested resolutions, both bogus. The problem is with 's': it's not bound by lambda but eaten by runST. I have to move the argument of runST to a separate function, to bind 's' in its result type signature, to be able to use it in the pattern type signature of marr. This situation can be improved. There was a discussion three months ago about making pattern and result type signatures one-way matching. Currently if a part of the type of an argument is not a type variable bound at the given place, I can't write a type variable in the appropriate pattern type signature, but must spell the inferred type. Except that its context is not written. For example changing 'e' in the type of f above into 'Int' makes the type signature on marr illegal: I must write 'STArray s i Int' too. This is especially tricky in the presence of fundeps, because whether a type is fully determined is not necessarily obvious if it's deduced from fundeps. Ghc requires the programmer to manually follow fundeps to infer the same amount that ghc knows, instead of specifying just the part of the type I am interested in. Another bad case is above. The problematic type is not bound by the given lambda, it's not a constant, and it's not bound by a pattern outside either. It's a free type variable of the argument of runST, eaten by runST. There is no way to write it except by moving the body of runST to a separate function with a result type signature. I would like to make pattern and result type signatures one-way matching, like in OCaml: a type variable just gives a name to the given part of the type, without constraining it any way - especially without "negative constraining", i.e. without yielding an error if it will be known more than that it's a possibly constrained type variable... SimonPJ sais he agreed and asked Hugs people what they think, and they didn't reply. This reminds me the 'with' story :-( This change, together with fixing pattern type signatures in 'do', would make the function at the top legal. -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK
On Fri, May 04, 2001 at 09:27:51AM +0200, John Hughes wrote:
One good reason for NOT giving inferrable type signatures is that including them makes programs less modifiable: a small local change, such as adding a parameter to a type, may force a large number of consequential changes to type signatures.
Absolutely -- suppose you add a `trace' somewhere in your program, which conjures up a Show constraint everywhere... -- Mieszko
participants (4)
-
elf@sandburst.com -
John Hughes -
John Meacham -
Marcin 'Qrczak' Kowalczyk