[Haskell-cafe] exceptions vs. Either
Evan LaForge
Exceptions are convenient in that you can rely on libraries throwing them
instead of prechecking for valid values yourself (for instance, why check
that the argument to Char.digitToInt is valid if digitToInt does so already),
and you don't have to modify a lot of function signatures. Unfortunately, in
the face of lazy evaluation, they can get thrown in unexpected places. Even
with Exception.evaluate, or code which is already explicitly sequenced in the
IO monad, like "t <- Exception.evaluate (map Char.digitToInt ['a'..'g'])" an
exception will only be thrown when you inspect the last element of 't'.
(digitToInt confusingly accepts hex "digits"---shouldn't it be "higitToInt"
then?).
So it seems to me that if you are, say, checking input, the options are
to handle exceptions from the checking code but expect them to come from the
processing code, or decorate all checking code with Rights and Lefts.
Problems with the first option are that checking code could also trigger some
exceptions, and Prelude functions throw undescriptive errors like "user
error" or low level ones like "refuted pattern match" and catching them over
the entire program means you could stifle a lot of real errors. This implies
that you have to make specific exceptions and convert Prelude and library
exceptions into yours as low down as possible, which is cluttering but maybe
not as cluttering as Either. Problems with the second option are many of the
problems that lead to us wanting exceptions in the first place.
Using Either seems much simpler and functional-friendly. So then, in what
contexts are exceptions appropriate in haskell?
_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Alastair Reid
> Exceptions are convenient [...]
> [but] an exception will only be thrown when you evaluate t.
>
> So it seems to me that if you are, say, checking input, the options are
> to handle exceptions from the checking code but expect them to come from
> [...]
> So then, in what contexts are exceptions appropriate in haskell?
I think you're right that exceptions aren't useful for input checking. You
really need something that will check all the input at once. i.e.,
evaluating any part of the checked input causes all input checks to be
performed. The easiest way to do this is with a monad or some such - which
provides you with a more flexible, more controllable error-reporting
mechanism anyway.
I usually use exceptions when dealing with the outside world where I want to
protect the outside world from any misbehaviour of the Haskell code. For
example, if opening and closing windows or files, controlling a robot, etc.,
I might use the exception catching/propagating to make sure that things are
shutdown properly when the Haskell program crashes.
In general, if there's a way to make your program bombproof using a
conventional mechanism (monads, Either, Maybe, etc.), then you should use it
since it will be easier to reason about and can be more flexible. But, if
your program really has to be bombproof and you can't convince yourself that
it is (e.g., it depends on a library you didn't write), exception handling
can help a lot.
--
Alastair Reid
MR K P SCHUPKE
I remember being taught to validate on input _and_ validate when
you use a value. So I would say do both - use maybe for input
functions, and exceptions for when you use a value. You can use
the type system to make this more efficient. Imagine you want an
integer between 10 and 20, you have a function like:
newtype ValidInt = Valid Int
validateInt :: Int -> Maybe ValidInt
validateInt x | x>=10 && x<=20 = Just (Valid x)
validateInt _ = Nothing
Now when you validate on input - you produce an error if
you get "Nothing" and in all the functions you use the
value you use ValidInt instead of Int. This way you
use the type system to differentiate between a valid
int (does not need to be rechecked) and a normal int
(which would need to be validated).
Of course you must make sure you don't write more than
one constructor function for ValidInt. This suggests a
form of constrained constructor would be useful... Whilst
this can be done in Haskell,
it is not easy and involves reifying the value to a type,
and using a type class to constrain the data statement.
Really here we are dealing with dependant types, and this
is much easier in a dependantly typed language like
Epigram.
Keean.
Graham Klyne
1. When I recently modified the HaXml XML parser, this is one of the
significant changes I made: providing (alterantive) return values based on
Either, so that input errors could be handled by the invoking function,
without forcing it into the IO monad. I guess that's a vote of agreement.
2. I like to distinguish between "expected errors" and "unexpected
errors". Having been burned in the past by using exceptions (not FP), I
try to use them only for conditions that are truly unexpected; i.e.
_exceptional_. Bad input, IMO, is something that is not unexpected, so I
don't really like to handle that via exceptions.
#g
--
------------
Graham Klyne
For email:
http://www.ninebynine.org/#Contact
Ketil Malde
> 2. I like to distinguish between "expected errors" and "unexpected
> errors". Having been burned in the past by using exceptions (not FP),
> I try to use them only for conditions that are truly unexpected;
> i.e. _exceptional_. Bad input, IMO, is something that is not
> unexpected, so I don't really like to handle that via exceptions.
I agree, trying to handle exceptions caused by incorrect input is just
needless complication, the program should crash, and the calling
function should be fixed instead.
Common errors that happen to me are:
Prelude.head : empty list
Prelude.read : no parse
and Prelude.(!!) : index too large
and so on.
Is there any easy way (TH?) to amend these to output the line number
of the offending caller? It would be a great improvement to see
something like
Prelude.head : empty list in Foo.hs, line 4711
since programs generally contain many, many calls to functions like
these.
-kzm
--
If I haven't seen further, it is by standing in the footprints of giants
Bjoern Knafla
intricacies. However I just recently read an article of Herb Sutter
about exception handling in C++ with some rules when to use exception
handling - and perhaps these rules might be applicable to Haskell too
(article: "When and How to Use Exceptions", Herb Sutter, C/C++ Users
Journal August 2004, pp. 47 -- 51)?
Herb Sutter gave these rules :
An error is any failure that prevents a function from succeeding. Three
main kind of errors:
- a condition that prevents the function from meeting a precondition of
another function that must be called (so to say: the caller has to
check for preconditions while the function called my use C/C++ asserts
to assert the correctness of its preconditions)
- a condition that prevents a function from establishing one of its own
postconditions (e.g. producing a (valid) return value)
- a condition that prevents the function from reestablishing an
invariant that it is responsible to maintain (special kind of
postcondition mainly found in object oriented code).
Any other condition is not an error and shouldn't be reported as one.
The code that could cause an error is responsible for detecting and
reporting the error otherwise this is a programming mistake.
I am not sure if these rules apply to real functional programming but
at least they seem to be useable. The point that the caller is
responsible for checking the preconditions of functions it is calling
is something I also found as a suggestion in using the object oriented
language Eiffel.
Cheers and best regards
Bjoern
Marcin 'Qrczak' Kowalczyk
> Herb Sutter gave these rules :
>
> An error is any failure that prevents a function from succeeding. Three
> main kind of errors:
[...]
These kinds don't explain much. They don't give a clue which errors
to report by exceptions and which by return values, because they don't
distinguish the reasons for which a (pre|post)condition can't be
fulfilled. And I see no point in distinguishing potential errors on
this axis.
I divide exceptional situations into 4 groups:
1. Expected error: The result can't be computed from this data; the
caller was not supposed to check this beforehand because it would
duplicate work of the function, or there would be a race condition,
or the design is simpler that way.
2. Program error: The given function was not supposed to be invoked
in this way by other parts of the program (with these arguments,
or with this external state, in this order wrt. other functions
etc.).
3. Out of resource: The function is sorry that it was not able to
produce the result due to limited memory or arithmetic precision
or similar resources. "Not yet supported" is also in this group.
4. Impossible error: The function thought this couldn't happen, it must
have a bug. This is like 2 in that there is a bug somewhere, but like
1 in that the calling code is probably fine.
I/O errors can be expected errors or out of resource conditions,
depending on whether they were caused by bad input or by external
failure.
Group 1 should be reported in Haskell by a distinguished result (Maybe,
Either, custom type) or by an exception passed in a suitable monad
(well, Maybe is a monad; this could be even the IO monad).
Other groups are handled in a similar way. In Haskell they can be
reported by a bottom, e.g. 'error' function. It makes sense to catch
them on a toplevel of the program or a large unit, and it's good that
GHC provides a way to catch them. There may be other actions possible
than just aborting the program: report the problem to the user, abort
just the given operation, but try to continue other work; save user data
before aborting; log the error or report it in an appropriate channel,
e.g. output a HTML page in case of a CGI program.
Sometimes the same function makes sense in two variants: one which
reports an expected error, and another which treats it as a program
error. Example: lookup in a dictionary.
Sometimes the qualification of an error changes while it is propagated.
I haven't thought about all cases, but for example program errors become
impossible errors if the caller thought that the arguments it passed
were good, and expected errors become program errors if the caller's
caller was not supposed to give arguments which cause such problems.
The most important distinction is between expected errors, whose way of
reporting should be visible in the interface and which should be checked
for in the calling code, and program errors, which should be
automatically propagated and reported near the toplevel.
--
__("< Marcin Kowalczyk
\__/ qrc...@knm.org.pl
^^ http://qrnik.knm.org.pl/~qrczak/
MR K P SCHUPKE
There was a discussion about this recently (on the ghc list I think)(
The proposed (partial) solution is to use mapException:
mapExceptionIO :: (Exception -> Exception) -> IO a -> IO a
mapExceptionIO f io = Exception.catch io (\e -> throw $ f e)
which would be used like:
main = mapExceptionIO (\x -> ErrorCall $ showString "in main: " $ show x) $ do
Exceptions can be thrown from anywhere, but can only be caught in the IO
monad hence mapException must be in the IO monad.
Map exception allows a kind of 'backtrace' allowing all functions in the
call stack of a function which throws an exception to annotate the error
message.
Exceptions should only really be used for unpredictcable events, I find
that the defintion of functions like head is lacking rigor... I would
prefer to see:
head :: [a] -> Maybe a
head (a0:_) = Just a0
head _ = Nothing
I think functions should only throw an exception if they are subject
to the halting problem (the only way to tell if an algorith will fail
is to run that algorith) - head and lots of other functions in the prelude
are not subject to this, and in my opinion should really be returning
Maybe...
nobody said anything about me previous post about using the type system
to have 'validated' types - does this mean everyone thinks its a good idea,
or was it too off topic - too obvious?
Keean.
Keith Wansbrough
> that the defintion of functions like head is lacking rigor... I would
> prefer to see:
>
> head :: [a] -> Maybe a
> head (a0:_) = Just a0
> head _ = Nothing
In principle, yes, but in practice, that would be silly. You use
"head" just when you know for sure that the list is non-empty; if it
is not, it's a "program error" for head, and an "impossible error" for
the caller. Consider:
f (head xs) -- old style
vs
f (case head xs of Some x -> x; None -> error "whoops") -- Schupke style
It should be clear that this function would never be used - if head
had this signature, programmers would just write
f (case xs of (x:_) -> x; [] -> error "whoops") -- direct style
--KW 8-)
MR K P SCHUPKE
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
Keean/
Daniel Yokomiso
"Keith Wansbrough" <Keith.Wa...@cl.cam.ac.uk> escreveu na mensagem
news:fa.g6rem4...@ifi.uio.no...
> > Exceptions should only really be used for unpredictcable events, I find
> > that the defintion of functions like head is lacking rigor... I would
> > prefer to see:
> >
> > head :: [a] -> Maybe a
> > head (a0:_) = Just a0
> > head _ = Nothing
>
> In principle, yes, but in practice, that would be silly. You use
> "head" just when you know for sure that the list is non-empty; if it
> is not, it's a "program error" for head, and an "impossible error" for
> the caller. Consider:
>
> f (head xs) -- old style
>
> vs
>
> f (case head xs of Some x -> x; None -> error "whoops") -- Schupke style
As he's advocating use of error only in cases impossible to verify
statically one would use other device here.
f =<< head xs -- propagating nothing
f (maybe x id (head xs)) -- using default values
> It should be clear that this function would never be used - if head
> had this signature, programmers would just write
>
> f (case xs of (x:_) -> x; [] -> error "whoops") -- direct style
>
> --KW 8-)
Daniel Yokomizo.
---
Outgoing mail is certified Virus Free.
Checked by AVG anti-virus system (http://www.grisoft.com).
Version: 6.0.733 / Virus Database: 487 - Release Date: 2/8/2004
MR K P SCHUPKE
Or use GHC's reifyLocation 'function' in a mapException.
Keean.
Alastair Reid
> Prelude.head : empty list
> Prelude.read : no parse
> and Prelude.(!!) : index too large
> and so on.
>
> Is there any easy way (TH?) to amend these to output the line number
> of the offending caller?
In a program of any size, I usually avoid using these functions and instead
define functions like:
--| 1st arg is error message for empty lists
head' :: Doc -> [a] -> a
--| 1st arg is description of kind of thing in list
-- Reports error if length of list /= 1
unique :: Doc -> [a] -> a
etc.
Another approach is to use a function:
inContext :: String -> a -> a
(implemented using mapException) like this:
inContext "evaluating expression" (eval env e)
to transform an exception of the form:
error "Division by zero"
into
error "Division by zero while evaluating expression"
Since the inContext function is rather like ghc's profiling function 'scc', it
would be nice if ghc had a command-line flag to insert a call to inContext
everywhere that it inserts a call to scc when you use -prof-all. (Of course,
you'd probably take a big stack-space hit from doing so since the chain of
calls to inContext is equivalent to the stack you would expect if using call
by value without tail call optimization.
--
Alastair Reid
Evan LaForge
> A lot of programming errors come from failure to correctly validate.
This was actually nicely illustrated in my program: I assumed that digitToInt
accepted '0'..'9' and wanted to rely on it throwing. After puzzling over
out of range errors (other functions expected digitToInt to be in the 0..9
range) I figured it out and inserted an explicit check. Unfortunately there
is no static check for pre and post conditions, unless you manually add them
to the type system, as you suggest. But that's work ;)
Wrting a monad bind for Either that returns Left immediately and binds Right
would make Either style error propagation easier. But it seems like it would
over sequence:
do a' <- checka a
b' <- checkb b
return $ process a' b'
is rather messier looking than 'process (checka a) (checkb b)'. It doesn't
really matter what order 'a' and 'b' are checked, what I really want is the
monad-style magic plumbing. I suppose I should just wrap 'process' in a
liftM2 and stop worrying about it.
> Of course you must make sure you don't write more than
> one constructor function for ValidInt. This suggests a
Can't you do this at the module level by exporting the ValidInt type, but not
the constructor? Of course, then you have to stick it in its own module, and
simple range validation is getting even more heavyweight...
In response to the "mysterious head exceptions" thread, isn't there a way to
compile with profiling and then get the rts to give a traceback on exception?
Graham Klyne
> >f (case xs of (x:_) -> x; [] -> error "whoops") -- direct style
>
>Yup, this is how I do it... I never use head!
As a general principle, this bothers me.
In the longer term (i.e. if and when large-scale production Haskell systems
become common), and as a matter of principle, I think it's better to use a
prelude (or standard) function when one will do the job, because a
widely-used "industrial strength" compiler might well have special
knowledge of these and be able to apply special optimizations (as, e.g.,
some C/C++ compilers do for standard library functions like memcpy).
As for head, I think it's fine that it throws an error because it is
specified to be defined for only non-empty lists. (I remain silent on
whether the prelude should contain a head-like function that returns a
value for empty lists.)
#g
------------
Graham Klyne
For email:
http://www.ninebynine.org/#Contact
_______________________________________________
Ketil Malde
> head :: [a] -> Maybe a
> head (a0:_) = Just a0
> head _ = Nothing
Argh, no! Violating the precondition of head is a bug in the caller,
I want it to crash, but I also want to know where. Wrapping it up in
Maybe (or any other error propagation) is not a solution.
I don't want to write a lot of unwrapping code in all the callers,
just to get a trackable error message in the (few) cases where I'm
using the function incorrectly.
Neither do I want to write
(\x -> if null x then error ("__FILE__:__LINE__") else head x)
everywhere instead of head, nor pollute my code with error tracking, but
otherwise meaningless strings. (Which is what I generally do when I
get this kind of anonymous error. if null x then error "foo" else
head x.
A mechanism for a function to report the caller site would obliviate
the need for all this ugliness.
-kzm
Hmm...if I run it through CPP and
#define HEAD (\x -> if null x then error ("__FILE__:__LINE__") else head x)
is the __LINE__ resolved at the place of declaration or at the place of usage?
--
If I haven't seen further, it is by standing in the footprints of giants
MR K P SCHUPKE
>specified to be defined for only non-empty lists.
But surely it is better to encode this fact in the type system by
useing a separate type for non-empty lists.
>Argh, no! Violating the precondition of head is a bug in the caller,
>I want it to crash,
Again by encoding this at the type level the compiler can guarantee that
that it is not going to crash or return a compile time error... also by
forcing the programmer to deliberatly cast to a non-empty list you
make explicit the 'non-emptyness'... also the type signature of head
contains the 'contract' that the list must be non empty.
>A mechanism for a function to report the caller site would obliviate
>the need for all this ugliness
Unfortunately the cost of this is prohabative as the call stack
would have to contain backtrace information. Also due to lazy
evaluation the 'call site' may not be what you expect.
I guess we just have to disagree I find very little cause to use head.
Here's what John Meacham had to say:
-----------------------------------
Note that pattern matching rather than deconstruction functions have a
number of benefits, not just relating to error messages, consider two
functions which use the head of their argument.
f xs =3D ... head xs ...=20
g (x:_) =3D ... x ...
now, g is superior to f in several ways,=20
1) the error message generated if the pattern fails will have the file
name, line number and name of function
2) everything but the head of xs may be garbage collected right away
since there is no reference to the rest of the list! This can cure some
nasty space leaks and is vital in certain cases.=20
3) even the simplest compiler will realize g is stirct in its first
argument and take advantage of the numerous optimizations that entails.=20
A good compiler may figure out 2 and 3 with f, but it can't always, and w=
hy
take the chance it won't? All of these benefits apply to deconstructing
more complicated types too, so using pattern matching for deconstruction
is just a good habit to get into.
--------------------------------------
Keean.
Fergus Henderson
>
> In response to the "mysterious head exceptions" thread, isn't there a way to
> compile with profiling and then get the rts to give a traceback on exception?
There is, but it doesn't really work properly, due to
- lazy evaluation
- tail call optimization
- lack of line numbers in the traceback
--
Fergus J. Henderson | "I have always known that the pursuit
Galois Connections, Inc. | of excellence is a lethal habit"
Phone: +1 503 626 6616 | -- the last words of T. S. Garp.
Fergus Henderson
>
> Another approach is to use a function:
>
> inContext :: String -> a -> a
>
> (implemented using mapException) like this:
>
> inContext "evaluating expression" (eval env e)
>
> to transform an exception of the form:
>
> error "Division by zero"
>
> into
>
> error "Division by zero while evaluating expression"
As written, that won't work properly; you will get misleading error
messages, due to lazy evaluation. If a division by zero exception is
thrown, it may have occurred when computing the expression e, rather
than in the function eval itself. Furthermore, if eval returns a compound
type, this code won't catch all division by zero errors that occur while
computing eval, only those that occur while computing the top-most node.
To make it work properly, you can do something like
class hyperSeq a where
hyperSeq :: a -> b -> b
inContext :: (hyperSeq a, hyperSeq b) => String -> (a -> b) -> a -> b
and then inContext can force full evaluation of the input and output,
making sure to force full evaluation of the input _before_
invoking mapException:
inContext msg fn input =
hyperSeq input $
mapException (...) $
let output = fn input
in hyperSeq output output
Of course then you rather completely lose lazy evaluation.
But who wants lazy evaluation, anyway? :)
--
Fergus J. Henderson | "I have always known that the pursuit
Galois Connections, Inc. | of excellence is a lethal habit"
Phone: +1 503 626 6616 | -- the last words of T. S. Garp.
David Menendez
> MR K P SCHUPKE writes:
>
> > 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
>
> Oleg described a similar technique a few months ago.
>
> From <http://haskell.org/pipermail/haskell/2004-June/014271.html>:
>
> |> newtype NonEmpty a = NonEmpty [a] -- the NonEmpty constructor
should
> |> -- be hidden (not exported from its module)
> |>
> |> head' (NonEmpty a) = head a -- no error can occur! Can use unsafe
> version
> |> tail' (NonEmpty a) = tail a -- no error can occur! Can use unsafe
> version
> |>
> |> -- trusted function: the only one that can use NonEmpty
constructor.
> |> fork_list_len f g x = if null x then f else g (NonEmpty x)
> |>
> |> revers x = revers' x []
> |> where
> |> revers' x accum = fork_list_len accum (g accum) x
> |> g accum x = revers' (tail' x) ((head' x):accum)
>
> We have these equivalences:
>
> toNonEmptyList == fork_list_len Nothing Just
> fork_list_len d f == maybe d f . toNonEmptyList
>
> I think defining 'toNonEmptyList' in terms of 'fork_list_len' is
> cleaner, but that's just my personal taste. (As it happens, I ended up
> defining a very similar function 'cons' in my recursion module[1]).
>
> [1]
> <http://www.eyrie.org/~zednenem/2004/hsce/Control.Recursion.html#v%
> 3Acons>
--
David Menendez <zedn...@psualum.com> <http://www.eyrie.org/~zednenem/>
Ketil Malde
>> As for head, I think it's fine that it throws an error because it is
>> specified to be defined for only non-empty lists.
> But surely it is better to encode this fact in the type system by
> useing a separate type for non-empty lists.
Yes, in principle. But that means you still need to write more and
tedious code to deal with it.
And there's a question how far you can practically get with this
approach. Are you going to discard lists in favor of tuples, just
because the type systems can't verify that the index passed to (!!) is
witin range?
>> A mechanism for a function to report the caller site would obliviate
>> the need for all this ugliness
> Unfortunately the cost of this is prohabative as the call stack
> would have to contain backtrace information. Also due to lazy
> evaluation the 'call site' may not be what you expect.
AFAICS, this disadvantage is shared by all other schemes of "labeling"
call sites. The only difference is that I want to do it automatically
(perhaps when a debug option is passed to the compiler)
I don't want it for all functions or anything, just the annoying,
small, and commonly used "leaf functions".
> Here's what John Meacham had to say:
> -----------------------------------
> Note that pattern matching rather than deconstruction functions have a
> number of benefits, not just relating to error messages, consider two
> functions which use the head of their argument.
> f xs = ... head xs ...=20
> g (x:_) = ... x ...
> now, g is superior to f in several ways,=20
I agree with this. How about constructs like
mins = map (head.sort)
Is
mins = map ((\(x:_)->x).sort)
still so superior? Is it really necessary to sacrifice code clarity
just to get decent error messages?
And how do you extend this approach to 'read' and (!!)?
-kzm
--
If I haven't seen further, it is by standing in the footprints of giants
MR K P SCHUPKE
>tedious code to deal with it.
Just because code is tedious does not mean it is not necessary to
handle all corner cases. A robust application does not fail when
given unexpected input.
>Are you going to discard lists in favor of tuples,
Of course not... You can actually define constrained datatypes where
the maximum length is a parameter of the type. Unfortunately in haskell
because these values have to be at the type level we end up encoding
them as Peano numbers... See Conor McBrides "Faking It" paper for
some examples of how to do this. Also see Oleg, Ralf and My paper
"Stronly Typed Heterogeneous Lists" to se how far you can get with
these techniques (we define a heterogeneous list that can be constrained
in many ways, including by length, or content type).
I guess in a way you are nearly right as these techniques fundamentaly
us binary products like (,) - but thats also exactly what any binary
constructor including ':' is anyway...
>The only difference is that I want to do it automatically
My point was that you can manually label some functions, but to automatically
do it for all functions is going to cause big stack space problems - think
about recursive functions... or mutually recursive functions...
Keean.
MR K P SCHUPKE
>mins = map ((\(x:_)->x).sort)
maybe what you meant was:
case sort x of
(x:_) -> ... do whatever with x ...
_ -> ... do failure conition ...
As I said, if you can _guarantee_ non failure I guess head is okay, but the
fact that this thread started with the observation that the error produced
by head is difficault to track dow
n we must conclude that programmers make mistakes and cannot be trusted to
make such guarantees .... Hence my suggestion to use the type system.
Effectively the 'case' forms a guarantee of non-emtyness for the stuff in
the case... but you cannot pass this guarantee into functions like 'head'
Using the type system to encode such things allows this 'guarantee' to
be passed into functions...
David Roundy
> Is there any easy way (TH?) to amend these to output the line number
> of the offending caller? It would be a great improvement to see
> something like
>
> Prelude.head : empty list in Foo.hs, line 4711
>
> since programs generally contain many, many calls to functions like
> these.
I include the following file in most files (and always use the C
preprocessor):
import DarcsUtils ( bug )
#define impossible (bug $ "Impossible case at "++__FILE__++":"++show (__LINE__ :: Int)++" compiled "++__TIME__++" "++__DATE__)
#define fromJust (\m -> case m of {Nothing -> bug ("fromJust error at "++__FILE__++":"++show (__LINE__ :: Int)++" compiled "++__TIME__++" "++__DATE__); Just x -> x})
Here "bug" is a function that just calls "error" with a little prefix
explaining that there is a bug in darcs, and would the user please report
it. Obviously, defining a head here would be just as easy, but I usually
have more trouble with fromJust, which in a few places gets called in
internal routines where I *should* know that the data structure has no
Nothings, but have been known to make mistakes.
I also catch all "error" exceptions and print a nicer error message, so I
use fail and error "raw" to indicate actual user errors.
--
David Roundy
http://www.abridgegame.org
Malcolm Wallace
> Hmm...if I run it through CPP and
> #define HEAD (\x -> if null x then error ("__FILE__:__LINE__") else head x)
> is the __LINE__ resolved at the place of declaration or at the place of usage?
According to the C standard, at the position of /usage/ of the macro `HEAD'.
Incidentally, cpphs does not yet implement __FILE__ or __LINE__
replacements. Is their usage widespread amongst Haskell users?
Regards,
Malcolm
Ketil Malde
>> mins = map ((\(x:_)->x).sort)
> maybe what you meant was:
> case sort x of
> (x:_) -> ... do whatever with x ...
> _ -> ... do failure conition ...
No, I don't think so. I only want the bug to be reported, and the
umatched pattern will do it nicely.
>> Yes, in principle. But that means you still need to write more and
>> tedious code to deal with it.
> Just because code is tedious does not mean it is not necessary to
> handle all corner cases. A robust application does not fail when
> given unexpected input.
But if I use head, I should *know* that I never pass it an
empty list. Whether head returns a Nothing or just crashes doesn't
matter, I have to go and fix my *design*, because it has a bug,
and not a "corner case" that should be "handled".
>> Are you going to discard lists in favor of tuples,
> Of course not... You can actually define constrained datatypes where
> the maximum length is a parameter of the type.
>>The only difference is that I want to do it automatically
> My point was that you can manually label some functions, but to automatically
> do it for all functions is going to cause big stack space problems - think
> about recursive functions... or mutually recursive functions...
Yes, of course. So *my* point is that it would be really nice to
write small leaf functions like these with an implicit file/line
parameter that identified the caller site, in order to avoid
cluttering the code with them.
Okay, perhaps I'm not using the type system to its full extent, but I
think this is fairly common practice.
An easy solution seems to be to use -cpp and add
#define head (\(x:_)->x)
at the top of the relevant source files. However, I'm not sure how to
make this work with the other difficult functions. Another
alternative (basically emulating the GHC's behavior in the above case)
is
#define head (\x -> case x of {(x:_) -> x; _ -> error ("head failed at "++__FILE__++":"++ show __LINE__)})
It seems difficult to generalize this, though.
-kzm
--
If I haven't seen further, it is by standing in the footprints of giants
MR K P SCHUPKE
I think preventing the bug using the type system if possible is a good
idea... something that should be encouraged!
>and not a "corner case" that should be "handled".
So if the list depends on user input is not the empty list a corner
case of the function on user input?
>write small leaf functions like these with an implicit file/line
This is a good idea - If I have given the impression I am opposed to it
then I have not expressed myself very well. I just think where this can
be avoided using the type system in the first place is an even better
idea. Design by contract is the way forward for large complex systems,
and where that contract can be expressed using the type system is
a selling point for Haskell in such applications.
>It seems difficult to generalize this, though.
Again for read you can use "reads"...
Sven Panne said:
"reads" is probably what you are looking for:
Prelude> (reads :: ReadS Integer) ""
[]
Prelude> (reads :: ReadS Integer) "a"
[]
Prelude> (reads :: ReadS Integer) "2"
[(2,"")]
Prelude> (reads :: ReadS Integer) "123blah"
[(123,"blah")]
Keean.
Ketil Malde
> Here "bug" is a function that just calls "error" with a little prefix
> explaining that there is a bug in darcs, and would the user please report
> it. Obviously, defining a head here would be just as easy,
Cool! The basic trick is just to inline the actual function
defintions using CPP macros. I've made macros for most of the
troublesome functions, but I can't get it to work for operators
(something like `(!!)` doesn't parse, it seems) Any tricks?
Unless I'm overlooking something, I could have a file prelude.h
containing something like:
----8<------
import Prelude hiding (head,(!!),read)
#define head (\xs -> case xs of { (x:_) -> x ; _ -> bug "head" __FILE__ __LINE__})
#define at (let {at (y:_) 0 = y; at (y:ys) n = at ys (n-1); at _ _ = bug "at" __FILE__ __LINE__} in \a x -> at a x)
#define read (\s -> case [ x | (x,t) <- reads s, ("","") <- lex t] of { [x] -> x ; _ -> bug "read" __FILE__ __LINE__})
#define fromJust (\x -> case x of Just a -> a; Nothing -> bug "fromJust" __FILE__ __LINE__)
bug c f l = error ("Program error - illegal parameters to '"++c++"', file '"++f++"', line "++show l)
----8<------
and just #include "prelude.h" if/when I want better debugging. No
expensive stack frames, no unwanted strictness, and no clutter.
Any comments?
-kzm
--
If I haven't seen further, it is by standing in the footprints of giants
Ketil Malde
> Unless I'm overlooking something
Which I of course did.
> #define at (let {at (y:_) 0 = y; at (y:ys) n = at ys (n-1); at _ _ = bug "at" __FILE__ __LINE__} in \a x -> at a x)
No prize for spotting the bug here.
Ketil Malde
> import Prelude hiding (head,(!!),read)
> Any comments?
Here's one: I thought this would make it difficult to have other
imports of Prelude, hiding other pieces of it (e.g. catch, to avoid
ambiguities with Control.Exception.catch)
(Also, the definition of 'bug' hinders forces the #include to be after
any imports, not sure it's better to have a separate module for it,
which would then need to be on the module search path)
(I seem to be mainly following up to my own posts, so if somebody
asks, I'll take this to a quiet corner at the -cafe :-)
John Meacham
{-# INLINE #-} could 'get at' their inlining point. like
{-# INLINE head #-}
head (x:_) = x
head _ = error $ {-# ERRLOC #-} "head: empty list"
the semantics being that when inlining {-# ERRLOC #-} is rewritten to
(\s -> "Foo.hs:24: " ++ s) (with Foo.hs and 24 replaced by the inlining
point).
Note that this is designed so that if the compiler does not support
ERRLOC or head could not be inlined for some reason, it degrades
gracfully.
John
--
John Meacham - ⑆repetae.net⑆john⑈
André Pang
>> 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
MR K P SCHUPKE
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.
Alastair Reid
> 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
MR K P SCHUPKE
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.
Conor T McBride
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
André Pang
> 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
_______________________________________________
Adam Megacz
Alastair Reid <alas...@reid-consulting-uk.ltd.uk> writes:
> I think the value of Haskell's type system is that it catches a lot of bugs
> _cheaply_.
I've heard the argument before that "unit testing" is a stochastic
approximation of strong typing. ;)
Sadly these days, a horde of mediocre programmers is generally cheaper
than a single programmer who understands Haskell's type system.
- a
MR K P SCHUPKE
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.
Keith Wansbrough
>
> 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-)
MR K P SCHUPKE
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.
Graham Klyne
>Static guarantees are great, but if you have to explicitly change your
>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
MR K P SCHUPKE
>>style of coding to cope with those extra constraints, it can become (very)
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.
Keith Wansbrough
> 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-)
MR K P SCHUPKE
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.
MR K P SCHUPKE
>instance HLe HZero HZero
>instance HLe x y => HLe (HSucc x) (HSucc y)
Erm of course this was the definition for Equals, not less than or
equals!
class HLe n n'
instance HLe HZero x
instance HLe x y => HLe (HSucc x) (HSucc y)
Is the definition for less than or equals... but it took me all of
5 seconds to realise the first definition I gave was wrong - because
it is so simple...
Duncan Coutts
> >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)
Somewhat off-topic,
It's when we write classes like these that closed classes would be
really useful.
You really don't want people to add extra instances to this class, it'd
really mess up your proofs!
I come across this occasionally, like when modelling external type
systems. For example the Win32 registry or GConf have a simple type
system, you can store a fixed number of different primitive types and in
the case of GConf, pairs and lists of these primitive types. This can be
modelled with a couple type classes and a bunch of instances. However
this type system is not extensible so it'd be nice if code outside the
defining module could not interfere with it.
The class being closed might also allow fewer dictionaries and so better
run time performance.
It would also have an effect on overlapping instances. In my GConf
example you can in particular store Strings and lists of any primitive
type. But now these two overlap because a String is a list. However
these don't really overlap because Char is not one of the primitive
types so we could never get instances of String in two different ways.
But because the class is open the compiler can't see that, someone could
always add an instance for Char in another module. If the class were
closed they couldn't and the compiler could look at all the instances in
deciding if any of them overlap.
So here's my wishlist item:
closed class GConfValue v where
...
Duncan
Ketil Malde
> closed class GConfValue v where
Hmm...doesn't
--8<--
module Closed(foo) where
class C a where foo = ...
instance C ...
--8<--
module Main where
import Closed
...foo...
--8<--
do what you want? You can only use existing instances of C, but not
declare them (outside of the Closed module), IIUC.
-ketil
--
If I haven't seen further, it is by standing in the footprints of giants
Malcolm Wallace
> Duncan Coutts <duncan...@worcester.oxford.ac.uk> writes:
>
> > closed class GConfValue v where
>
> Hmm...doesn't
>
> --8<--
> module Closed(foo) where
> class C a where foo = ...
> instance C ...
> --8<--
> module Main where
> import Closed
> ...foo...
> --8<--
>
> do what you want? You can only use existing instances of C, but not
> declare them (outside of the Closed module), IIUC.
Ah, but now you cannot use (Closed t) => as a predicate in type
signatures, and since you cannot write a partial signature, you must
omit the signature altogether...
Regards,
Malcolm
MR K P SCHUPKE
You want a closed type?
The parameter to a class is a type...
Actually if you allow undecidable instances you can use the generic
instance to close the class
class OnlyInt a
instance OnlyInt Int
instance Fail () => OnlyInt x
Where Fail is a class with no instances, that is not exported!
If you try and add an instance to OnlyInt the program will fail
with overlapping instances.
Keean.
Duncan Coutts
> > Hmm...doesn't
> >
> > --8<--
> > module Closed(foo) where
> > class C a where foo = ...
> > instance C ...
> > --8<--
> > module Main where
> > import Closed
> > ...foo...
> > --8<--
> >
> > do what you want? You can only use existing instances of C, but not
> > declare them (outside of the Closed module), IIUC.
>
> Ah, but now you cannot use (Closed t) => as a predicate in type
> signatures, and since you cannot write a partial signature, you must
> omit the signature altogether...
A similar non-solution is to export the class name but not the class
methods, so you cannot defined them in other modules.
However this doesn't help if there are default methods or no methods,
you can still say:
instance ClosedClass Foo
Note the lack of 'where' keyword.
Granted, for most classes this would stop other modules interfering but
it doesn't give the optimisation opportunities or the better overlapping
instance detection.
Duncan
Ketil Malde
> Ah, but now you cannot use (Closed t) => as a predicate in type
> signatures, and since you cannot write a partial signature, you must
> omit the signature altogether...
Hmm..yes, that would be a disadvantage. :-)
-ketil
--
If I haven't seen further, it is by standing in the footprints of giants
André Pang
>> 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
_______________________________________________
Duncan Coutts
> class OnlyInt a
> instance OnlyInt Int
> instance Fail () => OnlyInt x
>
> Where Fail is a class with no instances, that is not exported!
>
> If you try and add an instance to OnlyInt the program will fail
> with overlapping instances.
Very nice.
However I think I still need to use allow-overlapping-instances because
[Char] and GConfPrimitiveValue a => [a] still overlap. If closes classes
were a language feature the typechecker would see that the do not
overlap since there is no instance GConfPrimitiveValue Char.
Duncan
André Pang
> 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.
One feature I've always wanted is to be able to tell the compiler or
run-time system (whichever is responsible for enforcing the type
checks) to turn on exception checking or not. That way, if you are
programming in a fast and loose style (e.g. writing a throwaway
script), exceptions don't get in your way, and you can program
unencumbered by lots of useless error checking code. If you then
decide that the throwaway script isn't so throwaway after all, insert a
pragma in your program, and get back full static checking.
If you know Perl, it's the equivalent of 'use strict;' for exceptions.
I hope to see such a design in a Haskell compiler one day ...
--
% Andre Pang : trust.in.love.to.save
_______________________________________________
ol...@pobox.com
Malcolm Wallace wrote:
> and since you cannot write a partial signature,
Can't we really?
It seems `partial signature' means one of two things:
- we wish to add an extra constraint to the type of the function
but we don't wish to explicitly write the type of the
function and enumerate all of the constraints
- we wish to specify the type of the function and perhaps some
of the constraints -- and let the typechecker figure out the
rest of the constraints.
Both of the above is easily possible, in Haskell98.
In the first case, suppose we have a function
> foo x = Just x
and suppose we wish to add an extra constraint (Ord x) but without
specifying the full signature of the function. We just wish to add one
constraint.
> addOrd:: (Ord x) => x -> a
> addOrd = undefined
>
> foo' x | False = addOrd x
> foo' x = Just x
Even a not-so-sufficiently smart compiler should be able to eliminate
any traces of the first clause of foo' in the run code. So, the recipe
is to define a function like `addOrd' (or like an identity), give it
the explicit signature with the desired constraint, and then `mention'
that function somewhere in the body of foo. Or, as the example above
shows, prepend a clause of the form
foo arg ... | False = addOrd arg ...
In that case, the body of the function foo does not have to be changed at
all.
For the second case: suppose we wrote a function
> bar a i = a ! i
and wish to give it a type signature
*> bar:: Array i e -> i -> e
But that won't work: we must specify all the constraints:
Could not deduce (Ix i) from the context ()
arising from use of `!' at /tmp/d.lhs:207
Probable fix:
Add (Ix i) to the type signature(s) for `bar'
In the definition of `bar': bar a i = a ! i
But what if we wish to specify the type without the constraints (and
let the compiler figure the constraints out)? Again, the same trick
applies:
> barSig:: Array i e -> i -> e
> barSig = undefined
>
> bar' a i | False = barSig a i
> bar' a i = a ! i
Incidentally, barSig plays the role of a Java interface of a
sort. barSig is a bona fide function, and can be exported and
imported. To make sure that some other function baz satisfies the
barSig interface (perhaps with a different set of constraints), all we
need to do is to say
baz arg1 ... | False = barSig arg1 ...
We can also attach to barSig some constraints. The typechecker will
figure out the rest, for bar' and baz.
Ketil Malde
> As Keith said, Java will check at compile time whether or not you
> handle the exception.
This sounds very tedious! The right thing to do if you don't handle
them, is of course to propagate exceptions up; however, then you need
to update a 'throws' clause as you modify your implementation.
Sounds like a job for...Type Inference! Wouldn't it be nice if GHCi
and Hugs' ":i foo" would tell you about the exceptions it could throw?
(No idea how feasible that would be, and I may have misunderstood
stuff - it's ages since I wrote Java code)
-ketil
--
If I haven't seen further, it is by standing in the footprints of giants
MR K P SCHUPKE
In Olegs post where he gave examples of how to make exceptions explicit
in type signatures:
oleg said:
> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
>
> module TER where
>
> class CERROR a c where
> darn:: a -> c-> String -> b
>
> instance Show a => CERROR a c where
> darn label _ msg = error $ "Error: " ++ (show label) ++ " " ++ msg
>
>
> data EHead = EHead deriving Show
> data ETail = ETail deriving Show
> data EJust = EJust deriving Show
>
> myhead x@([]) = darn EHead x "head of an empty list"
> myhead (x:_) = x
>
> mytail x@([]) = darn ETail x "tail of an empty list"
> mytail (_:xs) = xs
Now, if we ask GHCi for the type of myhead, we get
*TER> :t myhead
myhead :: forall a. (CERROR EHead [a]) => [a] -> a
----------------------------------------------------------
As you can see you get the advantage of explicit exceptions,
but with type inference.
Keean.
Alastair Reid
> This sounds very tedious! The right thing to do if you don't handle
> them, is of course to propagate exceptions up; however, then you need
> to update a 'throws' clause as you modify your implementation.
>
> Sounds like a job for...Type Inference! Wouldn't it be nice if GHCi
> and Hugs' ":i foo" would tell you about the exceptions it could throw?
Do you just want exceptions to be displayed by an interpreter or do you want
them used in the compiler (i.e., part of the Haskell language).
I think it is straightforward enough to annotate expressions with the
exceptions they can raise. As a first attempt, I'll use e :: ty^ex to
indicate that an expression e has type ty and can raise exceptions ex.
1/0 :: Int^DivZero
[1/i | i <- [0..]] :: [Int^DivZero]
head [1/i | i <- [0..]] :: Int^{DivZero,Head_Empty}
There's a few problems with simply adding this to Hugs/GHC as they stand
though:
1) The exception parts of the types I showed should be types but, at
present they are values.
2) Since exceptions accumulate towards the root, it's common to have a
way of summarising a set of exceptions. Usually, this is done using
some notion of inheritance so that numeric overflow, division by zero,
etc might be summarized as 'ArithmeticError'.
(Often the inheritance graph is a tree but I suspect it would be useful
to have a DAG and to be able to define your own DAG just as you can
define your own inheritance using type classes.)
3) This doesn't take the non-deterministic part of Haskell exceptions
into account. Implementing the rules in the paper would be a good way
of checking that the rules capture all the transformations that
compilers like GHC do. Of course, to do this, you really need to push
the exception-types all the way through the optimizer since it is the
optimizer that introduces non-determinism.
--
Alastair Reid
Ketil Malde
> Do you just want exceptions to be displayed by an interpreter or do you want
> them used in the compiler (i.e., part of the Haskell language).
I think it would be difficult, and perhaps undesirable, to make it
part of the language. So my immediate thought was that an interactive
system could note any calls to functions that could produce exceptions
(e.g. performing file operations, division, calls to
undefined/error/fail, incomplete patterns...) and tell the user in the
response to the :i command.
> I think it is straightforward enough to annotate expressions with the
> exceptions they can raise.
Oleg (reposted by Kean) manages this, but as far as I understand it,
it requires additional work by the programmer.
As I said, I don't have a lot of experience working with Java, but
cluttering the type( annotation)s with exceptions seems to be
tedious, especially when you really just want to propagate the
exception. E.g. if I rewrite a function so that it no longer uses
division, I must potentially change all types up to the level where
division-by-zero would be handled.
Knowing programmers, I worry that people will write dummy catch
clauses that only serve to sweep the exception under the rug.
> 2) Since exceptions accumulate towards the root, it's common to have a
> way of summarising a set of exceptions. Usually, this is done using
> some notion of inheritance so that numeric overflow, division by zero,
> etc might be summarized as 'ArithmeticError'.
Doesn't this lose information? I can see why it is useful to *catch*
larger classes of error, in particular high up when you only deal with
it in a generalized way (e.g. reporting the error to the user), but
isn't it also useful to know exactly the kinds of error that can
occur?
-ketil
--
If I haven't seen further, it is by standing in the footprints of giants
Simon Peyton-Jones
case is to allow the programmer to declear new kinds, as well as new
types. This is what Tim Sheard's language Omega lets you do, and I'm
considering adding it to GHC.
kind HNat = HZero | HSucc HNat
class HNatC (a::HNat)
instance HNatC HZero
instance HNatC n => HNatC (HSucc n)
Here the keyword 'kind' is like 'data', except that it introduces a new
*kind* HNat with new *type* constructors HZero and HSucc, rather than a
new *type* constructor with new *data* constructors.
There is no way to construct a value of type HZero, or (HSucc HZero);
these are simply phantom types. Today we are forced to say
data HNat
data HSucc a
which loses the connection between the two. A merit of declaring a kind
is that the kind is closed -- the only types of kind HNat are HZero,
HSucc HZero, and so on. So the class doesn't need to be closed; no one
can add new instances to HNatC because they don't have any more types of
kind HNat.
At the moment I'm only thinking of parameter-less kind declarations but
one could easily imagine kind parameters, and soon we'll have kind
polymorphism.... but one step at a time.
Any thoughts?
Simon
| closed class GConfValue v where
| ...
|
| Duncan
C T McBride
On Mon, 9 Aug 2004, Simon Peyton-Jones wrote:
> Closed classes are certainly interesting, but a better way to go in this
> case is to allow the programmer to declear new kinds, as well as new
> types. This is what Tim Sheard's language Omega lets you do, and I'm
> considering adding it to GHC.
>
> kind HNat = HZero | HSucc HNat
>
> class HNatC (a::HNat)
>
> instance HNatC HZero
> instance HNatC n => HNatC (HSucc n)
>
[..]
> At the moment I'm only thinking of parameter-less kind declarations but
> one could easily imagine kind parameters, and soon we'll have kind
> polymorphism.... but one step at a time.
>
> Any thoughts?
Yes. "Yes please."
This is still in the realm of using type-level proxies for values,
but it's a much more practical fake of dependent types than you can
manage with type classes. It lets you do quite a lot of the handy
indexing that's found in basic dependently typed programs, without
quite crossing the line to full-on value dependency. Of course, I
recommend crossing this line in the long run, but I accept that doing
so might well mess things up for GHC. This is a sensible, plausible
step in the right direction. And I'm sure you'll be able to jack it
up to datakinds parametrized by datakinds, provided all the indices
are in constructor form: the unification apparatus you've already got
for datatype families (or GADTs as you've dubbed them) should do
everything you need, as long as you unify the indices before you
unify the indexed `values'.
What you still don't get is the ability to use datatype families to
reflect on values in order to extend pattern matching, the way James
McKinna and I do in `The view from the left'. But one step at a time.
You also don't get for free the ability to write type-level programs
over these things. If you do add type-level programs over datakinds,
you may find that the unification-in-the-typing-rules style comes
under strain. I'm told that's why the ALF crew retreated from full-on
datatype families, which is why they're not in Cayenne. The Epigram
approach is different: the unification problems are solved internally
to the theory, so you still get the solutions when they're easy, but
the wheels don't come off when they're not.
Even so, you do get quite a long way towards the `static' uses of
dependent types which support n-ary vectors and the like, but where
n isn't supposed to be a run-time value. You'll get `projection
from a vector is exception-free'; you won't get `projection from a
vector returns the thing in that position in the vector'.
So let's have this, and we'll see how many of the programs I've
written in the last 5+ years with these data structures become
Haskell programs. More than a few, I expect.
Cheers
Conor
Peter G. Hancock
> At the moment I'm only thinking of parameter-less kind declarations but
> one could easily imagine kind parameters, and soon we'll have kind
> polymorphism.... but one step at a time.
> Any thoughts?
Apologies if it's widely known, but a system with "kind polymorphism"
was first considered by Girard (in 1971!). It's mentioned in Appendix A
of "The System F of Variable Types, Fifteen Years Later" by Girard in
"Logical Foundations of Functional Programming", ed Huet,
Addison-Wesley 1990, pp 87-126. There he calls it "system U".
It is inconsistent, and non-normalising (as a logical system). The
implications of this for type-checking "should be considered very
cautiously" (to borrow Girard's words).
Peter Hancock
MR K P SCHUPKE
mind - what is the parameter of a kind statement (a type or a kind... a
kind makes more sense) ... do we have to stop with kinds what about
"kinds of kinds" - the statement has identical syntax to a data declaration,
is there no way to combine the two, with perhaps a level value?
An example of where you may need kinds-of-kinds (etc) is consider peano numbers
(declared as a kind) ... now consider we have several implementations
(unary - binary etc) which we wish to group together as an equivalent
to the Num class.
I accept the above is not a good example as this is better served by a class
(as you may well want it 'open')...
It seems from a theoretical point of view easy to add multiple levels of
kinds instead of one level... of course it is probably much more difficault
to do this to GHC?
Of course with kinds of kinds you either have to annotate the statement
with the level - or let the compiler infer the level. The latter seems
much more difficault as the same 'level-less-kind statement' could be
used on multiple levels...
Keean.
ol...@pobox.com
Simon Peyton-Jones wrote:
> kind HNat = HZero | HSucc HNat
>
> class HNatC (a::HNat)
>
> instance HNatC HZero
> instance HNatC n => HNatC (HSucc n)
>
> There is no way to construct a value of type HZero, or (HSucc HZero);
> these are simply phantom types. ... A merit of declaring a kind
> is that the kind is closed -- the only types of kind HNat are HZero,
> HSucc HZero, and so on. So the class doesn't need to be closed; no one
> can add new instances to HNatC because they don't have any more types of
> kind HNat.
With the flag -fallow-overlapping-instances, could I still add an instance
instance HNatC n => HNatC (HSucc (HSucc n))
or
instance HNatC (HSucc HZero)
??
If I may I'd like to second the proposal for closed classes. In some
sense, we already have them -- well, semi-closed. Functional
dependencies is the way to close the world somewhat. If we have a
class
class Foo x y | x -> y
instance Foo Int Bool
we are positive there may not be any instance 'Foo Int <anything>'
ever again, open world and -fallow-overlapping-instances
notwithstanding. In fact, it is because we are so positive about that
fact that we may conclude that "Foo Int x" implies x = Bool. At least
in the case of functional dependencies, the way to close the world gives
us type improvement rules. One might wonder if there are other ways
to (semi-)close the world with similar nice properties.
Duncan Coutts
[snip]
> and have found myself wondering if type-level lambda abstraction
> wouldn't be a useful feature to overcome this.
>
> Your suggestion seems to be another feature in the same vein: extending
> data features to types. I find myself wondering where this might all
> end. If types acquire many of the manipulations that are available for
> data values, then might one find that, in turn, cases will be found that
> seem to require similar capabilities for kinds?
>
> Is there any possibility of a theory that will avoid the need to replicate
> features at higher and higher levels?
As people have bee discussing recently on this list, this is what
dependent types gives you. Instead of having a hierarchy of
values->types->kinds-> ... where each is classified by the one above it
(values by types, types by kinds), dependent types allow you to have
types that depend on values in your program. It does indeed allow you to
manipulate types using the same manipulations that are available for
ordinary data values.
The trade off however is that the value system must be decidable (no
bottom allowed) or otherwise the type system is undecidable. There are
other ways of making the trade off that do allow you use general
recursion when you really need to (as Conor posted recently), but then
you loose the ability to prove certain things about your programs within
the type checking framework and you would have to go back to external
proofs. (Of course this is the situation in Haskell anyway, that these
kinds of proofs have to be done externally to the program)
Duncan
John Meacham
> At the moment I'm only thinking of parameter-less kind declarations but
> one could easily imagine kind parameters, and soon we'll have kind
> polymorphism.... but one step at a time.
>
> Any thoughts?
>
My first thought is I am going to need a better editor mode that can
tell from context whether an identifier is a value, type, or kind (or
meta-kind?) constructor and differentiate them visually :)
would these kind constructors need to be encoded into system F or the
lambda cube, or would it be possible that they be eliminated right
after typechecking or easily desugared away like classes?
The idea is quite interesting. I was thinking about explicit kinds the
other day, but just as an idle curiosity, now that this thread has
provided some real-world interesting uses, I will have to think about
them some more :)
John
--
John Meacham - ⑆repetae.net⑆john⑈
MR K P SCHUPKE
>features at higher and higher levels?
If we consider types, types are a collection of values, for example we could
consider Int to be:
data Int = One | Two | Three | Four ...
Okay, so the values in an integer are connected by functions (operations
like plus, multiply) - but we can consider these externally defined (as they
are primitives). Also we have special symbols for the values of this type
(type constructors are 'values') like 1, 2, 3... etc.
Likewise Char is effectively an enumeration of ascii values (or Unicode
values). All these standard types behave like enumerations of values.
Lists are effectively nested binary products:
data List a = Cons a (List a)
But I digress, my point is that types are a 'set' of values, and so
we can consider the simplest example:
data Bool = True | False
So bool is a type and True and False are the values 'in' that type - _but_
we can also write:
kind Bool = True | False
Where Bool is a kind and True and False are values, Kinds are really a different
name for "type_of_types"... and this continues upwards forever (a
type_of_type_of_types) ... we can effectively flatten this by considering
types as values and kinds as types. What is the difference between a type
and a value?
So we can consider: "data Bool = True | False" to be a relationship between
elements at the Nth level (the RHS) and the N+1th level (the LHS). This
relationship could be applied at any level, and it should be possible to
detemine the level at which we wish to apply this relationship by the
context in which it is used.
Imagine a function 'not':
not :: Bool -> Bool
not True = False
not False = True
we could apply this at the values level:
> not True
False
The type level:
class (Bool a,Bool b) => Not a b
| a -> b
instance True False
instance False True
How does this differ from the original functional form?
can we imagine doing:
not' :: Not a b => a -> b
but perhaps writing it:
not' :: Bool a => a -> not a
After all is not 'not' a complete function from Bool to Bool, whatever Bool is?
(Bool could be a type or a type of types, or a type of type of types...)
Would this not result in greater code re-use? Perhaps classes would become redundant
(apart from being used to allow overloading...)
My theory here is a bit shakey - but the name Martin Lof springs to mind.
Keean.
*errata - when I said "Where Bool is a kind and True and False are values" I of course
meant w
true and false are types!
Frank Atanassow
> Closed classes are certainly interesting, but a better way to go in
> this case is to allow the programmer to declear new kinds, as well as
> new types. This is what Tim Sheard's language Omega lets you do, and
> I'm considering adding it to GHC.
FWIW, Martin Wehr designed a Haskell-like type system with:
* not only datakinds, but datasuperkinds, datasupersuperkinds, etc., in
short, data-n-types for every finite dimension n, all parametric,
* along with parametrically polykinded, polysuperkinded, etc., in
short, poly-n-morphic functions,
* along with map, simple folds and nested folds for all these things,
* not to mention an algorithm for principal type inference
in his 1998 paper:
@misc{ wehr98higher,
author = "M. Wehr",
title = "Higher order algebraic data types",
text = "Martin Wehr. Higher order algebraic data types
(full paper). Technical report, University of
Edinburgh, URL
http://www.dcs.ed.ac.uk/home/wehr, July 1998.",
year = "1998",
url = "citeseer.nj.nec.com/wehr98higher.html"
}
The title of the paper is a bit misleading: "higher-dimensional" is
better than "higher-order", as higher-order functions are the chief
thing missing from Wehr's system. But these are easily added in the
standard fashion, which is to say, only at the value level, and by
simply neglecting the problem of defining folds for datatypes involving
(->).
Two significant differences between Wehr's system and the one Simon
described is that every kind in Wehr's system has values, and there is
no distinguished kind *.
I tried to champion this (very incoherently) in a talk at the Hugs/GHC
meeting in, I think, 2000, where Tim also presented some of his early
ideas on datakinds.
(BTW, given such an expressive system, I think you may find, as I did,
that the number of ways to represent what amount to essentially the
same type grows ridiculously large, and this is one of the motivations
for treating more general notions of type equivalence than equality,
like for example canonical isomorphy as I am doing in a forthcoming
paper.)
There is also an extended abstract of Wehr's paper in CTCS (no citation
handy---I'm posting this from at home), and a categorical semantics
which is, however, not for the faint of heart:
@article{ wehr99higherdimensional,
author = "Martin Wehr",
title = "Higher-dimensional syntax",
journal = "Electronic Notes in Theoretical Computer Science",
volume = 29,
year = 1999,
url = "citeseer.nj.nec.com/wehr99higher.html"
}
Eelco Visser also defines a notion of multi-level type system, and
gives several examples of how they can be used, in his PhD thesis. One
of the examples, as I recall, shows how datakinds and polykinded
functions subsume uni-parameter type classes (without overlapping
instances).
Regards,
Frank