[Haskell-cafe] Re: exists . a psuedo-standard non-empty list module

[Nicolas Frisby]

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 at pobox.com <oleg at 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.
>
>
>
>
>