[Ur] Code reuse and type constraints

[Gabriel Riba]

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


> 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.)

I have worked it out (in haskell: constraint to the instance context (ML
input signature)) :

functor EqSet(Q: sig con item :: Type
                     val eq_item: eq item
                 end)
 
> 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.
> 

Is this about using [a] in the right hand side?. Thanks for the hint.

  type t a = list Q.item

(* --- new code: *)

functor EqSet(Q: sig con item :: Type
                     val eq_item: eq item
                 end): sig
  con t :: Type -> Type
  con a :: Type
  val empty: t a
  val singleton : a -> 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
  type a = Q.item
  type t a = list Q.item
  val empty: t a = []
  val singleton (x: a): t a = x :: []
  val member (x: a) (li: t a)  = List.exists (eq x) li
  val insert (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 item = int
                                  val eq_item = eq_int
                           end)

Thanks, I will use the model in my too Haskell stylish library.