Explicit specification of function types

Everything I've read has said that it's generally considered good practice to specify the full type of a function before the definition. Why is this? It almost seems to go against the principles of type inference. Why let the compiler infer types if you're just going to tell it what types to use for everything? Ok well, not really for everything, you don't typically specify types for local bindings, but still why the inconsistency? I have a little experience with ML and F# and there you're encouraged to -not- specify types explicitly, and let the compiler infer them for you. In fact, it seems like it would be fairly common where you specify a type that is -less- general than the type that the compiler would infer for you, because the most general type might involve a combination of type classes used in various ways, and it may not always be obvious to the programmer how to specify it correctly.

Zachary Turner wrote:
Everything I've read has said that it's generally considered good practice to specify the full type of a function before the definition. Why is this?
I'm still a newbie but using (and leaving) the type definitions helps me quickly recall what a routine is doing and also provides handy documentation when I have to hack (uhh ... I mean modify) the code weeks later. I also agree that when coding having the definitions 'localize' the type error messages resulting in faster development. Tom
It almost seems to go against the principles of type inference. Why let the compiler infer types if you're just going to tell it what types to use for everything? Ok well, not really for everything, you don't typically specify types for local bindings, but still why the inconsistency? I have a little experience with ML and F# and there you're encouraged to -not- specify types explicitly, and let the compiler infer them for you. In fact, it seems like it would be fairly common where you specify a type that is -less- general than the type that the compiler would infer for you, because the most general type might involve a combination of type classes used in various ways, and it may not always be obvious to the programmer how to specify it correctly.

On Mon, Mar 23, 2009 at 7:08 PM, Tom Poliquin
Zachary Turner wrote:
Everything I've read has said that it's generally considered good practice to specify the full type of a function before the definition. Why is this?
I'm still a newbie but using (and leaving) the type definitions helps me quickly recall what a routine is doing and also provides handy documentation when I have to hack (uhh ... I mean modify) the code weeks later.
I agree with this. It's quite useful to be able to just look at a function and see what its type is without having to go into GHCi and query it. This becomes less useful for local-er variables because their type can often be inferred from context and they are not generally used elsewhere in the function. Alex

I'm a beginner just learning about type inference (through getting lots of error messages and using :t a lot). I find it fascinating, and it seems a shame to disregard this power by declaring all types. However I realize that it's the more global or critical types that should be declared, and more local areas can be left to inference. Perhaps also the compiler's ability to infer is related to its ability to detect compile-time type errors. In other words, if you program a compiler to be sensitive enough to detect all type errors at compile time, then by necessity you are giving it the smarts to infer types. Is that right? Thanks, Mike

On 2009 Mar 24, at 0:21, Michael Mossey wrote:
I'm a beginner just learning about type inference (through getting lots of error messages and using :t a lot). I find it fascinating, and it seems a shame to disregard this power by declaring all types. However I realize that it's the more global or critical types that should be declared, and more local areas can be left to inference. Perhaps also the compiler's ability to infer is related to its ability to detect compile-time type errors. In other words, if you program a compiler to be sensitive enough to detect all type errors at compile time, then by necessity you are giving it the smarts to infer types. Is that right?
It may have the knowledge but not the mechanism (consider C++). -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH

2009/3/23 Brandon S. Allbery KF8NH
On 2009 Mar 24, at 0:21, Michael Mossey wrote:
I'm a beginner just learning about type inference (through getting lots of error messages and using :t a lot). I find it fascinating, and it seems a shame to disregard this power by declaring all types. However I realize that it's the more global or critical types that should be declared, and more local areas can be left to inference. Perhaps also the compiler's ability to infer is related to its ability to detect compile-time type errors. In other words, if you program a compiler to be sensitive enough to detect all type errors at compile time, then by necessity you are giving it the smarts to infer types. Is that right?
It may have the knowledge but not the mechanism (consider C++).
I guess now would be a bad time to mention that C++0x has type inference :D Off topic, but couldn't resist. Anyway, back to the original topic (kind of), would you consider it bad advice to omit type annotations in languages like ML or F# as well? I can identify with both arguments, and I just wonder why one group of people would recommend omitting them, and another would recommend supplying them, with the only difference being the language. I know in something like F# you have a fairly advanced IDE, so you can simply hover the mouse over a function name and get its inferred type signature. I know you mentioned the performance penalty associated with a type being "too generic", in the sense that typeclass lookups will constantly have to be done at runtime if something is too generic. Perhaps the fact that these other languages don't support typeclasses and hence don't have the same performance penalty is part of the reason why it's ok (or at the very least, not as bad) to do this in these languages as it is in Haskell? I'm mostly just trying to understand why it's good in one language, and bad in another. I'm sure there must be a number of tangible advantages in each language, that either don't apply or are mapped to disadvantages in the other.

On 2009 Mar 24, at 0:41, Zachary Turner wrote:
typeclass lookups will constantly have to be done at runtime if something is too generic. Perhaps the fact that these other languages don't support typeclasses and hence don't have the same performance penalty is part of the reason why it's ok (or at the very least, not as bad) to do this in these languages as it is in Haskell?
That's my understanding, F++ types don't require any runtime lookups so inference can't surprise you. Note that this is also applicable to the other problem: since F++ doesn't have typeclasses, type errors are less likely to be caught in confusing places, and when they are the type error is much simpler; Haskell will happily infer unexpected typeclasses if it moves inference along, then include the typeclass in the error message when it finally stalls out. Most commonly something like "Num (a -> b)" because you had too few/too many arguments somewhere, which points to another reason that type inference in Haskell can do unexpected things: F++ has parenthesized function arguments, so it will catch too few/too many arguments directly, but Haskell's uncurried function call notation almost guarantees strange errors in those cases even if you have everything explicitly typed.
Prelude> :t fromInteger 4 6 :: Double
<interactive>:1:0: No instance for (Num (t -> Double)) arising from a use of `fromInteger' at <interactive>:1:0-14 Possible fix: add an instance declaration for (Num (t -> Double)) In the expression: fromInteger 4 6 :: Double
-- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH

2009/3/24 Brandon S. Allbery KF8NH
That's my understanding, F++ types don't require any runtime lookups so inference can't surprise you.
It uses .NET interfaces for that, but the F# expert book mentions they would like to have type classes in a future version of the language.
in Haskell can do unexpected things: F++ has parenthesized function arguments, so it will catch too few/too many arguments directly, but Haskell's uncurried function call notation almost guarantees strange errors in those cases even if you have everything explicitly typed.
Not really, F# has both curried and uncurried forms, just like Haskell. It is true that F# encourages automatic generalization without type signatures. You never need to give one, even for exported modules. But the lack of type classes has its price. E.g. add x y = x + y What is the type of add in F#? Well, that depends on the first usage of this function... Give it Ints and it becomes add :: Int -> Int -> Int, and you can't use it on Doubles any more. Very confusing, since you can use the overloaded (+) on any type. These are current limitations of the language. At least that what I understood from it...

On Tue, Mar 24, 2009 at 6:02 PM, Peter Verswyvelen
2009/3/24 Brandon S. Allbery KF8NH
That's my understanding, F++ types don't require any runtime lookups so inference can't surprise you.
It uses .NET interfaces for that, but the F# expert book mentions they would like to have type classes in a future version of the language.
in Haskell can do unexpected things: F++ has parenthesized function arguments, so it will catch too few/too many arguments directly, but Haskell's uncurried function call notation almost guarantees strange errors in those cases even if you have everything explicitly typed.
Not really, F# has both curried and uncurried forms, just like Haskell.
It is true that F# encourages automatic generalization without type signatures. You never need to give one, even for exported modules.
But the lack of type classes has its price. E.g.
add x y = x + y
What is the type of add in F#?
Well, that depends on the first usage of this function... Give it Ints and it becomes add :: Int -> Int -> Int, and you can't use it on Doubles any more. Very confusing, since you can use the overloaded (+) on any type. These are current limitations of the language.
At least that what I understood from it...
What you say is partially true. For example, if delcared as you typed it, a rule similar to the monomorphism restriction (from what I understand of the monomorphism restriction) applies. If it's never used, x and y are of type int, and if they are used, x and y pick up the type of whatever you call it with. So doubles if you invoke it with 3.0 and 4.0, ints if you invoke it with 3 and 4, and an error if you invoke it once with doulbes and once with ints. The F# answer to this is to "inline" the function. For example: let inline add (x:'a) (y:'a) : 'a = x+y let result1 = add 3 4 let result2 = add 3.0 4.0 Hover over this declaration of add to get its type and you see "add : 'a -> 'a -> 'a (requires member (+)) Here, result1 is an int and result2 is a double. I haven't heard this from straight from the developers, but I suspect inlining is necessary due to the .NET Framework's support for reflection. Consider, for example, what would happen if you tried to obtain the method add via reflection and there was code for exactly 1 add method present in the binary. The code would have no reasonable way to behave. By inlining, I believe it inserts multiple definitions of hte function into the code, similar to what you get when you instantiate a C++ template. Anyway, a bit off topic, but at the very least I'm starting to understand why it's ok in F# but not really so much in Haskell. The issue of documenting the function I think is kind of a non issue actually, because if it were really just for the purposes of documentation you could just comment out the the type signature so that it's still visible but not interpreted by the compiler. In F# though the documentation is even less of an issue since you get automatic mouse-hover type definitions. The same thing applies to the issue of detecting type errors. It's pretty easy to find them when all the type inference mismatches are underlined for you on the fly. But in Haskell it seems the problem of finding type errors is made more difficult not only by the lack of a helpful syntax underliner, but also by the typeclasses, which make the errors even more far removed from what you would expect. Not to mention the performance penalties associated with making something too generic, which I didn't think of originally.

Zachary Turner wrote:
it's generally considered good practice to specify the full type of a function before the definition. Why is this? It almost seems to go against the principles of type inference.
Michael Mossey wrote:
...it seems a shame to disregard this power by declaring all types.
I concur with the reasons given by previous responders for why it's important to specify type signatures for top-level functions. I'll add that this practice is not at all against the principles of type inference, and you still use its full power: o for auxiliary functions defined in let and where clauses o for functions defined at the interactive prompt o for quick scripting Type inference provides a powerful technique for investigating how to use various tools in Haskell: you use the :type command at the interactive command prompt (or in our IRC channels) to find out what type is assigned to an expression. Besides these direct usages, the compiler makes essential use of type inference whenever you write any non-trivial expression. You may have specified the type of the final result, but the compiler needs to know the type of every intermediate result. This requires type inference because of the very general kinds of polymorphism that Haskell allows. -Yitz

Zachary Turner wrote:
I'm mostly just trying to understand why it's good in one language, and bad in another. I'm sure there must be a number of tangible advantages in each language, that either don't apply or are mapped to disadvantages in the other.
I do not know about F#, but ML requires type signatures at module boundaries. That does limit how far you can get relying on inference alone. Also, the O'Caml community recommends type annotations for documentation purposes although leaving out the annotations is not uncommon for local values. Finally, with "type" synonyms, type inference sometimes results in equivalent typings that are less useful than an annotation (Parsec is the case I remember). -- Tommy M. McGuire mcguire@crsr.net

On 2009 Mar 23, at 22:02, Zachary Turner wrote:
Everything I've read has said that it's generally considered good practice to specify the full type of a function before the definition. Why is this? It almost seems to go against the principles of type inference. Why let the compiler infer types if you're just going to tell it what types to use for everything? Ok well, not really for everything, you don't typically specify
1. Specifying the type of a top level binding avoids the monomorphism restriction. 2. Type inference is nice right up until you have to debug a type error; then the error gets reported at the point where the compiler realizes it can't match up the types, which could be somewhere not obviously related (depends on what the call chain looks like). The more concrete types you give the compiler, the better (both more complete and more correctly located) the type errors will be. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH

On Mon, Mar 23, 2009 at 9:51 PM, Brandon S. Allbery KF8NH < allbery@ece.cmu.edu> wrote:
On 2009 Mar 23, at 22:02, Zachary Turner wrote:
Everything I've read has said that it's generally considered good practice to specify the full type of a function before the definition. Why is this? It almost seems to go against the principles of type inference. Why let the compiler infer types if you're just going to tell it what types to use for everything? Ok well, not really for everything, you don't typically specify
1. Specifying the type of a top level binding avoids the monomorphism restriction.
2. Type inference is nice right up until you have to debug a type error; then the error gets reported at the point where the compiler realizes it can't match up the types, which could be somewhere not obviously related (depends on what the call chain looks like). The more concrete types you give the compiler, the better (both more complete and more correctly located) the type errors will be.
Regarding the second issue, this occurs in most other type inferring languages as well, but usually you just specify types up until such time that your function is fully tested and you deem that it's good, then removing the type specification. Or, when you get strange type errors, binding a few relevant values to the types you expect, and then the type errors become clearer. Then once you fix them you can remove the type annotations again. Regarding the first issue, I haven't gotten deep enough into Haskell yet to fully appreciate the monomorphism restriction, although I've run into it once I believe. So I'll probably appreciate that aspect of it more later. That being said, is it as common as I expect it would be that the progarmmer unknowingly specifies a type that is not the most general type possible? I would think this would be "bad", although not the end of the world or anything it would still be desirable to be as generic as possible.

On 2009 Mar 23, at 23:02, Zachary Turner wrote:
That being said, is it as common as I expect it would be that the progarmmer unknowingly specifies a type that is not the most general type possible? I would think this would be "bad", although not the end of the world or anything it would still be desirable to be as generic as possible.
One practical consideration is that the more general a function is, the more expensive it could be, either due to lack of optimization or a requirement to look up a typeclass instance at runtime. You can avoid this by using GHC's SPECIALIZE pragma, but in many cases it's best to be just as generic as you require but not more so. The monomorphism restriction is in fact a workaround for a common case of this: a = 5 Looking at that, one might expect its type to be Int, but without the monomorphism restriction it would be Num a => a and force runtime lookups everywhere a is directly or indirectly used. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH

2009/3/24 Zachary Turner
2. Type inference is nice right up until you have to debug a type error; then the error gets reported at the point where the compiler realizes it can't match up the types, which could be somewhere not obviously related (depends on what the call chain looks like). The more concrete types you give the compiler, the better (both more complete and more correctly located) the type errors will be.
Regarding the second issue, this occurs in most other type inferring languages as well, but usually you just specify types up until such time that your function is fully tested and you deem that it's good, then removing the type specification.
This seems perverse to me. The type signature is very good documentation for other people wanting to use the function. Removing it is a very hostile activity.

I'd argue that this is good practice for beginners especially, but as you get to be more practiced, your mileage may vary. Certainly, if you're only writing first-order code, this is perhaps less useful. But the moment you begin to pass around higher-order functions with abandon, it becomes quite useful. Say, for example, that I want to write a function to abstract a data- handling pattern I've noticed. I have a number of records I want to query. Each time, I first restrict them to those where a certain field is present. Then, I sort them by some arbitrary ordering. Finally, I return a list of records grouped by some key, as processed by some combining function. Now there's a bunch of steps there to think through, and I might not even have a good name for the function yet to express what it does, but I can write the type straight off the bat: foo :: (Ord c) => (a -> Maybe b) -> (a -> a -> Ordering) -> (a -> c) -
([a] -> d) -> [d]
This at least begins to articulate the intent of this (admittedly, made up, but not actually all that made-up) function, and for me at least, helps me to think about what to write next. Another way to think about this is sometimes you know the type of the function you want simply from context: say that you have some list of data, and you know you want to express a foldr over it. You may not know where to begin with the function that you want to foldr, but you do know, at least, that it needs to be of type a -> a -> b, and if you figure out what the a is and what the b is, you're much closer to being able to write the function itself. Another advantage of this is that, once you've specified a correct type signature, then rather than having a function that produces something totally off the wall, but which you only realize elsewhere in the program, you'll get a nice helpful type error right at the point where you did something weird. Cheers, S. On Mar 23, 2009, at 10:02 PM, Zachary Turner wrote:
Everything I've read has said that it's generally considered good practice to specify the full type of a function before the definition. Why is this? It almost seems to go against the principles of type inference. Why let the compiler infer types if you're just going to tell it what types to use for everything? Ok well, not really for everything, you don't typically specify types for local bindings, but still why the inconsistency? I have a little experience with ML and F# and there you're encouraged to - not- specify types explicitly, and let the compiler infer them for you. In fact, it seems like it would be fairly common where you specify a type that is -less- general than the type that the compiler would infer for you, because the most general type might involve a combination of type classes used in various ways, and it may not always be obvious to the programmer how to specify it correctly. _______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners

On Mon, Mar 23, 2009 at 09:02:56PM -0500, Zachary Turner wrote:
Everything I've read has said that it's generally considered good practice to specify the full type of a function before the definition. Why is this?
I've written some reasons not too long ago: http://www.haskell.org/pipermail/beginners/2009-February/001045.html Note that catching errors is probably the most useful benefit of writing type signatures. For a simple example, see
-- f :: Int -> Int f n = (n * 45 + 10) / 3
Do you see the problem? I've used (/) while I meant `div`. But, suppose you didn't write any type signature at all, the code would compile just fine with type 'f :: Floating a => a -> a'. Now, in another module you say
-- Type signature needed here to select what Read instance you want getNum :: IO Int getNum = read `fmap` getLine
-- doF :: IO () doF = getNum >>= print . f
Try it for yourself, what error message you get? The usual cryptic one about "Fractional Int" but *in the definition 'doF'*. Your *programmer mistake* propagated to another *module*. That is a bad, bad thing. Whenever you write type signatures, all these kinds of errors get contained inside the function they were written, saving you a lot of time. The second most important benefit probably would be to help you write the function itself. If you can't write the signature of your function, then you can't write your function at all. And it is not uncommon, even among experienced Haskellers, to write a type signature and then realise they were trying to do something completely wrong! Unfortunately I can't give you any example right now, but believe me. -- Felipe.
participants (11)
-
Alexander Dunlap
-
Brandon S. Allbery KF8NH
-
Colin Adams
-
Felipe Lessa
-
Michael Mossey
-
Peter Verswyvelen
-
Sterling Clover
-
Tom Poliquin
-
Tommy M. McGuire
-
Yitzchak Gale
-
Zachary Turner