[Haskell-cafe] naturally, length :: a -> Int

[David Duke]

You might want to revisit the following paper by Colin Runciman -:
author = {Colin Runciman},
    title = {What About the Natural Numbers},
    journal = {Computer Languages},
    year = {1989},
    volume = {14},
    pages = {181--191}
It  makes  similar points and fills out details ...

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.56.3442

regards
David

On Tue, Mar 2, 2021 at 2:56 PM Johannes Waldmann <
johannes.waldmann at htwk-leipzig.de> wrote:

> Dear Cafe,
>
>
> thanks for ideas and arguments.
>
>
> > [Ben Franksen] I would support a move Int->Word in all libraries
> > where that makes sense.
>
> I find it hard to think of a library where that does NOT make sense...
>
>
> The following is somewhat related but actually orthogonal:
> I mentioned that numbers often arise as cardinalities
> (so they are natural, by definition) and serve as pointers.
> The next step is then: pointer type safety. Vincent Hanquez' Foundation
> https://hackage.haskell.org/package/foundation-0.0.25  defines
>
> class (IsList c, Item c ~ Element c) => Collection c where
>   length :: c -> CountOf (Element c)
> class ( ... Collection c) => Sequential c where
>   take :: CountOf (Element c) -> c -> c
>
> with   newtype CountOf ty (and there's also   newtype Offset ty)
>
> I tend to agree. The phantom type argument for CountOf
> would catch errors like adding the number of students
> to the number of exercises (in my application).
>
> (Well and the next step after that would be to have
> the size of the collection in the (dependent) type as well.)
>
> Current implementation is  newtype CountOf ty = CountOf Int
> and the author adds (and that was also the point I was making)
> "Int is a terrible backing type which is hard  to get away from,
> considering that GHC/Haskell are mostly using  this for [counting
> and] offset. Trying to bring some sanity by a lightweight wrapping."
>
>
> NB: I found out about this from Michael Snoyman's
> (very much entertaining, and too much true)
> https://www.snoyman.com/blog/2020/12/haskell-bad-parts-3/
>
>
> Best regards, J.W.
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.



-- 
David Duke
Emeritus Professor of Computer Science
School of Computing University of Leeds UK
E:duke.j.david at gmail.com
W:https://engineering.leeds.ac.uk/staff/334/Professor_David_Duke
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210302/6b41c789/attachment.html>