Best idiom for avoiding Defaulting warnings with ghc -Wall -Werror ??
Hi all, I've been going over my code trying to get it all to compile with "ghc -Wall -Werror", without introducing constructs that would make my code the laughing stock of the dynamic typing community. They already think we're nuts; my daydreams are of a more computer literate society where Jessie Helms stands up in the U.S. Senate to read aloud my type declarations to the derisive laughter of the Ruby and Lisp parties. There's a fine line between my opinion as to how GHC should issue warnings, and a legitimate bug report. I've already submitted a bug report for the need to declare the type of the wildcard pattern, because I believe that the case is clear. Here, I'm seeking guidance. Perhaps I just don't know the most elegant construct to use? My sample code is this:
{-# OPTIONS_GHC -Wall -Werror #-}
module Main where
import Prelude hiding ((^)) import qualified Prelude ((^))
default (Int)
infixr 8 ^ (^) :: Num a => a -> Int -> a x ^ n = x Prelude.^ n
main :: IO () main = let r = pi :: Double x = r ^ (3 :: Int) y = r ^ 3 z = r Prelude.^ 3 in putStrLn $ show (x,y,z)
GHC issues a "Warning: Defaulting the following constraint(s) to type `Int'" for the definition of z. The definition of y glides through, so a qualified import and redefinition of each ambiguous operator does provide a work-around, but the code is lame. (I could always encapsulate it in a module Qualude.) If I import a module that I don't use, then "ghc -Wall -Werror" rightly complains. By analogy, if I use "default (Int)" to ask GHC to default to Int but the situation never arises, then GHC should rightly complain. Instead, if I use "default (Int)", GHC complains about defaulting anyways. In my opinion, this is a bug, but I'd like guidance before reporting it. Is there a more elegant way to handle the numeric type classes with "ghc -Wall -Werror" ? No one is forced to use "ghc -Wall -Werror", but it should be a practical choice. I've enjoyed the recent typing discussions here. On one hand, there's little difference between using dynamic typing, and writing incomplete patterns in a strongly typed language. On the other hand, how is an incomplete pattern any different from code that potentially divides by zero? One quickly gets into decidability issues, dependent types, Turing-complete type systems. My personal compromise is to use "ghc -Wall -Werror", live with the consequences, and get back to work. Perhaps I'll get over it, but that's a slippery slope back to Lisp.
On Fri, Jun 22, 2007 at 11:37:15AM -0700, Dave Bayer wrote:
GHC issues a "Warning: Defaulting the following constraint(s) to type `Int'" for the definition of z.
Why don't you just use -fno-warn-type-defaults? Warnings are just that: warnings. If you believe the defaulting matches what you want to do, then you don't need the warning. ghc -Werr -Wall is a often good idea, but if you prefer a different programming style (e.g. no top-level type declarations required), ghc gives you the flexibility to do that. -- David Roundy Department of Physics Oregon State University
On Jun 22, 2007, at 11:42 AM, David Roundy wrote:
On Fri, Jun 22, 2007 at 11:37:15AM -0700, Dave Bayer wrote:
GHC issues a "Warning: Defaulting the following constraint(s) to type `Int'" for the definition of z.
Why don't you just use -fno-warn-type-defaults? ... ghc -Werr -Wall is a often good idea, but if you prefer a different programming style (e.g. no top-level type declarations required), ghc gives you the flexibility to do that.
To be precise, I __PREFER__ a "ghc -Wall -Werror" programming style. In particular, I always want defaulting errors, because sometimes I miss the fact that numbers I can count on my fingers are defaulting to Integer. Once I explicitly declare "default (Int)", I want "ghc -Wall - Werror" to shut up, unless this defaulting rule never gets used. Instead, it complains anyways when the defaulting takes place that I've just declared I know about. In other words, I want warnings involving "default" to follow the same logic currently used for warnings involving "import". This is a bug. I want "ghc -Wall -Werror" to be a practical choice, left on all the time, and in my example I had to work too hard to avoid the warning. Other people just wouldn't use "ghc -Wall - Werror", the way some people won't use seat belts, and the way some people view any strongly typed language as a cumbersome seat belt. If we tolerate ridiculously arcane syntax to handle these situations, we fully deserve to be marginalized while Ruby takes over the world. In other words, I'm disputing that the top-level declarations are in fact required. GHC can be trivially modified to allow Haskell to handle this situation far more elegantly. (It is amusing the sides we're taking on this, and the stereotype that physicists compute faster than mathematicians because they don't worry about convergence issues. Effectively, the stereotype holds that mathematicians think with "-Wall -Werror" on, and physicists don't. Perhaps it's true?)
On Fri, Jun 22, 2007 at 12:34:09PM -0700, Dave Bayer wrote:
On Jun 22, 2007, at 11:42 AM, David Roundy wrote:
On Fri, Jun 22, 2007 at 11:37:15AM -0700, Dave Bayer wrote:
GHC issues a "Warning: Defaulting the following constraint(s) to type `Int'" for the definition of z.
Why don't you just use -fno-warn-type-defaults? ... ghc -Werr -Wall is a often good idea, but if you prefer a different programming style (e.g. no top-level type declarations required), ghc gives you the flexibility to do that.
To be precise, I __PREFER__ a "ghc -Wall -Werror" programming style. In particular, I always want defaulting errors, because sometimes I miss the fact that numbers I can count on my fingers are defaulting to Integer.
Once I explicitly declare "default (Int)", I want "ghc -Wall - Werror" to shut up, unless this defaulting rule never gets used. Instead, it complains anyways when the defaulting takes place that I've just declared I know about. In other words, I want warnings involving "default" to follow the same logic currently used for warnings involving "import".
I see, that makes sense. And I have no idea that would help you.
This is a bug. I want "ghc -Wall -Werror" to be a practical choice, left on all the time, and in my example I had to work too hard to avoid the warning. Other people just wouldn't use "ghc -Wall - Werror", the way some people won't use seat belts, and the way some people view any strongly typed language as a cumbersome seat belt. If we tolerate ridiculously arcane syntax to handle these situations, we fully deserve to be marginalized while Ruby takes over the world.
In other words, I'm disputing that the top-level declarations are in fact required. GHC can be trivially modified to allow Haskell to handle this situation far more elegantly.
I think of top-level type declarations as type-checked comments, rather than a seat-belt. It forces you to communicate to others what a function does, if that function may be used elsewhere. I like this. Although it can be cumbersome for quick and dirty code, developers trying to read your code will thank you for it (unless you make *everything* top-level, which is just poor coding style). -Wall -Werror isn't a seat belt, it's a coding-style guideline. -- David Roundy Department of Physics Oregon State University
On Jun 22, 2007, at 2:46 PM, David Roundy wrote:
I think of top-level type declarations as type-checked comments, rather than a seat-belt. It forces you to communicate to others what a function does, if that function may be used elsewhere. I like this. Although it can be cumbersome for quick and dirty code, developers trying to read your code will thank you for it (unless you make *everything* top-level, which is just poor coding style).
-Wall -Werror isn't a seat belt, it's a coding-style guideline.
I don't think one can make blanket statements as to what type systems "are for". I doubt that the people who've dedicated their lives to type theory are doing so to provide style guidelines. I like the quick and open-ended definition that types are compile- time proxies for run-time values. It happens that current type systems are closely tied to propositional logic, because so many logicians are drawn to the work. This need not be the case. From this point of view, one pays attention to type theory because one produces the best code by providing the best guidance to the compiler. -Wall -Werror is establishing a contract to do so.
On Fri, Jun 22, 2007 at 03:07:59PM -0700, Dave Bayer wrote:
On Jun 22, 2007, at 2:46 PM, David Roundy wrote:
I think of top-level type declarations as type-checked comments, rather than a seat-belt. It forces you to communicate to others what a function does, if that function may be used elsewhere. I like this. Although it can be cumbersome for quick and dirty code, developers trying to read your code will thank you for it (unless you make *everything* top-level, which is just poor coding style).
-Wall -Werror isn't a seat belt, it's a coding-style guideline.
I don't think one can make blanket statements as to what type systems "are for". I doubt that the people who've dedicated their lives to type theory are doing so to provide style guidelines.
-Wall doesn't flag type errors, and really has little to do with type systems. It's a set of heuristics describing for what someone considers poor programming practices. I agree that type systems are much more than that, that wasn't what (I thought) we were talking about. You get strongly-typed code whether or not you enable warnings. And regarding my above statement about top-level type declarations, that's about the declarations, not the type system. They have no effect on the code that's generated (except in occasional rare cases, where they allow the compiler to do more optimizations), but they do allow you to get better error messages, and they communicate your intent to code readers. I see the latter as the better reason to always include top-level type declarations. -- David Roundy Department of Physics Oregon State University
On Jun 22, 2007, at 4:37 PM, David Roundy wrote:
You get strongly-typed code whether or not you enable warnings.
In my opinion it's delusional to think one is using strong typing if one doesn't enable warnings. All the puffing about the advantages of strong typing look pretty silly if code hangs up on an incomplete pattern. Let's remember that the other side of this debate is rather eloquent, be it Paul Graham or a Ruby enthusiast. People who don't worry so much about types believe that they get things done. Is using a strongly typed language like buying a hybrid car, it costs too much but you're helping with "maybe someday...?" I refuse to drink the Kool-Aid and recite precisely what I'm told a type is in June, 2007; I'm hoping that types will evolve by the time I die. For types to evolves, we need to step back a few feet and think more loosely what a type really is. If someone writes working code with incomplete patterns, they're effectively using a dependent type without being able to say so in Haskell. They're using a specialization of the type they claim to be using, in which the missing patterns are never needed. Filling in with _ -> error "I'm sweeping this under the rug so it's no longer the type system's problem" just highlights the inadequacy of the type system. The code hangs either way, if the belief that this case doesn't happen is wrong. I'm more of a "Will the code hang or not?" kind of guy than "Will I be kicked out of the tree house if I use the wrong words for things?" kind of guy. The missing pattern that shouldn't happen is abstractly a type issue, whether we can get the compiler to lay off or not. Similarly, the whole defaulting debate is good form/bad form considerations for how best to use types to automatically write code for us. It all comes back to what I said before, types are compile-time proxies for run-time values. I'm nudging at compile-time, therefore I'm messing with types, not values. If I go away and write in Lisp or Ruby, then return to Haskell with "ghc -Wall -Werror", it is glaringly obvious to me that the nudging I have to do to get things to work with warnings on has to do with types. I truly don't mind the nudging, it is very educational, but let's call a spade a spade?
On Fri, 2007-06-22 at 17:39 -0700, Dave Bayer wrote:
On Jun 22, 2007, at 4:37 PM, David Roundy wrote:
You get strongly-typed code whether or not you enable warnings.
In my opinion it's delusional to think one is using strong typing if one doesn't enable warnings. All the puffing about the advantages of strong typing look pretty silly if code hangs up on an incomplete pattern. Let's remember that the other side of this debate is rather eloquent, be it Paul Graham or a Ruby enthusiast. People who don't worry so much about types believe that they get things done. Is using a strongly typed language like buying a hybrid car, it costs too much but you're helping with "maybe someday...?"
Okay... people who don't worry so much about incomplete patterns believe that they get things done. There are trade offs in type systems about how much effort you want to require of the user and how much the type system will catch. Haskell's type system is at a point that does a lot with very little. You can do ridiculously more if you don't mind requiring more from the user.
I refuse to drink the Kool-Aid and recite precisely what I'm told a type is in June, 2007; I'm hoping that types will evolve by the time I die. For types to evolves, we need to step back a few feet and think more loosely what a type really is.
If someone writes working code with incomplete patterns, they're effectively using a dependent type without being able to say so in Haskell. They're using a specialization of the type they claim to be using, in which the missing patterns are never needed. Filling in with
_ -> error "I'm sweeping this under the rug so it's no longer the type system's problem"
just highlights the inadequacy of the type system.
It's not an inadequacy, it's a trade off, but if you want, Epigram is right over there.
Hi
All the puffing about the advantages of strong typing look pretty silly if code hangs up on an incomplete pattern.
Okay... people who don't worry so much about incomplete patterns believe that they get things done.
There are trade offs in type systems about how much effort you want to require of the user and how much the type system will catch. Haskell's type system is at a point that does a lot with very little. You can do ridiculously more if you don't mind requiring more from the user.
I know Catch got mentioned at the beginning of this thread, but it does read like an advert for Catch :) You can have existing Haskell with no annotations that is proven free from pattern-match errors automatically. You can do the trick of saying error "this branch cannot be reached", then Catch will validate that you are correct. http://www-users.cs.york.ac.uk/~ndm/catch/ Thanks Neil
On Fri, Jun 22, 2007 at 05:39:10PM -0700, Dave Bayer wrote:
On Jun 22, 2007, at 4:37 PM, David Roundy wrote:
You get strongly-typed code whether or not you enable warnings.
In my opinion it's delusional to think one is using strong typing if one doesn't enable warnings. All the puffing about the advantages of strong typing look pretty silly if code hangs up on an incomplete pattern. Let's remember that the other side of this debate is rather eloquent, be it Paul Graham or a Ruby enthusiast. People who don't worry so much about types believe that they get things done. Is using a strongly typed language like buying a hybrid car, it costs too much but you're helping with "maybe someday...?"
Depends on the definition of strong typing, I suppose. I'd say that using the conventional definition is reasonable, rather than using the definition which defines strong typing to mean some language that hasn't ever been written. Enabling warnings gains you some protection, but you need a new language (lacking head, tail, error, etc) if you want to statically avoid all runtime errors. It's silly to claim or believe that "strong typing" means that code which type-checks cannot fail. Maybe such a language exists, but I haven't heard of it.
I refuse to drink the Kool-Aid and recite precisely what I'm told a type is in June, 2007; I'm hoping that types will evolve by the time I die. For types to evolves, we need to step back a few feet and think more loosely what a type really is.
When talking about Haskell on Haskell mailing lists, it makes communication easier if you use Haskell terminology. e.g. when you use the word type, if you mean the thing that is called a type in the Haskell language.
If someone writes working code with incomplete patterns, they're effectively using a dependent type without being able to say so in Haskell. [...]
So what you're talking about is that Haskell doesn't have a type that is capable of describing a total function? That any function can return bottom? That would definitely be nice to have. As I understand it, in Haskell non-termination is considered bottom (the result of error or failed pattern matches), and I don't see how we could avoid all non-terminating code in the type system (I believe that's known to be undecideable?), so what you want is to get rid of the existence of error? ...which I believe is what pattern match failure desugar to. That's be nice in many ways, but I suspect it would reduce once again the number of correct programs that could be written. -- David Roundy http://www.darcs.net
On Sat, 23 Jun 2007, David Roundy wrote:
I refuse to drink the Kool-Aid and recite precisely what I'm told a type is in June, 2007; I'm hoping that types will evolve by the time I die. For types to evolves, we need to step back a few feet and think more loosely what a type really is.
When talking about Haskell on Haskell mailing lists, it makes communication easier if you use Haskell terminology. e.g. when you use the word type, if you mean the thing that is called a type in the Haskell language.
This means people cannot talk about future developments of type theory here ...
On Jun 22, 2007, at 17:46 , David Roundy wrote:
-Wall -Werror isn't a seat belt, it's a coding-style guideline.
So, as long as we're on this topic... I have a program which I'm checking with -Wall but not -Werror, because it has several pattern matches which *I* know are fine but which ghc doesn't. (I suspect, from its description, that Catch would also recognize it's fine.) Which leads me to wonder: (1) any way to flag a pattern match as "I know this is okay", don't warn about it" without shutting off pattern match warnings completely? (2) any way that, given the need to roll a bunch of records into a single type, I can somehow declare things such that calling one of these functions that expects only a single component record type with a different record type raises a *compile-time* error? (That is, roughly the opposite of the usual pattern match error behavior.) Unfortunately I can't split the records into independent types because the full record type controls a state machine and different states require different components, and I can't use a typeclass to do it because you can't declare a list of a typeclass (VRow r) => [r]. (Yes, this may become an array later, but it's only 25 or so entries.) The special cases are where I'm asking the state machine to do lookups from "files" that are actually things like DNS lookups. Some of these are passed file-based lookups in order to modify the DNS lookup's result (domain stripping, for example) and these will (a) never be invoked with a lookup type other than VDNS and (b) never be handed a VProcess-based VLookup or a VDNS as the modifier. -- 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 Fri, Jun 22, 2007 at 06:11:24PM -0400, Brandon S. Allbery KF8NH wrote:
(1) any way to flag a pattern match as "I know this is okay", don't warn about it" without shutting off pattern match warnings completely?
case scrutinee of Pattern -> alternative Pattern -> alternative _ -> error "Can't happen in functionname" Stefan
On Fri, Jun 22, 2007 at 03:14:06PM -0700, Stefan O'Rear wrote:
On Fri, Jun 22, 2007 at 06:11:24PM -0400, Brandon S. Allbery KF8NH wrote:
(1) any way to flag a pattern match as "I know this is okay", don't warn about it" without shutting off pattern match warnings completely?
case scrutinee of Pattern -> alternative Pattern -> alternative _ -> error "Can't happen in functionname"
darcs has an "impossible" C-preprocessor macro that we use for this, which uses __FILE__ and __LINE__ to automatically give a useful (to developers) error message if it turns out that the case was possible after all. -- David Roundy http://www.darcs.net
On Fri, 22 Jun 2007, Brandon S. Allbery KF8NH wrote:
I have a program which I'm checking with -Wall but not -Werror, because it has several pattern matches which *I* know are fine but which ghc doesn't. (I suspect, from its description, that Catch would also recognize it's fine.) Which leads me to wonder:
(1) any way to flag a pattern match as "I know this is okay", don't warn about it" without shutting off pattern match warnings completely?
Add the "catch all" case with '_': f _ = error "this case cannot occur, because this would violate the invariant X" If the error occurs anyway, you get a report that your believe was wrong. (Or the user gets the report, and he doesn't know how to react.)
On Sat, 2007-06-23 at 00:29 +0200, Henning Thielemann wrote:
On Fri, 22 Jun 2007, Brandon S. Allbery KF8NH wrote:
I have a program which I'm checking with -Wall but not -Werror, because it has several pattern matches which *I* know are fine but which ghc doesn't. (I suspect, from its description, that Catch would also recognize it's fine.) Which leads me to wonder:
(1) any way to flag a pattern match as "I know this is okay", don't warn about it" without shutting off pattern match warnings completely?
Add the "catch all" case with '_':
f _ = error "this case cannot occur, because this would violate the invariant X"
If the error occurs anyway, you get a report that your believe was wrong. (Or the user gets the report, and he doesn't know how to react.)
Sure he does. Irately tell you that your program doesn't work and then, upon repeated prompting and guidance, provide you with said error message.
On Jun 22, 2007, at 18:29 , Henning Thielemann wrote:
If the error occurs anyway, you get a report that your believe was wrong. (Or the user gets the report, and he doesn't know how to react.)
Well, that's why I included the other leg, where I'd like the compiler to catch me at compile time if I set up a situation where it might occur --- because ideally that case can't happen at run time, but if I set up the types that way then I can't build the state machine because it's a polymorphic list. (And no, I don't think HList is the right answer here.) -- 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 Jun 22, 2007, at 3:11 PM, Brandon S. Allbery KF8NH wrote:
(1) any way to flag a pattern match as "I know this is okay", don't warn about it" without shutting off pattern match warnings completely?
GHC doesn't issue warnings about patterns on the left of = For example, the following code compiles just fine with ghc -Wall - Werror, but the use of "Just m" generates a run-time exception:
module Main where
a :: [(Int,Int)] a = [(2*n,n) | n <- [1..100]]
m :: Int Just m = lookup 3 a
main :: IO () main = putStrLn $ show m
I'd take this as a ghc feature, not a bug. When I use this construct in practice, I have a proof in mind that the pattern match cannot fail for my data, but I can't express the proof in Haskell's type system. I'm ok with skipping writing that proof. The difference here is programmer intent. While a missing pattern case can often be an oversight, there's no way to put both cases here to the left of =, so the programmer clearly intends this code as written. (An example of a language with a Turing complete type system is Qi: http://www.lambdassociates.org/ As pointed out elsewhere in this thread, it is unreasonable/ undecidable to expect a type system to work out arbitrarily difficult issues for you automatically. Some work is required, programming in the type system. They extend this point of view.)
On Jun 22, 2007, at 12:34 PM, Dave Bayer wrote:
In particular, I always want defaulting errors, because sometimes I miss the fact that numbers I can count on my fingers are defaulting to Integer.
So no one took the bait to actually offer me a shorter idiom, but I thought about the above sentence, and had a big Homer Simpson "Doh!" revelation. In the acual code I was cleaning up, just write out the exponentiations, for example,
evalBezier :: R -> Bezier -> [R] evalBezier t b = let s = 1-t in case b of Line x y -> s*.x .+. t*.y Cubic w x y z -> s*s*s*.w .+. 3*s*s*t*.x .+. 3*s*t*t*.y .+. t*t*t*.z
To my taste, that's much prettier than half a dozen lines of declarations to get ^ to behave with ghc -Wall -Werror, and after all I'm just hand-unrolling the code for ^.
On Fri, 22 Jun 2007, Dave Bayer wrote:
If I import a module that I don't use, then "ghc -Wall -Werror" rightly complains. By analogy, if I use "default (Int)" to ask GHC to default to Int but the situation never arises, then GHC should rightly complain. Instead, if I use "default (Int)", GHC complains about defaulting anyways. In my opinion, this is a bug, but I'd like guidance before reporting it. Is there a more elegant way to handle the numeric type classes with "ghc -Wall -Werror" ?
My understanding of defaulting is that it is bad style to rely on it. It is mostly needed for working in GHCi. For the particular exponentiation issue, I found the following: The overwhelming part of constant exponents of (^) in my modules is 2. The defaulting is mostly relevant for number literals, whereas variables get their types from somewhere else. So you may consider implementing a 'sqr' function for squaring values.
Dave Bayer wrote:
I've enjoyed the recent typing discussions here. On one hand, there's little difference between using dynamic typing, and writing incomplete patterns in a strongly typed language. On the other hand, how is an incomplete pattern any different from code that potentially divides by zero? One quickly gets into decidability issues, dependent types, Turing-complete type systems.
True enough, in a sense, a dynamically typed language is like a statically typed language with only one type (probably several by distinguishing function types) and many incomplete pattern matches. So, you can embed a dynamically typed language into a strongly typed language without loosing static type checking. However, the other way round is impossible: virtually void of static type checking, the dynamic language is incapable of embedding a strongly typed language without loosing type safety. Thus, you still gain something with strong typing even with incomplete pattern matches. In fact, the programmer has the power to arrange things such that he gains extremely much. What about throwing out incomplete patterns completely? Well, this is a very mixed blessing. There are incomplete patterns and non-terminating programs, both commonly denoted with _|_. As long as you allow non-termination, you can't get rid of incomplete patterns. But enforcing termination everywhere can be very limiting: 1) The programmer has to detail in some form the proof that his program terminates. Arguably, he ought to do so anyway but he doesn't need to write his proof in a way that can be checked by a dumb computer. Take for example minimum = head . sort Here, the theorem that this program proves is obvious from the proof itself. But to make it checkable by a machine, I'm sure that further type annotations are needed that don't add additional insight anymore. 2) There are programs that terminate but cannot be stated in a given always-terminating language. Most likely, an interpreter for this language is one of those programs. Getting rid of incomplete patterns means to rule out terms that do not fulfill a given invariant. Dependent types are a good way too that, but again, you have issue 1). The proofs will only be tractable if it's possible to concentrate on the interesting invariants and drop the others. In the end, strongly normalizing languages and dependent types are an active research area for exactly these problems. In the end, I think that strong types is only one thing that makes Haskell programs work after compilation. The other ones are higher-order functions and *purity*. No type system can achieve what purity offers. Regards, apfelmus
Hi
1) The programmer has to detail in some form the proof that his program terminates. Arguably, he ought to do so anyway but he doesn't need to write his proof in a way that can be checked by a dumb computer. Take for example
minimum = head . sort
minimum [1..] gives _|_ non-termination miniumum [1,_|_,3] gives _|_ while head [1,_|_,3] doesn't. Termination is all a bit more complex once you get to laziness. Thanks Neil
Neil Mitchell wrote:
1) The programmer has to detail in some form the proof that his program terminates. Arguably, he ought to do so anyway but he doesn't need to write his proof in a way that can be checked by a dumb computer. Take for example
minimum = head . sort
minimum [1..] gives _|_ non-termination
miniumum [1,_|_,3] gives _|_ while head [1,_|_,3] doesn't.
Termination is all a bit more complex once you get to laziness.
Oops, the example was not meant for termination but for the invariants. I wanted to say that the code of minimum is likely to be shorter than a computer-checkable proof that shows that its result is indeed the smallest element from the list. Regards, apfelmus
True enough, in a sense, a dynamically typed language is like a statically typed language with only one type (probably several by distinguishing function types) and many incomplete pattern matches. So, you can embed a dynamically typed language into a strongly typed language without loosing static type checking.
statically typed: typed at compile time dynamically typed: typed at runtime weakly typed: .. strongly typed: everything is typed and type-checked there are at least two problems with embedding strongly and dynamically typed languages into strongly and statically typed languages: - it assumes that there is a globally unique static stage, entirely separate from a globally unique dynamic stage - it assumes that there is a unique, unchanging (closed) world of types static typing alone is too static to deal with dynamically evolving types or flexible ideas such as runtime compilation or dynamic linking.. the solution is long-known as type Dynamic (a universal type in which expressions are paired with type tags): projecting from a Dynamic to the tag type (using a typecase) involves a 'static' type check prior to stripping the type info away for a limited 'runtime', embedding into a Dynamic involves creating a runtime type tag, to prepare for situations that can't be handled statically. if you have a strongly and otherwise statically typed language extended with Dynamic/typecase, you can embed strongly and dynamically typed languages into it. and you can try to reduce the number of Dynamic and typecase uses to a minimum, giving you maximal phases of pre-checked runtime without dynamic type representations or type checks. but there are situations that need Dynamic/typecase. if you have a strongly and dynamically typed language, you can embed strongly and statically typed languages into it. by default, that means you get more type-checks than necessary and type-errors later than you'd wish, but you still get them. eliminating runtime type information and runtime type-checks in a strongly and dynamically typed language is a question of optimisation, similar to deforestation. if you have a strongly and statically typed language, there are situations where you'll get stuck. extending the type system may get you beyond some of these barriers, but only to the next set of problems. it is impressive just how far languages like haskell have managed to take the idea of strong static typing, and it is worthwhile noting that many people need nothing more most of the time. it is also worthwhile recalling that the struggle involved has given us type systems that can handle many of the problems that were thought to be dynamic in nature within a static type system (such as generic programming). but there always remains a small set of essential problems that exceed what strong static typing can handle on its own. adding Dynamic/typecase gives you the best of both worlds: the expressiveness of strongly and dynamically typed languages and the efficiency and early safety (between a typecase and a reembedding into Dynamic, there will be no runtime type-checks and no runtime type-errors) of strongly and statically typed languages. even better, for the large number of programs that do not need dynamic types, there'll be no sign of them - those programs work in the strongly and statically typed subset of the language. claus
Claus Reinke wrote:
apfelmus wrote:
True enough, in a sense, a dynamically typed language is like a statically typed language with only one type (probably several by distinguishing function types) and many incomplete pattern matches. So, you can embed a dynamically typed language into a strongly typed language without loosing static type checking.
statically typed: typed at compile time dynamically typed: typed at runtime
weakly typed: .. strongly typed: everything is typed and type-checked
Ah, thanks for the clear terminology.
there are at least two problems with embedding strongly and dynamically typed languages into strongly and statically typed languages:
- it assumes that there is a globally unique static stage, entirely separate from a globally unique dynamic stage - it assumes that there is a unique, unchanging (closed) world of types
static typing alone is too static to deal with dynamically evolving types or flexible ideas such as runtime compilation or dynamic linking..
the solution is long-known as type Dynamic
Yes, that's what I meant. The "embedding" is a rather degenerate one, making everything to be of type Dynamic.
if you have a strongly and dynamically typed language, you can embed strongly and statically typed languages into it. by default, that means you get more type-checks than necessary and type-errors later than you'd wish, but you still get them. eliminating runtime type information and runtime type-checks in a strongly and dynamically typed language is a question of optimisation, similar to deforestation.
Well, you can't embed the static checks into dynamic checks without loosing the fact that they're static. Which I think is the crucial point: "program testing can be used very effectively to show the presence of [type] bugs but never to show their absence." To me, dynamic typing is next to useless, i want a (partial) proof that the program works since a proof is really the only way to know whether it works. Regards, apfelmus
On Sun, 2007-06-24 at 13:33 +0100, Claus Reinke wrote:
if you have a strongly and dynamically typed language, you can embed strongly and statically typed languages into it. by default, that means you get more type-checks than necessary and type-errors later than you'd wish, but you still get them.
Are you sure this is true in a meaningful way? You can always simply run the type checker at run-time, and this is indeed where statically typed languages are heading, but e.g. phantom types, and runST style tricks are areas where the embedding into a dynamically typed language is, at the very least, not trivial.
if you have a strongly and dynamically typed language, you can embed strongly and statically typed languages into it. by default, that means you get more type-checks than necessary and type-errors later than you'd wish, but you still get them.
Are you sure this is true in a meaningful way? You can always simply run the type checker at run-time, and this is indeed where statically typed languages are heading, but e.g. phantom types, and runST style tricks are areas where the embedding into a dynamically typed language is, at the very least, not trivial.
true, meaningful, yes; you'd still not be able to access ST references in the wrong thread, but in a purely dynamically typed language, you will only find out about problems in that area while the thread is already in the middle of its run. runST alone does not give transaction semantics. but it is also true that being able to isolate whole sub-programs at once, so that their type-checks are done before they are being run, and no type-checks are done while those sub-programs are run, is more than just an optimisation. it is a question of being able to express certain type-check-level transaction constraints: either the whole sub-program can be shown to run without type-errors or no part of the sub-program is permitted to run. (being able to fit a whole program into a single such type-level transaction is a special case, which we call static typing) see also apfelmus' message, which raised the same point, and my reply. that exchange reminded me that dynamic/typecase is not only a necessary addition to otherwise static typing, but also enables a very desirable addition to otherwise dynamic typing. the idea being that by default, all typing should be static, unless explicitly specified otherwise by use of dynamic/typecase. in other words, dynamic typing has to be made explicit, and is only used were static typing is not expressive enough; the majority of code consists of statically typed fragments enjoying the type-level transaction property; entry into such a fragment is protected by a dynamic type check, exit from such a fragment might reconstruct dynamic type information. claus
The intention is that it should be straightforward to suppress warnings. Warning about defaulting is important, because it's a place where a silent choice affects the dynamic semantics of your program. You can suppress the warning by supplying a type signature. In your example: | > main = | > let r = pi :: Double | > x = r ^ (3 :: Int) | > y = r ^ 3 | > z = r Prelude.^ 3 | > in putStrLn $ show (x,y,z) Simply add a type signature for 'z', or for the naked 3 in z's definition. I think it matters what type is chosen, because it affects the output of the program; it's good practice to be explicit about what type you want, at each site where defaulting is applied. If your idea of good practice differs from mine, then you can record your choice by using -fno-warn-type-defaults. Simon
On Jun 25, 2007, at 4:48 AM, Simon Peyton-Jones wrote:
The intention is that it should be straightforward to suppress warnings.
Simply add a type signature for 'z', or for the naked 3 in z's definition.
I constructed my example from larger modules peppered with small integer constants; such signatures would become a significant percentage of the code. I was hoping for a solution whose code size is at worst linear in the number of distinct integer constants used, not the number of times they are used. I'd like to avoid redefining operators if I can help it. Given that there are entire languages in common use that don't support Integer, I don't see why "ghc -Wall -Werror" can't become such a language when it sees
default (Int)
Instead it issues defaulting warnings even in the presence of this declaration. I couldn't find a way to add a type signature once for each small integer constant I plan to use; it would appear to me that
2,3 :: Int
by itself is not legal Haskell. The best I can do is to instead write
i2,i3 :: Int (i2,i3) = (2,3)
which imposes a per-use penalty of one character per use, and is less readable than simply unrolling the constants in each use. In other words, if I can't write x^3, I find x*x*x more transparent than x^i3 or x^(3::Int). Despite my participation in a broader discussion, my hope in starting this thread was to understand how to most elegantly use the specific programming language "ghc -Wall -Werror". It continues to appear to me that "ghc -Wall -Werror" doesn't support small Int constants without a per-use penalty, measured in code length. On Jun 25, 2007, at 4:48 AM, Simon Peyton-Jones wrote:
I think it matters what type is chosen, because it affects the output of the program; it's good practice to be explicit about what type you want, at each site where defaulting is applied.
I agree, so I'm glad I asked here rather than reporting warnings in the presence of "default (Int)" as a bug. Unless I misunderstand and it is already possible, I'd now prefer a language extension that allows the explicit declarations
2,3 :: Int
once for each affected numeric literal.
| Unless I misunderstand and it is already possible, I'd now prefer a | language extension that allows the explicit declarations | | > 2,3 :: Int | | once for each affected numeric literal. i2 = 2 :: Int i3 = 3 :: Int S
On Jun 25, 2007, at 8:15 AM, Simon Peyton-Jones wrote:
i2 = 2 :: Int i3 = 3 :: Int
The code
{-# OPTIONS_GHC -Wall -Werror #-}
module Main where
i2 = 2 :: Int i3 = 3 :: Int
main :: IO () main = putStrLn $ show (i2,i3)
generates the errors
Main.hs:5:0: Warning: Definition but no type signature for `i2' Main.hs:6:0: Warning: Definition but no type signature for `i3'
and imposes a linear per-use penalty of one extra character per use. If I can't write x^3, I find x*x*x more transparent than x^i3. I know how to fix this; my previous message considered
i2,i3 :: Int (i2,i3) = (2,3)
which still imposes a linear per-use penalty of one extra character per use. It continues to appear to me that "ghc -Wall -Werror" doesn't support small Int constants without a per-use penalty, measured in code length. Am I the only one blessed/cursed with a vision of how proponents of "practical" languages would have a field day with this? Perhaps I'm reading too many blogs.
On Mon, Jun 25, 2007 at 08:53:18AM -0700, Dave Bayer wrote:
It continues to appear to me that "ghc -Wall -Werror" doesn't support small Int constants without a per-use penalty, measured in code length.
Why not use "ghc -Wall -Werror -fno-warn-defaulting", maybe with default(Int)? It removes the potential problems that justified coding the warning, and turns off the warning. By the way, using Integer for exponents really shouldn't be less efficient - but it seems it is. The code for (^) should be something like this: {-# INLINE ^ #-} n ^ m = case toInteger m of S# i -> powerInt# n i J# a p -> powerGmp n a p (With powerInt# and powerGmp specialized on various types of n, when there is something to gain). Then the standard optimizations (inlining, static instance selection, more inlining, and case of constructor) should turn n^3 into the same code whether 3 is Int or Integer. Perhaps GHC.Real needs to be sprinkled with more pragmas.
Am I the only one blessed/cursed with a vision of how proponents of "practical" languages would have a field day with this? Perhaps I'm reading too many blogs.
Seeing as it only happens if you specifically ask the compiler to be as annoying as possible, no reasonable person should take this much farther than complaining about the GHC warning options. After all, the type system and purity we claim are generally good things are still around whatever options you pass, and none of the justifications for them have much to say one way or the other on this sort of compiler warning. I think nobody will argue if you suggest GHC shouldn't complain about defaulting if only one of the candidate types is actually usable. It's rather like typeclasses with -fallow-overlapping-instaces. Brandon
| By the way, using Integer for exponents really shouldn't be less | efficient - | but it seems it is. | | The code for (^) should be something like this: | | {-# INLINE ^ #-} | n ^ m = case toInteger m of | S# i -> powerInt# n i | J# a p -> powerGmp n a p I've done something like this now. Simon
I've been going over my code trying to get it all to compile with "ghc -Wall -Werror"
I recently ran across what may be a good reason not to use -Wall in combination with -Werror (and similar combinations in other compilers), at least not as the standard build switches for software you intend to distribute. It causes bitrot, because -Wall will in the future turn on warnings that don't even exist yet today, and -Werror will turn those warnings into errors. The upshot is that you can write code that entirely follows the standard that defines whatever language you're using (e.g. Haskell 98), and still have it break in the future, even if future compilers adhere to the standard. If you are serious about writing portable and durable code, you may want to avoid this. (I ran into this problem while trying to resurrect an excellent but unmaintained compiler written in lots of OCaml and a little C. Both ocaml and gcc have grown many new warnings in the last few years.) -- /jaap
On Fri, Jun 22, 2007 at 11:37:15AM -0700, Dave Bayer wrote:
z = r Prelude.^ 3
I don't know if (^) in particular is what is causing you problems, but IMO it has the wrong type; just as we have (!!) :: [a] -> Int -> a genericIndex :: (Integral b) => [a] -> b -> a we should also have (^) :: (Num a) => a -> Int -> a genericPower :: (Num a, Integral b) => a -> b -> a (or some other function name). I've mentioned this before, but until http://hackage.haskell.org/trac/haskell-prime/ticket/118 is resolved we don't know where to discuss it (the haskell-prime or libraries list). Incidentally, I am another person who wants to be warned when defaulting happens because I don't want to actually use defaulting, but I would have no objection to the warning being suppressed if someone has explicitly given a "default" declaration (and thus, presumably, does want to use defaulting). Thanks Ian
On Mon, Jun 25, 2007 at 07:31:09PM +0100, Ian Lynagh wrote:
I don't know if (^) in particular is what is causing you problems, but IMO it has the wrong type; just as we have (!!) :: [a] -> Int -> a genericIndex :: (Integral b) => [a] -> b -> a we should also have (^) :: (Num a) => a -> Int -> a genericPower :: (Num a, Integral b) => a -> b -> a (or some other function name).
I've mentioned this before, but until http://hackage.haskell.org/trac/haskell-prime/ticket/118 is resolved we don't know where to discuss it (the haskell-prime or libraries list).
That would be great! -- David Roundy Department of Physics Oregon State University
On Mon, Jun 25, 2007 at 07:31:09PM +0100, Ian Lynagh wrote:
I don't know if (^) in particular is what is causing you problems, but IMO it has the wrong type; just as we have (!!) :: [a] -> Int -> a genericIndex :: (Integral b) => [a] -> b -> a we should also have (^) :: (Num a) => a -> Int -> a genericPower :: (Num a, Integral b) => a -> b -> a
On Jun 25, 2007, at 11:40 AM, David Roundy wrote:
That would be great!
Ahh, a consensus I can enthusiastically support. It would seem to me a good library design rule of thumb to make ANY argument that will be counted down to zero by simple recursion an Int, with the type of (^) a standard application of this general principle. Even with strict evaluation and tail recursion, if I want to write something that's going to need more than 2^31 iterations, I want the compiler to make me jump through hoops to say so. With the current type for (^), I'm jumping through hoops to say something that I can more easily unroll by hand. Your proposal for (^) would allow genericPower to use the asymptotically faster algorithm of writing out the exponent in binary and multiplying together repeated squares, leaving the simple recursion to (^).
On Mon, 25 Jun 2007, Ian Lynagh wrote:
On Fri, Jun 22, 2007 at 11:37:15AM -0700, Dave Bayer wrote:
z = r Prelude.^ 3
I don't know if (^) in particular is what is causing you problems, but IMO it has the wrong type; just as we have (!!) :: [a] -> Int -> a genericIndex :: (Integral b) => [a] -> b -> a we should also have (^) :: (Num a) => a -> Int -> a genericPower :: (Num a, Integral b) => a -> b -> a (or some other function name).
Seconded!
I've mentioned this before, but until http://hackage.haskell.org/trac/haskell-prime/ticket/118 is resolved we don't know where to discuss it (the haskell-prime or libraries list).
| happens because I don't want to actually use defaulting, but I would | have no objection to the warning being suppressed if someone has | explicitly given a "default" declaration (and thus, presumably, does | want to use defaulting). I'm not against this particular proposal if there's a consensus in favour of it. Simon
participants (13)
-
apfelmus -
Brandon Michael Moore -
Brandon S. Allbery KF8NH -
Claus Reinke -
Dave Bayer -
David Roundy -
Derek Elkins -
Henning Thielemann -
Ian Lynagh -
Jaap Weel -
Neil Mitchell -
Simon Peyton-Jones -
Stefan O'Rear