[Haskell-cafe] Re: exceptions vs. Either
After all, Java basically does exactly what you're asking for with Java's head/tail would be doing runtime checks if they are throwing exceptions, static guarantees mean the program would not be allowed to compile if it broke the static guarantees. end-programmers have to worry much less about handling errors properly. Which is a bad thing! All programmers always have to consider error conditions, if they don't they write buggy code - that's the nature of the beast. I prefer making programmers expicitly face the decisions they are making, rather than have things implicitly handled in a way that hides what is going on from the programmer. Keean. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: exceptions vs. Either
After all, Java basically does exactly what you're asking for with Java's head/tail would be doing runtime checks if they are throwing exceptions, static guarantees mean the program would not be allowed to compile if it broke the static guarantees. Not so. In Java, the programmer is forced to handle most exceptions by the type system. That is, if the exception is not handled, the program will not compile, thus providing a static guarantee that exceptions are handled. Only unchecked exceptions (RuntimeException and Error) are exempt from this check. --KW 8-) ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: exceptions vs. Either
Not so. In Java, the programmer is forced to handle most exceptions I forgot you had to do that... Exceptions are explicit in the type signatures. I think Oleg posted a message a while back about how to make exceptions explicit in haskell type signatures... But I would rather use static guarantees where possible, and exceptions where necessary. I haven't really tried using the techniques for explicit exceptions, but on consideration I might see if it is practical to code in that style... Keean. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: exceptions vs. Either
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. I had to change coding style moving from imperative to declarative languages, but I think it was worth it... Likewise I think having the ability to make strong static guaranees is worth it - you may not, which is why it is important not to break any existing programs with language extensions (if any are necessary). My programs will have less bugs though! worse-is-better, even in its strawman form, has better survival I fully subscribe to the 'worse is better' approach, but I don't see how it contradicts the principle of static guarantees - you can have both. Simplicity is about algorithmic complexity not about whether type signatures are provided by the programmer. Infact type signatures are in themselves an embodyment of the simple is better principle. A type signature expresses certain static guarantees about the function in a vary compact way. Consider the sort example... being able to declare a type signature on a sort algorith that enforces ordering of the output would prove the sort algorithm can _only_ output correctly sorted lists under _all_ circunstances. This type signature is much simpler than the actual sort - hence is useful. sort :: (HList l,HOrderedList l') = l - l' Nice and readable, and much simpler than the actual algorithm (be it bubble sort, or a quick sort) Keean. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: exceptions vs. Either
correctly sorted lists under _all_ circunstances. This type signature is much simpler than the actual sort - hence is useful. sort :: (HList l,HOrderedList l') = l - l' Nice and readable, and much simpler than the actual algorithm (be it bubble sort, or a quick sort) The type signature you give is no different from sort :: (C1 l, C2 l') = l - l' and conveys no more information. You should include the definitions of the classes before saying this is much simpler than the actual sort. --KW 8-) ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: exceptions vs. Either
You should include the definitions of the classes before saying HOrderedList l' just has to prove by induction that for any element in the list, the next element is greater, so the class is simply: class HOrderedList l instance HNil instance HCons a HNil instance (HOrderedList (HCons b l),HLe a b) = HCons a (HCons b l) which is the equivalent type level program to ordered :: [Int] - Bool ordered [] = True ordered [a] = True ordered (a:(b:l)) = if a=b then ordered (b:l) else False ordered _ = False It is obvious by observation that the a=b ensures order. This is a lot simpler than say a heap-sort. I suppose you could contend that there are some classes above I still haven't defined - but you wouldn't expect to see definitions for (=) which is defined in the prelude. Of course to show statically that order is preserved the 'value' of the elements to be ordered must be visible to the type system - so the values must be reified to types... This can be done for any Haskell type, but for numbers we would use Peano numbers - the HLe class for these is again easily defined by induction: class HLe n n' instance HLe HZero HZero instance HLe x y = HLe (HSucc x) (HSucc y) Keean. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: exceptions vs. Either
On 06/08/2004, at 6:56 PM, MR K P SCHUPKE wrote: After all, Java basically does exactly what you're asking for with Java's head/tail would be doing runtime checks if they are throwing exceptions, static guarantees mean the program would not be allowed to compile if it broke the static guarantees. As Keith said, Java will check at compile time whether or not you handle the exception. My point is this: it is impossible to check whether the exception is properly handled. If you adjust Haskell's tail function to return (Maybe [a]) instead of just ([a]), you are doing the thing as Java from a pragmatic perspective: you are adding information to the type system that tells the programmer the function may fail. You also suffer the same consequence as Java: you have no idea whether the programmer properly handles the error situation. If I am writing a one-shot, never-use-again script that takes 3 minutes to write, and I _know_ that I'm not going to be feeding the tail function a non-empty list--e.g. because I'm writing a one-shot five-minute script to transform a file from one text format to another, as is the case for lots of Perl programs--then the extra Maybe type just gets in the way. I'll either ignore the Nothing case, or write `case tail foo of ... Nothing - error bleh'. I will go so far to say that such a program can be considered correct: it does exactly what I want it to do, in exactly the circumstances I desire (0 byte files being specifically excluded from the circumstances!). Which is a bad thing! All programmers always have to consider error conditions, if they don't they write buggy code - that's the nature of the beast. I prefer making programmers expicitly face the decisions they are making, rather than have things implicitly handled in a way that hides what is going on from the programmer. It's a question of whether the library designer should impose their will on the library user. As a library designer, do you feel that you are always making the right decision for the library user 100% of the time? I know I never feel like that when I write libraries ... -- % Andre Pang : trust.in.love.to.save ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] 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. ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: exceptions vs. Either
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 ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: exceptions vs. Either
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 ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: exceptions vs. Either
specify that a sort function (say) returns an ordered list
Fistly this is already possible in Haskell - see Oleg, Ralf and
My paper:
@misc{KLS04,
author = Oleg Kiselyov and Ralf L{\a}mmel and Keean Schupke,
title = {Strongly typed heterogeneous collections},
booktitle = {ACM SIGPLAN Workshop on Haskell},
year = 2004,
month = sep,
publisher = ACM Press,
notes = To appear
}
http://homepages.cwi.nl/~ralf/HList/
Here we show constrained heterogeneous lists (but you can also
constrain the type in the list to turn it into a homogeneous list)
that includes the ability to impose ordering constraints...
Writing the constraint classes is a little involved but using it is
as simple as:
sort :: (HList l,HOrderedList l') = l - l'
and supposing you dont like having to write the complete type, you
can use:
ordered :: HOrderedList l = l - l
ordered = id
then you can use this in a function with no type given:
sort = ordered . sort'
So my point is this can be added to haskell _without_ breaking
any existing functionality - it is not either/or it is both/and!
Keean.
___
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: exceptions vs. Either
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
___
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: exceptions vs. Either
On 04/08/2004, at 12:28 AM, MR K P SCHUPKE wrote: f (case xs of (x:_) - x; [] - error whoops) -- direct style Yup, this is how I do it... I never use head! I like to pass failures back up to the level where some kind of sensible error message can be generated. In your example the error is no better than with 'head' - the point is a Nothing can be 'caught' outside of an IO monad. I would suggest using the type system as I said earlier so: toNonEmptyList :: [a] - Maybe (NonEmpty a) toNonEmptyList (a0:_) = Just (NonEmpty a) toNonEmptyList _ = Nothing Then redefine head: head :: NonEmpty a - a head (NonEmpty (a0:_)) = a0 There's an interesting discussion going on at Lambda the Ultimate right now, about this very topic: http://lambda-the-ultimate.org/node/view/157#comment There are plenty of noteworthy comments there, but one which quite nicely expresses my point of view is: Using Maybe for this is like saying - let's turn this partial function into a total one by lifting its range to include Nothing. It became total by obtaining permission to return something I have no use of. I do not say monads are not useful, or Maybe is not useful. And, of course, there's the type wizardry post by Oleg: http://lambda-the-ultimate.org/node/view/157#comment-1043 I'd like to point out that it is possible in Haskell98 to write non-trivial list-processing programs that are statically assured of never throwing a `null list' exception. That is, tail and head are guaranteed by the type system to be applied only to non-empty lists. Again, the guarantee is static, and it is available in Haskell98. Because of that guarantee, one may use implementations of head and tail that don't do any checks. Therefore, it is possible to achieve both safety and efficiency. Please see the second half of the following message: http://www.haskell.org/pipermail/haskell/2004-June/014271.html -- % Andre Pang : trust.in.love.to.save ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
