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

[Adam Chlipala]

Marc Weber wrote:
> 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 would expect that the compiler error messages do a good job of 
explaining the problem here.  In the definitions of [Next] and [Prev], 
you are treating the value [a] as an [int] when it is really described 
by the type parameter [a].

> 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?
>    

Unlike in Haskell, you can provide multiple type class "constructors," 
based on different sets of provided "methods," with any means of 
calculating the core type class representation that you like.  That is, 
you could provide other differently-typed functions along the lines of 
[mkEnum].