Derek Elkins <derek.a.elkins <at> gmail.com> writes: > > On Sun, Jan 17, 2010 at 2:22 PM, Will Ness <will_n48 <at> yahoo.com> wrote: > > Hello cafe, > > > > I wonder, if we have List.insert and List.union, why no List.merge (:: Ord a => > > [a] -> [a] -> [a]) and no List.minus ? These seem to be pretty general > > operations. > > Presumably by List.minus you mean the (\\) function in Data.List. You > probably also want to look at the package data-ordlist on hackage > (http://hackage.haskell.org/packages/archive/data-ordlist/0.0.1/doc/html/Data- OrdList.html) > which represents sets and bags as ordered lists and has all of the > operations you mention.
thanks for the pointers! > > Brief look into haskell-prime-report/list.html reveals nothing. > > > > Could we please have them? > > The trend is to remove things from "standard" libraries and to push > them more to 3rd party libraries hosted on hackage. understood. > > On the wider perspective, is their a way to declare an /ordered/ list on the > > type level (e.g. [1,2,3] would be one, but not [2,3,1])? Non-decreasing lists? > > Cyclical, or of certain length? What are such types called? > > There are a few ways to encode such things. The most direct route is > to use dependent types as Miguel mentioned, but Haskell has no support > for those. See languages like Agda or Coq. Another approach is to > use a type that specifically represents what you want and nothing > else. For example, a list of a set length is just a tuple. It is > easy to make a type that represents cyclic lists. Finally, the most > general method is to use an abstract data type to maintain the > invariant. It is trivial to handle ordered/non-decreasing lists in > this way. One note about the dependent types route is that the > ability to assert arbitrary properties comes with it the > responsibility to prove them later on. So you can make a function > which only accepts ordered lists, but then the users need to pass in a > proof that their lists are ordered when they use such functions and > these proofs can be a significant burden. Presumably a system would be able to prove - to know - by itself that [1..n] is an ordered list, to start with. The idea is to have a way of maintaining - and refining - our knowledge about objects we work on/with. I've also found out about refinement types, but the wikipedia page is _very_ sketchy. Presumably each function definition would automatically produce a part of proof for the values it produces, given the compliance of its inputs to their preconditions. A program built as a chain of such fuctions would automatically have its proof calculated for it. The goal, to illustrate it by way of example, is to be able to compile/simplify the expression ( x = sum $ take n $ cycle $ [1..m] ) into a straightforward math formula with some quotRem call in it. I think this would naturally extend to the constraint programming. All I have is some vague notions for now. :) _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
