[Ur] Code reuse and type constraints

[Adam Chlipala]

On 02/10/2015 04:06 PM, Gabriel Riba wrote:
>
> Since [a] is no more in EqSet, I have to pair the Item structure and the Set
> one when as input to the MkSetOps functor:

The solution is again a standard ML idiom.

signature SET = sig
   type item
   type t
   val empty: t
   val singleton : item -> t
   val insert: item -> t -> t
   val member: item -> t -> bool
   val foldr: b ::: Type -> (item -> b -> b) -> b -> t -> b
end

functor EqSet(Q: sig type item
                      val eq_item: eq item
                  end): SET where type item = Q.item = struct ... end


> (* *** code: *)
>
> functor EqSet(Q: sig con item :: Type
>                       val eq_item: eq item
>                   end): sig
>    con t :: Type
>    val empty: t
>    val singleton : Q.item -> t
>    val insert: Q.item -> t -> t
>    val member: Q.item -> t -> bool
>    val foldr: b ::: Type -> (Q.item -> b -> b) -> b -> t -> b
> end = struct
>    type t = list Q.item
>    val empty: t = []
>    val singleton (x: Q.item): t = x :: []
>    val member (x: Q.item) (li: t)  = List.exists (eq x) li
>    val insert (x: Q.item) (xs : t) =
>                   if member x xs then xs else x :: xs
>    val foldr [b]: (Q.item -> b -> b) -> b -> t -> b = List.foldr
> end