
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 dataordlist on hackage
> (http://hackage.haskell.org/packages/archive/dataordlist/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 haskellprimereport/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])? Nondecreasing
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/nondecreasing 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. :)
_______________________________________________
HaskellCafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskellcafe

