[Ur] urweb-library playground - and question about how to complete implemention of "enum" like class

[Marc Weber]

Excerpts from Adam Chlipala's message of Wed Dec 08 23:17:34 +0100 2010:
> There's already a non-trivial standard library in the compiler 
> distribution.  I'm also planning to take that "meta.tgz" tarball I 
> linked to and turn it into a supplementary standard library specific to 
> metaprogramming (and yes, I'll add a public Mercurial repo Real Soon Now).

You're right, That's why I changed the meaning. 
https://github.com/MarcWeber/urweb-library

Also pay attention to its description:
http://impredicative.com/wiki/index.php/Libraries_and_FFI_bindings
quoting myself: "
  code which could be moved into the core library later.
  http://github.com/MarcWeber/urweb-library Contact MarcWeber using the
  github page to get push / commit access I would have liked to create a
  repository which is easier to get access to (eg by registering at github
  only) But I didn't find a way. I'm fine with creating a more neutral
  name such as github.com/urweb later if several users start contributing.
  (I also tried gitorious - but got yet another "I'm sorry" error .. )
"

Hope that's fine to everyone for now. I'm willing to change everything -
but for now I use what I'm used to - which works best for me.
So join this effort and let's create some useful code everybody can use.



I also added a "test" branch. It adds the functions "next" and "prev"
to enum - howver it doesn't compile. What am I doing wrong?


== .urs file ==
  class enum

  val mkEnum  : a ::: Type -> {ToInt   : a -> int,
                               FromInt : int -> a } -> enum a


== .ur file ==

    class enum a = { ToInt   : a -> int,
                     FromInt : int -> a,
                      Next    : a -> a,
                      Prev    : a -> a
                    }

    val mkEnum [a] (x : { ToInt   : a -> int,
                          FromInt : int -> a }) =
                                { ToInt   = fn a => x.ToInt a
                                , FromInt = fn a => x.FromInt a
                                , Next    = fn a => x.ToInt (x.FromInt (a + 1))
                                , Prev    = fn a => x.ToInt (x.FromInt (a - 1))
                                }


I try to derive next, prev using FromInt, ToInt.
There may exist optimized versions.
Is it even worth allowing passing those optimized versions - if so how
would this be done?

In Haskell this all is only:

class MyEnm a where
  toInt : a -> Int
  fromInt : Int -> a

  -- note how next and prev is using toInt and fromInt which will be
  -- defined in instances below
  next : a -> a
  next = fromInt . (+1) . toInt
  prev : a -> a
  prev = fromInt . (-1) . toInt

instance MyEnm  Int where
  toInt = id
  fromInt = id
  -- prev, next already defined above. But optimized versions could be
  -- specified here


If I look at the amount of code I have to write Haskell wins.

Marc Weber