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

[Jonas Almström Duregård]

I just noticed Plus is a type family and not a type :), ignore my previous
comment. Nice library!

/J

2010/10/14 Jonas Almström Duregård <jonas.duregard at chalmers.se>

> 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/a6fe6e52/attachment.html