[Ur] Code reuse and type constraints

Adam Chlipala adamc at csail.mit.edu
Tue Feb 10 10:16:36 EST 2015


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.

P.S.: You can omit the line for [eq_item] at the very end, and the 
compiler will infer it, just as you'd expect with type classes!

On 02/10/2015 07:37 AM, Gabriel Riba wrote:
> 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)



More information about the Ur mailing list