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

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

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 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe