Re: [Caml-list] type var in functor instance?

Re: [Caml-list] type var in functor instance?

[Jean-Christophe Filliatre]

[-- Attachment #1: message body and .signature --]
[-- Type: text/plain, Size: 593 bytes --]


skaller writes:
 > Is it possible instantiate a functor with a module
 > containing a type variable? I have a Set with t = int,
 > and I now need 'a * int.. 

No it is not possible. This is a recurrent question on this
list. Various unsatisfying solutions have been proposed, among which

- to make a copy of Set with an additional type parameter eveywhere (I
  attach such a module below. Beware: this is an old version of Set)

- to make an unfunctorized version of Set that uses Pervasives.compare,
  thus polymorphic

regards,
-- 
Jean-Christophe Filliâtre (http://www.lri.fr/~filliatr)


[-- Attachment #2: pset.mli --]
[-- Type: application/octet-stream, Size: 5775 bytes --]

(***********************************************************************)
(*                                                                     *)
(*                           Objective Caml                            *)
(*                                                                     *)
(*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         *)
(*                                                                     *)
(*  Copyright 1996 Institut National de Recherche en Informatique et   *)
(*  en Automatique.  All rights reserved.  This file is distributed    *)
(*  under the terms of the GNU Library General Public License.         *)
(*                                                                     *)
(***********************************************************************)

(* $Id: pset.mli,v 1.2 2002/02/22 15:54:43 filliatr Exp $ *)

(* Module [Set]: sets over ordered types *)

(* This module implements the set data structure, given a total ordering
   function over the set elements. All operations over sets
   are purely applicative (no side-effects).
   The implementation uses balanced binary trees, and is therefore
   reasonably efficient: insertion and membership take time
   logarithmic in the size of the set, for instance. *)

module type POrderedType =
  sig
    type 'a t
    val compare: 'a t -> 'a t -> int
  end
          (* The input signature of the functor [Set.Make].
             [t] is the type of the set elements.
             [compare] is a total ordering function over the set elements.
             This is a two-argument function [f] such that
             [f e1 e2] is zero if the elements [e1] and [e2] are equal,
             [f e1 e2] is strictly negative if [e1] is smaller than [e2],
             and [f e1 e2] is strictly positive if [e1] is greater than [e2].
             Example: a suitable ordering function is
             the generic structural comparison function [compare]. *)

module type S =
  sig
    type 'a elt
          (* The type of the set elements. *)
    type 'a t
          (* The type of sets. *)
    val empty: 'a t
          (* The empty set. *)
    val is_empty: 'a t -> bool
        (* Test whether a set is empty or not. *)
    val mem: 'a elt -> 'a t -> bool
        (* [mem x s] tests whether [x] belongs to the set [s]. *)
    val add: 'a elt -> 'a t -> 'a t
        (* [add x s] returns a set containing all elements of [s],
           plus [x]. If [x] was already in [s], [s] is returned unchanged. *)
    val singleton: 'a elt -> 'a t
        (* [singleton x] returns the one-element set containing only [x]. *)
    val remove: 'a elt -> 'a t -> 'a t
        (* [remove x s] returns a set containing all elements of [s],
           except [x]. If [x] was not in [s], [s] is returned unchanged. *)
    val union: 'a t -> 'a t -> 'a t
    val inter: 'a t -> 'a t -> 'a t
    val diff: 'a t -> 'a t -> 'a t
        (* Union, intersection and set difference. *)
    val compare: 'a t -> 'a t -> int
        (* Total ordering between sets. Can be used as the ordering function
           for doing sets of sets. *)
    val equal: 'a t -> 'a t -> bool
        (* [equal s1 s2] tests whether the sets [s1] and [s2] are
           equal, that is, contain equal elements. *)
    val subset: 'a t -> 'a t -> bool
        (* [subset s1 s2] tests whether the set [s1] is a subset of
           the set [s2]. *)
    val iter: ('a elt -> unit) -> 'a t -> unit
        (* [iter f s] applies [f] in turn to all elements of [s].
           The order in which the elements of [s] are presented to [f]
           is unspecified. *)
    val fold: ('a elt -> 'b -> 'b) -> 'a t -> 'b -> 'b
        (* [fold f s a] computes [(f xN ... (f x2 (f x1 a))...)],
           where [x1 ... xN] are the elements of [s].
           The order in which elements of [s] are presented to [f] is
           unspecified. *)
    val for_all: ('a elt -> bool) -> 'a t -> bool
        (* [for_all p s] checks if all elements of the set
           satisfy the predicate [p]. *)
    val exists: ('a elt -> bool) -> 'a t -> bool
        (* [exists p s] checks if at least one element of
           the set satisfies the predicate [p]. *)
    val filter: ('a elt -> bool) -> 'a t -> 'a t
        (* [filter p s] returns the set of all elements in [s]
           that satisfy predicate [p]. *)
    val partition: ('a elt -> bool) -> 'a t -> 'a t * 'a t
        (* [partition p s] returns a pair of sets [(s1, s2)], where
           [s1] is the set of all the elements of [s] that satisfy the
           predicate [p], and [s2] is the set of all the elements of
           [s] that do not satisfy [p]. *)
    val cardinal: 'a t -> int
        (* Return the number of elements of a set. *)
    val elements: 'a t -> 'a elt list
        (* Return the list of all elements of the given set.
           The returned list is sorted in increasing order with respect
           to the ordering [Ord.compare], where [Ord] is the argument
           given to [Set.Make]. *)
    val min_elt: 'a t -> 'a elt
        (* Return the smallest element of the given set
           (with respect to the [Ord.compare] ordering), or raise
           [Not_found] if the set is empty. *)
    val max_elt: 'a t -> 'a elt
        (* Same as [min_elt], but returns the largest element of the
           given set. *)
    val choose: 'a t -> 'a elt
        (* Return one element of the given set, or raise [Not_found] if
           the set is empty. Which element is chosen is unspecified,
           but equal elements will be chosen for equal sets. *)
  end

module Make(Ord: POrderedType): (S with type 'a elt = 'a Ord.t)
        (* Functor building an implementation of the set structure
           given a totally ordered type. *)

[-- Attachment #3: pset.ml --]
[-- Type: application/octet-stream, Size: 9950 bytes --]

(***********************************************************************)
(*                                                                     *)
(*                           Objective Caml                            *)
(*                                                                     *)
(*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         *)
(*                                                                     *)
(*  Copyright 1996 Institut National de Recherche en Informatique et   *)
(*  en Automatique.  All rights reserved.  This file is distributed    *)
(*  under the terms of the GNU Library General Public License.         *)
(*                                                                     *)
(***********************************************************************)

(* $Id: pset.ml,v 1.1 2000/07/07 16:13:17 filliatr Exp $ *)

(* Sets over ordered types *)

module type POrderedType =
  sig
    type 'a t
    val compare: 'a t -> 'a t -> int
  end

module type S =
  sig
    type 'a elt
    type 'a t
    val empty: 'a t
    val is_empty: 'a t -> bool
    val mem: 'a elt -> 'a t -> bool
    val add: 'a elt -> 'a t -> 'a t
    val singleton: 'a elt -> 'a t
    val remove: 'a elt -> 'a t -> 'a t
    val union: 'a t -> 'a t -> 'a t
    val inter: 'a t -> 'a t -> 'a t
    val diff: 'a t -> 'a t -> 'a t
    val compare: 'a t -> 'a t -> int
    val equal: 'a t -> 'a t -> bool
    val subset: 'a t -> 'a t -> bool
    val iter: ('a elt -> unit) -> 'a t -> unit
    val fold: ('a elt -> 'b -> 'b) -> 'a t -> 'b -> 'b
    val for_all: ('a elt -> bool) -> 'a t -> bool
    val exists: ('a elt -> bool) -> 'a t -> bool
    val filter: ('a elt -> bool) -> 'a t -> 'a t
    val partition: ('a elt -> bool) -> 'a t -> 'a t * 'a t
    val cardinal: 'a t -> int
    val elements: 'a t -> 'a elt list
    val min_elt: 'a t -> 'a elt
    val max_elt: 'a t -> 'a elt
    val choose: 'a t -> 'a elt
  end

module Make(Ord: POrderedType) =
  struct
    type 'a elt = 'a Ord.t
    type 'a t = Empty | Node of 'a t * 'a elt * 'a t * int

    (* Sets are represented by balanced binary trees (the heights of the
       children differ by at most 2 *)

    let height = function
        Empty -> 0
      | Node(_, _, _, h) -> h

    (* Creates a new node with left son l, value x and right son r.
       l and r must be balanced and | height l - height r | <= 2.
       Inline expansion of height for better speed. *)

    let create l x r =
      let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in
      let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in
      Node(l, x, r, (if hl >= hr then hl + 1 else hr + 1))

    (* Same as create, but performs one step of rebalancing if necessary.
       Assumes l and r balanced.
       Inline expansion of create for better speed in the most frequent case
       where no rebalancing is required. *)

    let bal l x r =
      let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in
      let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in
      if hl > hr + 2 then begin
        match l with
          Empty -> invalid_arg "Set.bal"
        | Node(ll, lv, lr, _) ->
            if height ll >= height lr then
              create ll lv (create lr x r)
            else begin
              match lr with
                Empty -> invalid_arg "Set.bal"
              | Node(lrl, lrv, lrr, _)->
                  create (create ll lv lrl) lrv (create lrr x r)
            end
      end else if hr > hl + 2 then begin
        match r with
          Empty -> invalid_arg "Set.bal"
        | Node(rl, rv, rr, _) ->
            if height rr >= height rl then
              create (create l x rl) rv rr
            else begin
              match rl with
                Empty -> invalid_arg "Set.bal"
              | Node(rll, rlv, rlr, _) ->
                  create (create l x rll) rlv (create rlr rv rr)
            end
      end else
        Node(l, x, r, (if hl >= hr then hl + 1 else hr + 1))

    (* Same as bal, but repeat rebalancing until the final result
       is balanced. *)

    let rec join l x r =
      match bal l x r with
        Empty -> invalid_arg "Set.join"
      | Node(l', x', r', _) as t' ->
          let d = height l' - height r' in
          if d < -2 or d > 2 then join l' x' r' else t'

    (* Merge two trees l and r into one.
       All elements of l must precede the elements of r.
       Assumes | height l - height r | <= 2. *)

    let rec merge t1 t2 =
      match (t1, t2) with
        (Empty, t) -> t
      | (t, Empty) -> t
      | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) ->
          bal l1 v1 (bal (merge r1 l2) v2 r2)

    (* Same as merge, but does not assume anything about l and r. *)

    let rec concat t1 t2 =
      match (t1, t2) with
        (Empty, t) -> t
      | (t, Empty) -> t
      | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) ->
          join l1 v1 (join (concat r1 l2) v2 r2)

    (* Splitting *)

    let rec split x = function
        Empty ->
          (Empty, None, Empty)
      | Node(l, v, r, _) ->
          let c = Ord.compare x v in
          if c = 0 then (l, Some v, r)
          else if c < 0 then
            let (ll, vl, rl) = split x l in (ll, vl, join rl v r)
          else
            let (lr, vr, rr) = split x r in (join l v lr, vr, rr)

    (* Implementation of the set operations *)

    let empty = Empty

    let is_empty = function Empty -> true | _ -> false

    let rec mem x = function
        Empty -> false
      | Node(l, v, r, _) ->
          let c = Ord.compare x v in
          c = 0 || mem x (if c < 0 then l else r)

    let rec add x = function
        Empty -> Node(Empty, x, Empty, 1)
      | Node(l, v, r, _) as t ->
          let c = Ord.compare x v in
          if c = 0 then t else
          if c < 0 then bal (add x l) v r else bal l v (add x r)

    let singleton x = Node(Empty, x, Empty, 1)

    let rec remove x = function
        Empty -> Empty
      | Node(l, v, r, _) ->
          let c = Ord.compare x v in
          if c = 0 then merge l r else
          if c < 0 then bal (remove x l) v r else bal l v (remove x r)

    let rec union s1 s2 =
      match (s1, s2) with
        (Empty, t2) -> t2
      | (t1, Empty) -> t1
      | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) ->
          if h1 >= h2 then
            if h2 = 1 then add v2 s1 else begin
              let (l2, _, r2) = split v1 s2 in
              join (union l1 l2) v1 (union r1 r2)
            end
          else
            if h1 = 1 then add v1 s2 else begin
              let (l1, _, r1) = split v2 s1 in
              join (union l1 l2) v2 (union r1 r2)
            end

    let rec inter s1 s2 =
      match (s1, s2) with
        (Empty, t2) -> Empty
      | (t1, Empty) -> Empty
      | (Node(l1, v1, r1, _), t2) ->
          match split v1 t2 with
            (l2, None, r2) ->
              concat (inter l1 l2) (inter r1 r2)
          | (l2, Some _, r2) ->
              join (inter l1 l2) v1 (inter r1 r2)

    let rec diff s1 s2 =
      match (s1, s2) with
        (Empty, t2) -> Empty
      | (t1, Empty) -> t1
      | (Node(l1, v1, r1, _), t2) ->
          match split v1 t2 with
            (l2, None, r2) ->
              join (diff l1 l2) v1 (diff r1 r2)
          | (l2, Some _, r2) ->
              concat (diff l1 l2) (diff r1 r2)

    let rec compare_aux l1 l2 =
        match (l1, l2) with
        ([], []) -> 0
      | ([], _)  -> -1
      | (_, []) -> 1
      | (Empty :: t1, Empty :: t2) ->
          compare_aux t1 t2
      | (Node(Empty, v1, r1, _) :: t1, Node(Empty, v2, r2, _) :: t2) ->
          let c = Ord.compare v1 v2 in
          if c <> 0 then c else compare_aux (r1::t1) (r2::t2)
      | (Node(l1, v1, r1, _) :: t1, t2) ->
          compare_aux (l1 :: Node(Empty, v1, r1, 0) :: t1) t2
      | (t1, Node(l2, v2, r2, _) :: t2) ->
          compare_aux t1 (l2 :: Node(Empty, v2, r2, 0) :: t2)

    let compare s1 s2 =
      compare_aux [s1] [s2]

    let equal s1 s2 =
      compare s1 s2 = 0

    let rec subset s1 s2 =
      match (s1, s2) with
        Empty, _ ->
          true
      | _, Empty ->
          false
      | Node (l1, v1, r1, _), (Node (l2, v2, r2, _) as t2) ->
          let c = Ord.compare v1 v2 in
          if c = 0 then
            subset l1 l2 && subset r1 r2
          else if c < 0 then
            subset (Node (l1, v1, Empty, 0)) l2 && subset r1 t2
          else
            subset (Node (Empty, v1, r1, 0)) r2 && subset l1 t2

    let rec iter f = function
        Empty -> ()
      | Node(l, v, r, _) -> iter f l; f v; iter f r

    let rec fold f s accu =
      match s with
        Empty -> accu
      | Node(l, v, r, _) -> fold f l (f v (fold f r accu))

    let rec for_all p = function
        Empty -> true
      | Node(l, v, r, _) -> p v && for_all p l && for_all p r

    let rec exists p = function
        Empty -> false
      | Node(l, v, r, _) -> p v || exists p l || exists p r

    let filter p s =
      let rec filt accu = function
        | Empty -> accu
        | Node(l, v, r, _) ->
            filt (filt (if p v then add v accu else accu) l) r in
      filt Empty s

    let partition p s =
      let rec part (t, f as accu) = function
        | Empty -> accu
        | Node(l, v, r, _) ->
            part (part (if p v then (add v t, f) else (t, add v f)) l) r in
      part (Empty, Empty) s

    let rec cardinal = function
        Empty -> 0
      | Node(l, v, r, _) -> cardinal l + 1 + cardinal r

    let rec elements_aux accu = function
        Empty -> accu
      | Node(l, v, r, _) -> elements_aux (v :: elements_aux accu r) l

    let elements s =
      elements_aux [] s

    let rec min_elt = function
        Empty -> raise Not_found
      | Node(Empty, v, r, _) -> v
      | Node(l, v, r, _) -> min_elt l

    let rec max_elt = function
        Empty -> raise Not_found
      | Node(l, v, Empty, _) -> v
      | Node(l, v, r, _) -> max_elt r

    let choose = min_elt

  end

Re: [Caml-list] type var in functor instance?

[skaller]

On Mon, 2004-09-20 at 21:58, Jean-Christophe Filliatre wrote:
> skaller writes:
>  > Is it possible instantiate a functor with a module
>  > containing a type variable? I have a Set with t = int,
>  > and I now need 'a * int.. 

> Various unsatisfying solutions have been proposed, among which
> 
> - to make a copy of Set with an additional type parameter eveywhere (I
>   attach such a module below. Beware: this is an old version of Set)

Hmmm. I see. I think I understand why this is needed.
Dependent typing problem? Set depends on element...

> - to make an unfunctorized version of Set that uses Pervasives.compare,
>   thus polymorphic

This is already in the standard distro for Hashtbl.
Why not for Set and Map as well? Why is this
unsatisfactory?

I actually use heaps of Hashtbl of polymorphic kind
and am ready to switch some over to an functor instance
with key type int -- most of my tables use int keys
and I hope to gain some performance and reasoning ability.

The duplicate interface has let me experiment rapid
prototyping style, then lock down the typing a bit,
leaving the raw function names and semantics the same.

I think that's nice -- one reason I use Hashtbl
even when Set or Map would be better.

-- 
John Skaller, mailto:skaller@users.sf.net
voice: 061-2-9660-0850, 
snail: PO BOX 401 Glebe NSW 2037 Australia
Checkout the Felix programming language http://felix.sf.net



-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] type var in functor instance?

[Daniel Bünzli]

Hello,

Accidentally I'm running into the same problem. I'd like to have a 
polymorphic Hashtbl that uses physical equality. Using Hashtbl.Make is 
not possible since the type t of the input signature HashedType has no 
variable.

More precisely I would like to have a key with the following type

type 'a 'b key = 'a option * 'b option

and the following equal function,

let equal k k' = match k, k' with
| (Some x, y), (Some x', y') -> if x == x' then y = y' else false
| _, _ -> k = k'

which tests for physical equality when the first component of the key 
is "Some" in both keys.

Any hints besides those already suggested ?

Daniel

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Core library (was: type var in functor instance?)

[Jon Harrop]

On Monday 20 September 2004 16:43, skaller wrote:
> > - to make an unfunctorized version of Set that uses Pervasives.compare,
> >   thus polymorphic
>
> This is already in the standard distro for Hashtbl.
> Why not for Set and Map as well? Why is this
> unsatisfactory?

You mean Hashtbl uses a polymorphic hash?

I think it would be productive to factor the tree out of set and map.

What if someone released backwards-compatible replacement modules for List, 
Array, Set, Map etc. which implemented this stuff? Then package maintainers 
could replace them if they liked the alternative implementations and coders 
could assume their existence. Maybe.

> I actually use heaps of Hashtbl of polymorphic kind
> and am ready to switch some over to an functor instance
> with key type int -- most of my tables use int keys
> and I hope to gain some performance and reasoning ability.

IMHO, hash tables are a bit less safe than sets and maps because hash tables 
make it easier to apply a structure-based polymorphic function incorrectly, 
e.g. to many abstract types, when a semantically meaningful (e.g. comparison) 
function should be used. For example, I don't think a hash table of sets 
would be very useful...

This strikes me as an important way to screw up ML programs and, consequently, 
it would be nice to address this. I've been trying to think of a solution but 
all I've come up with is: you could enforce the use of an appropriate 
comparison by making everything an object with its own compare method. But 
then you're going back to dynamic typing. Perhaps phantom types could do 
it...

Cheers,
Jon.

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners