[Haskell-cafe] ANNOUNCE: tagged-list v1.0
Gregory Crosswhite
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
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Christopher Done
Jonas Almström Duregård
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
Jonas Almström Duregård
Gregory Crosswhite
> [...]
>
> Also, what is UntaggedList used for, and how is it different from [].
>
> /J
>
UntaggedList makes it easy for you do things like the following:
processListAsTaggedList :: [a] -> (forall n. TaggedList n a -> b) -> b
processListAsTaggedList xs f =
case fromListAsUntagged xs of
UntaggedList lst -> f lst