[Ur] Code reuse and type constraints

[Gabriel Riba]

Adam Chlipala <adamc <at> csail.mit.edu> writes:

> 
> This code is looking better.  However, [EqSet] retains the same problem: 
> its output signature hides the equality [a = Q.item].  You really want 
> the output signature to contain just a [type t] with no [a].  Then just 
> use [Q.item] in place of [a] and [t] in place of [t a], everywhere in 
> the signature.

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:

(* *** 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

(* *** *)

functor MkSetOps (Q:sig
           structure It: sig
               con item :: Type
           end
           structure Set: sig
               con t :: Type
               val empty: t
               val insert: It.item -> t -> t
               val member: It.item -> t -> bool
               val foldr: b ::: Type -> (It.item -> b -> b) -> b -> t -> b
           end
end) = struct
        open Q.It
        open Q.Set

        fun filterFoldr [b] (prop: item -> bool) (myop: item -> b -> b)
                            (z: b) : (t -> b) =
                let fun myop' (x: item) (acc': b) =
                        if prop x
                                then myop x acc'
                                else acc'
                in foldr myop' z
                end

        fun union (s1: t) (s2: t): t = foldr insert s2 s1  

        fun intersect (s1: t) (s2: t): t =
                let
                        val memberOf = HFunction.flip member
                in
                        filterFoldr (memberOf s1) insert empty s2
                end
end

(* functor instances *)

structure IntItem = struct
                      type item = int
                      val eq_item = eq_int
                  end

structure IntEqSet = EqSet( IntItem)

structure IntEqSetOps = MkSetOps (struct
                                  structure It = IntItem
                                  structure Set = IntEqSet
                                  end)