[Haskell-cafe] Re: Why no merge and listDiff?

[Will Ness]

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. :)