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]) 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
> 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
> > 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