Re: exceptions vs. Either
What can I say... Static typing guarantees is what made me switch from object oriented languages like C++/ObjectiveC/Java (that and the availability of a good compiler) - So I am obviously in favour of more static guarantees - I believe programming by contract is the way to reliable _engineered_ software, so the more contractual obligations that can be concisely and clearly expressed in the type system the better. I think Haskell should support dependant types, after all if you don't want to use them you don't have to... (backwards compatability and all that) although it would be useful to have a replacement prelude that used dependant types versions of head etc... I have a hard time understanding why functional programmers would not want more static typing guarantees, after all they can always use C if they dont like type systems! Keean.
I have a hard time understanding why functional programmers would not want more static typing guarantees, after all they can always use C if they dont like type systems!
I think the value of Haskell's type system is that it catches a lot of bugs _cheaply_. That is, with little programmer effort to write the type annotations, little effort to understand them and little effort to maintain them as the program evolves. In general, as we try to express more and more in the type system, the costs go up so the goal in using a different programming style or extending the type system is to catch more bugs without significantly increasing the cost. At an extreme, we could probably use some variant of higher order predicate calculus as our type system and specify that a sort function (say) returns an ordered list but the programmer effort in doing so would probably be quite high. Using Maybe and the like to catch more errors with the type system isn't as expensive as using full-on specification and is often the right thing to do but, in some cases, the benefits of programming that way don't justify the effort required whereas the techniques suggested for reporting the location of the problem are cheap and effective. -- Alastair Reid
Hi folks Alastair Reid wrote:
I have a hard time understanding why functional programmers would not want more static typing guarantees, after all they can always use C if they dont like type systems!
I think the value of Haskell's type system is that it catches a lot of > bugs _cheaply_. That is, with little programmer effort to write the type annotations, little effort to understand them and little effort to maintain them as the program evolves.
I entirely agree. The effort-to-reward ratio is the key consideration when deciding how much information to build into types. I'm biased, of course, but the thing I like about working with a dependent type system is that I at least have the option to explore a continuum of static expressivity and choose a compromise which suits my conception of the task at hand. To oppose the availability of more informative types is to rule out the option of exploiting them even when they are useful. A key aspect of the Epigram approach is to pay attention to the /tools/ we use to write programs. Of course it gets harder to work with more involved types if you have to do it all in your head. Frankly, polymorphic recursion is enough to make my brain hurt, let alone the kind of type class shenanigans which various people (myself included) have been engaging in. I have a not-so-secret weapon. Once I've developed the program interactively in Epigram (or its predecessor, OLEG, in the case of the Faking It stuff), exploiting the fact that a computer can push type information /into/ the programming process, it's quite easy to crank out the relevant steaming lump of obfuscated Haskell. One tool that's really needed here is a refactoring editor which enables you to write the program naively, exposing the exceptional cases, then, once you've seen where they show up, refine the data structures to eliminate some or all of them. It's a fair cop: at the moment, Epigram requires you to dream up the data structures from thin air before you write the programs. That doesn't fit with the fact that good ideas only tend to come a bit at a time. However, we can certainly improve on this situtation, given time and effort.
In general, as we try to express more and more in the type system, the costs go up so the goal in using a different programming style or extending the type system is to catch more bugs without significantly increasing the cost. At an extreme, we could probably use some variant of higher order predicate calculus as our type system
I'd recommend a system which enables you to build stronger structural invariants directly into data structures, rather than using data types which are too big, and then a whole pile of predicates to cut them down to size afterwards: as you fear, the latter is a good way to fill a program up with noisy proofs. But if you use indexed datatype families (Dybjer, 1991), you can avoid a lot of this mess and what's more, a type-aware editor can rule out many exceptional cases on your behalf. In many cases, the Epigram editor shows you exactly the data which are consistent with the invariants, without any effort on your part.
and specify that a sort function (say) returns an ordered list but the programmer effort in doing so would probably be quite high.
I'm pleased to say it isn't. See http://www.dur.ac.uk/c.t.mcbride/a-case/ and in particular http://www.dur.ac.uk/c.t.mcbride/a-case/16so/ onwards, for treesort-enforcing-sorted-output. There's not much to it, really. The thing is, ordinary if-then-else loses the fact that performing the comparisons directly establishes the properties required to satisfy the sorting invariants in the output structures. It's not hard to remedy this situation. Moreover, most of the logical plumbing can be managed implicitly, as it merely requires picking up proofs which are immediately visible in the context. Of course, (see Inductive Families Need Not Store Their Indices, by Edwin Brady, James McKinna and myself) none of this logical stuff incurs any run-time overhead.
Using Maybe and the like to catch more errors with the type system isn't as expensive as using full-on specification and is often the right thing to do but, in some cases, the benefits of programming that way don't justify the effort required whereas the techniques suggested for reporting the location of the problem are cheap and effective.
You're absolutely right. And today's technology often means that the match-exception way, let alone the Maybe-way, wins this trade-off. Tomorrow's technology will not remove this trade-off, but it might sometimes change the outcome of the calculation. I think that's worth working for. Cheers Conor
On 05/08/2004, at 7:40 PM, MR K P SCHUPKE wrote:
I have a hard time understanding why functional programmers would not want more static typing guarantees, after all they can always use C if they dont like type systems!
Static guarantees are great, but if you have to explicitly change your style of coding to cope with those extra constraints, it can become (very) cumbersome. After all, Java basically does exactly what you're asking for with head/tail: if you were to write a tail method in a List class, you could simply throw a EmptyListException. That's really the same effect as tail in Haskell returning a Maybe: both forms force you to perform error-handling in the calling function. However, I think Java has shown that forcing error-handling on the caller via exceptions is no magic bullet: a lazy programmer will simply catch the exception in an empty catch {} block. It's a human problem, not a technical one. Obviously exceptions, Maybes, monads etc. are useful, but forcing the programmer to Do The Right Thing is nearly impossible. I personally think that using tricks such as type classes to propagate constraints and errors via the type system is a fantastic idea, because then end-programmers have to worry much less about handling errors properly. -- % Andre Pang : trust.in.love.to.save
At 12:36 06/08/04 +1000, André Pang wrote:
Static guarantees are great, but if you have to explicitly change your style of coding to cope with those extra constraints, it can become (very) cumbersome.
[...] It's a human problem, not a technical one.
I think that's an important point. For some related opinion, see: "worse-is-better, even in its strawman form, has better survival characteristics than the-right-thing" -- http://www.jwz.org/doc/worse-is-better.html [*] My point being that we have some knobs to play with here, and that winding them fully to one end of the scale is likely to result in something that few want to use, or can be bothered to learn. #g -- [*] I acknowledge Dan Connolly (W3C) for pointing this out in a different forum, just a couple of days ago. ------------ Graham Klyne For email: http://www.ninebynine.org/#Contact
participants (5)
-
Alastair Reid -
André Pang -
Conor T McBride -
Graham Klyne -
MR K P SCHUPKE