Derek Elkins
On Sun, Jan 17, 2010 at 2:22 PM, Will Ness
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.
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
understood. 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. :)