The haddock at http://www-users.cs.york.ac.uk/~ndm/projects/safe/Safe.html doesn't indicate that Safe.List already exists. It seems Safe.List would indeed be a new module in that heirarchy. That said, it may be a bit confusing to see both approaches in the same package, but both do support "safety" (explicit code with good error messages versus static checks). Perhaps actua Regarding decimal numbers, I have a bad habit of not respecting Haskell98 compliance. (Sorry if that sentence just caused any compiler writers to wince.) It is a fine point you raise though. Does the clarity of the decimal types out weigh the type-extensions overhead? Or: do the benefits of Haskell98-compliance merit the verbosity of unary/binary type-level naturals? When we discuss "lightweightness", I think the heavy-lifting of decimals would be contained within the library, not exposed. In particular, the smaller decimal type are so much easier to digest, they could be considered more lightweight than the alternatives (that I've seen). Is that a fair claim? Off-Topic: has On computable types III been release yet? Thank you to Henning, Oleg, Neil, and Alfonso for discussing. On 2/21/07, oleg@pobox.com wrote:

Nicolas Frisby wrote:

...

Some of the code from the previous wiki link, type-level decimal numbers

I would rather advice against type-level decimal numbers, if we are looking at a lightweight solution. The [complete] code at

http://www.haskell.org/haskellwiki/Non-empty_list is Haskell98! It also provides for a head and tail functions -- which are total and so raise no errors.

Incidentally, inserting NList into the existing Safe.List does not seem like a good match as NList critically relies on being in a separate module with a limited export. NList constitutes a security kernel, whose invariants are to be described explicitly (and hopefully, automatically proven at some point). For that reason, it is beneficial to keep module NList separate and compact. It could of course be placed within Safe.* hierarchy, etc -- as a separate module.

Neil Mitchell wrote:

...

Fortunately the problem of pattern match errors is being tackled by at least two projects:

* Catch: http://www-users.cs.york.ac.uk/~ndm/projects/catch.php * ESC-Haskell: http://www.cl.cam.ac.uk/~nx200/research/escH-hw.ps

I would submit the approach of the lightweight static capabilities (cf above Wiki link) to be counted as the third project in that area. The latter has an advantage that it is available in Haskell right now and requires no extra tools.