Re: [Haskell-cafe] Strict type system allows for a maximum number of programming errors to be caught at compile time.
On 04/05/2010, at 13:30, Luke Palmer wrote: On Mon, May 3, 2010 at 11:07 AM, Kyle Murphy orc...@gmail.com wrote: The fact that it doesn't is proof enough that there's a problem with it even if that problem is simply that the types you're using aren't exactly correct. Further, I'd argue that in the first instance with a non-strict type system, the instance of wrong code that compiles would be higher. The only argument to support non-strict typing would be if you could show that it takes less time to track down runtime bugs than it does to fix compile time type errors, and any such claim I'd be highly skeptical of. Clearly. But many people believe in this methodology, and use test suites and code coverage instead of types. Indeed, such practices are essentially empirical type checking, and they afford the advantage that their verification is much more expressive (however less reliable) than our static type system, because they may use arbitrary code to express their predicates. I don't think it's a question of types vs. testing. Rather, it's types + testing vs. just testing. How is the latter more expressive than the former for defining properties of programs? Also, testing loses a lot of appeal once you start dealing with concurrent programs. Testing for this program doesn't have race conditions isn't exactly easy. You want as many static guarantees as possible. Roman ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strict type system allows for a maximum number of programming errors to be caught at compile time.
On Mon, May 3, 2010 at 11:34 AM, Casey Hawthorne cas...@istar.ca wrote: Strict type system allows for a maximum number of programming errors to be caught at compile time. I keep hearing this statement but others would argue that programming errors caught at compile time only form a minor subset of all errors caught. So, in functional programming languages with a strict type system, e.g. Haskell, do typing errors from a larger subset of all programming errors. Yes. You can usually write much the same program with and without static types. The difference will be that in the dynamic typing/untyped setting you'll get the errors at runtime, and in the statically typed setting you'll get (many of) the errors at compile time. You can express a lot of invariants with types once you become familiar with their usage. For instance you can make a 2-3 tree in Haskell where the types enforce the fact that the tree is balanced. You can implement the same code in Scheme or another dynamically typed language, but the result will lack that extra guarantee. Nothing says that your insert operation drops the node in the right place, etc, but at last you know you are safe from one class of bugs. Types effectively prove lots of little boring theorems about your code as you program. Inconsistent code will often cause these sorts of little proofs to fail. One thing that thinking about types helps you to do is to figure out if given the types if the choice of implementation is more-or-less unique. For instance given the type for fmap, and the extra law(s) you need to satisfy, you really only have one correct implementation option. ;) So not only do you get benefit from the compiler giving you errors rather than finding out later when your runtime system blows up in production, but the types help inform you as to what the shape of a correct implementation should be. -Edward Kmett ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strict type system allows for a maximum number of programming errors to be caught at compile time.
Are you really sure about that... it might cause a typing error if you misspell something. Proposal: The double typing error Kind regards, Samuel On 4/05/2010, at 3:34 AM, Casey Hawthorne wrote: I don't mean tpynig errros. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strict type system allows for a maximum number of programming errors to be caught at compile time.
On Mon, May 3, 2010 at 9:34 AM, Casey Hawthorne cas...@istar.ca wrote: Strict type system allows for a maximum number of programming errors to be caught at compile time. I keep hearing this statement but others would argue that programming errors caught at compile time only form a minor subset of all errors caught. So, in functional programming languages with a strict type system, e.g. Haskell, do typing errors from a larger subset of all programming errors. Absolutely! Haskell developers trade debugging time for time arguing with the compiler about the correctness of their code. I'll give this meaningless anecdotal statistic: Compiler says my code is right = My code is actually right -- 60% Compiler says my code is wrong = My code is actually wrong -- 95% Haskell has a particular reputation for the former. Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strict type system allows for a maximum number of programming errors to be caught at compile time.
The problem with dynamic typing is that it has a much higher chance of having a subtle error creep into your code that can go undetected for a long period of time. A strong type system forces the code to fail early where it's easier to track down and fix the problem, rather than trying to perform debugging on the fly in a production system. This has an added advantage for compiled languages in that for many non-trivial applications the time to build and deploy a new instance of the program, even in the development environment is often substantial, and the more trivial errors are discovered at compile time, the less time is wasted on builds. For small code bases the time spent tracking down a error at runtime might be less than the time spent making your code conform to strict type requirements, but for larger code bases the amount of time necessary to track down such errors greatly out weighs the amount of time needed to make your code well typed. To look at the flip side of your statistics: Compiler says my code is right = My code is actually wrong -- 40% Compiler says my code is wrong = My code is actually right -- 5% I'd argue this is provably wrong, as correct code by definition would compile. The fact that it doesn't is proof enough that there's a problem with it even if that problem is simply that the types you're using aren't exactly correct. Further, I'd argue that in the first instance with a non-strict type system, the instance of wrong code that compiles would be higher. The only argument to support non-strict typing would be if you could show that it takes less time to track down runtime bugs than it does to fix compile time type errors, and any such claim I'd be highly skeptical of. -R. Kyle Murphy -- Curiosity was framed, Ignorance killed the cat. On Mon, May 3, 2010 at 12:00, Luke Palmer lrpal...@gmail.com wrote: On Mon, May 3, 2010 at 9:34 AM, Casey Hawthorne cas...@istar.ca wrote: Strict type system allows for a maximum number of programming errors to be caught at compile time. I keep hearing this statement but others would argue that programming errors caught at compile time only form a minor subset of all errors caught. So, in functional programming languages with a strict type system, e.g. Haskell, do typing errors from a larger subset of all programming errors. Absolutely! Haskell developers trade debugging time for time arguing with the compiler about the correctness of their code. I'll give this meaningless anecdotal statistic: Compiler says my code is right = My code is actually right -- 60% Compiler says my code is wrong = My code is actually wrong -- 95% Haskell has a particular reputation for the former. Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strict type system allows for a maximum number of programming errors to be caught at compile time.
In my opinion code is 'right' when it conforms to the specification. Haskell's type system allows the programmer to express a part of the specification in the types, which then get checked by the compiler/type-checker. This is where I see the biggest benefit of a very expressive statically checked type system. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strict type system allows for a maximum number of programming errors to be caught at compile time.
On Mon, May 3, 2010 at 11:07 AM, Kyle Murphy orc...@gmail.com wrote: The problem with dynamic typing is that it has a much higher chance of having a subtle error creep into your code that can go undetected for a long period of time. A strong type system forces the code to fail early where it's easier to track down and fix the problem, rather than trying to perform debugging on the fly in a production system. This has an added advantage for compiled languages in that for many non-trivial applications the time to build and deploy a new instance of the program, even in the development environment is often substantial, and the more trivial errors are discovered at compile time, the less time is wasted on builds. For small code bases the time spent tracking down a error at runtime might be less than the time spent making your code conform to strict type requirements, but for larger code bases the amount of time necessary to track down such errors greatly out weighs the amount of time needed to make your code well typed. To look at the flip side of your statistics: Compiler says my code is right = My code is actually wrong -- 40% Compiler says my code is wrong = My code is actually right -- 5% I'd argue this is provably wrong, as correct code by definition would compile. Here is a contrived example of what I am referring to: prefac f 0 = 1 prefac f n = n * f (n-1) fac = (\x - x x) (\x - prefac (x x)) If this code were allowed to compile (say by inserting unsafeCoerce anywhere you like), it would correctly implement a factorial function. It is precisely these cases behind the dynamically typed languages' advocacy: my code is right but I can't (or it is too much work to) convince the compiler of that fact. It is a pretty bold statement to say that these do not occur. The fact that it doesn't is proof enough that there's a problem with it even if that problem is simply that the types you're using aren't exactly correct. Further, I'd argue that in the first instance with a non-strict type system, the instance of wrong code that compiles would be higher. The only argument to support non-strict typing would be if you could show that it takes less time to track down runtime bugs than it does to fix compile time type errors, and any such claim I'd be highly skeptical of. Clearly. But many people believe in this methodology, and use test suites and code coverage instead of types. Indeed, such practices are essentially empirical type checking, and they afford the advantage that their verification is much more expressive (however less reliable) than our static type system, because they may use arbitrary code to express their predicates. What I seem to be getting at is this plane of type systems: Constrained - Expressive Unreliable | (C) |(test suites) | (C++). |. | (Java/C#)(Scala) . |. |. | (Haskell). | | (Agda) Reliable Where by Constrained/Expressive I mean the ability for the system to express properties *about the code* (so C++'s type system being turing complete is irrelevant). By Unreliable/Reliable I mean, given popular engineering practice in that language, the chance that if it passes the checks then it works as intended. For all the languages, I mean their compilers. Test suites extend down the right-hand side, depending on how rigorous you are about testing, but they never get as far down as Agda. :-) Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strict type system allows for a maximum number of programming errors to be caught at compile time.
lrpalmer: What I seem to be getting at is this plane of type systems: Constrained - Expressive Unreliable | (C) |(test suites) | (C++). |. | (Java/C#)(Scala) . |. |. | (Haskell). | | (Agda) Reliable Where have I seen this before oh!! http://i.imgur.com/srLvr.jpg The Big Lebowski Alignment Chart, mirrored!! + | Lawful Good Chaotic Good | (Agda) (C++) | | |True Netural | (Haskell) | | | | Lawful Evil Chaotic Evil | (testsuites) (C) + | | | | ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strict type system allows for a maximum number of programming errors to be caught at compile time.
On 4 May 2010 13:30, Luke Palmer lrpal...@gmail.com wrote: Here is a contrived example of what I am referring to: prefac f 0 = 1 prefac f n = n * f (n-1) fac = (\x - x x) (\x - prefac (x x)) I can't work out how this works (or should work rather); is it meant to be using church numerals or something (assuming that they have been made an instance of Num so that - and * work)? -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strict type system allows for a maximum number of programming errors to be caught at compile time.
prefac is just a normal factorial function with recursion factored out. fix prefac 5 gives 120, for example. On Tue, May 4, 2010 at 12:13 AM, Ivan Miljenovic ivan.miljeno...@gmail.comwrote: On 4 May 2010 13:30, Luke Palmer lrpal...@gmail.com wrote: Here is a contrived example of what I am referring to: prefac f 0 = 1 prefac f n = n * f (n-1) fac = (\x - x x) (\x - prefac (x x)) I can't work out how this works (or should work rather); is it meant to be using church numerals or something (assuming that they have been made an instance of Num so that - and * work)? -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strict type system allows for a maximum number of programming errors to be caught at compile time.
On Tue, May 4, 2010 at 12:13 AM, Ivan Miljenovic ivan.miljeno...@gmail.com wrote: On 4 May 2010 13:30, Luke Palmer lrpal...@gmail.com wrote: Here is a contrived example of what I am referring to: prefac f 0 = 1 prefac f n = n * f (n-1) fac = (\x - x x) (\x - prefac (x x)) I can't work out how this works (or should work rather); is it meant to be using church numerals or something (assuming that they have been made an instance of Num so that - and * work)? Looks like a variation on H. Curry's fixed-point combinator to me, e.g.: y f = (\x - f (x x)) (\x - f (x x)) Which of course is perfectly useful, but not valid in any type system that excludes absurdities. The otherwise-infinite type signature for Y is circumvented by built-in recursion in Haskell (making halting undecidable in the process, unfortunately). - C. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strict type system allows for a maximum number of programming errors to be caught at compile time.
On Mon, May 3, 2010 at 10:13 PM, Ivan Miljenovic ivan.miljeno...@gmail.com wrote: On 4 May 2010 13:30, Luke Palmer lrpal...@gmail.com wrote: Here is a contrived example of what I am referring to: prefac f 0 = 1 prefac f n = n * f (n-1) fac = (\x - x x) (\x - prefac (x x)) I can't work out how this works (or should work rather); is it meant to be using church numerals or something (assuming that they have been made an instance of Num so that - and * work)? No they're just integers. fac is a beta expansion of fix prefac. Obseve the magic: (\x - x x) (\x - prefac (x x)) 2 (\x - prefac (x x)) (\x - prefac (x x)) 2 prefac ((\x - prefac (x x)) (\x - prefac (x x))) 2 2 * ((\x - prefac (x x)) (\x - prefac (x x)) (2-1) 2 * prefac ((\x - prefac (x x)) (\x - prefac (x x))) (2-1) 2 * prefac ((\x - prefac (x x)) (\x - prefac (x x))) 1 2 * (1 * ((\x - prefac (x x)) (\x - prefac (x x))) (1-1)) 2 * (1 * prefac ((\x - prefac (x x)) (\x - prefac (x x))) (1-1)) 2 * (1 * prefac ((\x - prefac (x x)) (\x - prefac (x x))) 0) 2 * (1 * 1) 2 Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
