[Haskell-cafe] ANNOUNCE: tagged-list v1.0

[Jonas Almström Duregård]

Hi Gregory,

What can i do with the list i get from join (TaggedList (Plus m n))? I can't
use head or tail on it... Maybe something like:

shiftl :: TaggedList (Plus (SuccessorTo m) n) -> TaggedList (SuccessorTo
(Plus m n))

I'm still not sure there's an actual case where it's useful... You could
make a class of non-empty lists:

class NonEmpty n where
 head :: TaggedList n b -> b
 tail :: TaggedList n b -> TaggedList (? n) b

instance NonEmpty (SuccessorTo a) where
 head = theOldHeadFunction
 tail    = ?

instance (NonEmpty m, NonEmpty m) => NonEmpty (Plus n m) where
 head = Prelude.head . toList
 tail    = ?

All you need to do is invent a suitable predecessor type (including its
NonEmpty instance) and do the magic for tail. :)


Also, what is UntaggedList used for, and how is it different from [].

/J




On 14 October 2010 04:17, Gregory Crosswhite <gcross at phys.washington.edu>
wrote:
>
>  Hey everyone,
>
> I am pleased to announce the release of tagged-list version 1.0, a package
which provides fixed-length lists that are tagged with a phantom type-level
natural number corresponding to the length. The advantage of such lists is
that you can make static guarantees about them, so that for example the
function
>
> addLists :: TaggedList n Int -> TaggedList n Int -> TaggedList n Int
> ...
>
> which adds two lists is guaranteed to get two lists of the same length and
to produce a list with the same length as the inputs. Some basic operations
on these lists have been provided, including instances for Applicable,
Traversable, etc. One of the more interesting of these operations is the
"join" function",
>
> join :: TaggedList m α → TaggedList n α → (TaggedList (Plus m n)
α,TaggedList (Plus m n) β → (TaggedList m β,TaggedList n β))
>
> This function takes two lists and appends them, and returns not only the
appended list but also a function that takes a list of the same length and
splits it into two lists with the same lengths as the inputs; one way of
interpreting the second parameter is that it provides a "proof" that a
TaggedList of type TaggedList (Plus m n) β can be broken into lists of type
TaggedList m β and TaggedList n β. This function is provided because I
couldn't figure out how to make a general "split" function pass the
type-checker, and fortunately I found that in practice I didn't need a
general such function because I was usually taking a list that was the
result of some operation applied to two lists I had earlier appended and
breaking the result list into sublists the lengths of the original two
lists.
>
> I also provided functions to convert tagged lists to and from tuples,
which can be useful at the times when the type-checker gets confused by your
"a :. b :. ... :. E" expression and gives you obscure error messages.
>
> Anyway, I hope that the community finds this package useful, and welcome
any feedback that you all have to offer.
>
> Cheers,
> Greg
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20101014/cc60136f/attachment.html