[Ur] Code reuse and type constraints

[Adam Chlipala]

I wonder if the issue is that you are most familiar with Haskell and are 
trying to fit Haskell idioms incrementally into the style of ML module 
systems?

The idiomatic ML way would be to extend [EqSet]'s input signature with a 
fixed [eq item] instance, so that there is no need for [eq] 
quantification in any function type, anywhere in your example. (In ML, 
it would usually be an explicit equality function, because of lack of 
type classes, but an [eq] instance is an appropriate Ur analogue.)

A related problem in your code below is that the signature of [EqSet] 
hides the fact that [a] in the output module equals [item] in the input 
module.  Any introduction to modules in OCaml or Standard ML will 
explain the idioms for avoiding that problem, and they generalize well 
to Ur.

On 02/09/2015 01:14 PM, Gabriel Riba wrote:
> I would like to reuse code between a SortedSet and an EqSet, for functions
> that have neither ord nor eq constraint at the element.
>
> When I apply the unconstrained ops functor to the base one I get:
>
> Have:  val insert : (eq a) -> a -> (t a) -> t a
> Need:  val insert : a -> (t a) -> t a
>
> Is there a way to factor out the constraint from the method definitions,
> e.g. as a type lower bound
>
> Here is the code:
>
> (* --- *)
>
> (* unconstrained set ops *)
>
> functor MkSetOps (Set: sig
>    con t :: Type -> Type
>    con a :: Type
>    val empty: t a
>    val insert: a -> t a -> t a
>    val member: a -> t a -> bool
>    val foldr: b ::: Type -> (a -> b -> b) -> b -> t a -> b
> end) = struct
>          open Set
>
>          fun filterFoldr [b] (prop: a -> bool) (myop: a -> b -> b)
>                              (acc: b) : (t a -> b) =
>                  let fun myop' (x: a) (acc': b) =
>                          if prop x
>                                  then myop x acc'
>                                  else acc'
>                  in foldr myop' acc
>                  end
>
>          fun union (s1: t a) (s2: t a): t a = foldr insert s2 s1
>
>          fun intersect (s1: t a) (s2: t a): t a =
>                  let
>                          val memberOf = HFunction.flip member
>                  in
>                          filterFoldr (memberOf s1) insert empty s2
>                  end
> end
>
> (* base ops *)
>
> functor EqSet(Q: sig con item :: Type end): sig
>    con t :: Type -> Type
>    con a :: Type
>    val empty: t a
>    val insert: eq a -> a -> t a -> t a
>    val member: eq a -> a -> t a -> bool
>    val foldr: b ::: Type -> (a -> b -> b) -> b -> t a -> b
> end = struct
>    type a = Q.item
>    type t a = list a
>    val empty: t a = []
>    val member (_: eq a) (x: a) (li: t a)  = List.exists (eq x) li
>    val insert (_: eq a) (x: a) (xs : t a) =
>                   if member x xs then xs else x :: xs
>    val foldr [b] (myop: a -> b -> b) (z: b) (li: t a) = List.foldr myop z li
> end
>
>
> structure IntEqSet = EqSet(struct type elem = int end)
> structure IntEqSetOps = MkSetOps( IntEqSet)