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 <[email protected]> > 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 <[email protected]> > 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 > > [email protected] > > http://www.haskell.org/mailman/listinfo/haskell-cafe > >
_______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
