pairs


Subject: pairs
From: Philippe Meunier (meunier@ccs.neu.edu)
Date: Mon Feb 11 2002 - 23:41:38 EST


Here we go. The first untyped version was easy. Then adding the pair
type took some time, just to get the type right (the pair type itself
was not strictly necessary, I just wanted to add it to have better
types printed - only the u type is relevant to what we were discussing
this afternoon (i.e. having a sum type and projecting), and that one
was fine to add). Then I played a little with types, and reached the
conclusion that being able to abstract over type constructors would be
nice. Then I tried to add the type constructors directly inside the
pairs, and spent a looong time just trying to understand what was
wrong with it...

Caveat: the indentation might be funny, since I don't use the default
indentation settings in emacs...

Philippe

(************************************************************)
(* polymorphic version *)
(* 'a -> 'b -> ('a -> 'b -> 'c) -> 'c *)
let make_pair =
  fun x y ->
    (fun f ->
      f x y);;

(* (('a -> 'b -> 'a) -> 'c) -> 'c *)
let left = fun p -> p (fun x y -> x);;

(* (('a -> 'b -> 'b) -> 'c) -> 'c *)
let right = fun p -> p (fun x y -> y);;

(* (int -> string -> '_a) -> '_a *)
make_pair 1 "a";;

(* int *)
left(make_pair 1 "a");;

(* string *)
right(make_pair 1 "a");;

(* (bool -> int -> '_a) -> '_a *)
make_pair true 2;;

(************************************************************)
(* Now for the typed version, we add a common return type for the left
         and right projectors, since it really is the only one that causes
         problems when we add types *)
type ('s, 't) u =
                S of 's
        | T of 't;;

(* let's add a pair type, to get much more readable types too *)
type ('s, 't) pair =
                Pair of (('s -> 't -> ('s, 't) u) -> ('s, 't) u);;

(* 'a -> 'b -> ('a, 'b) pair *)
let make_pair =
        fun x y ->
                Pair
                        (fun f ->
                                f x y);;

(* ('a, 'b) pair -> 'a *)
(* note: the actual projector (fun x y -> S x) has to wrap its result
         with S, so that the type of the projector matches the
         parameter type ('s -> 't -> ('s, 't) u) defined for p. Once the
         wrapping is done, the result of applying p, which has the
         type (('s, 't) u), can be immediately unwrapped using the
         outermost match. We can ignore the warning from the type checker
         about the outer match not being exhaustive, since we know that the
         result of the projection is always an S. *)
let left =
        fun p_p ->
                match
                        match p_p with
                                Pair p ->
                                        p (fun x y -> S x)
                with
                        S x -> x;;

(* ('a, 'b) pair -> 'b *)
let right =
  fun p_p ->
                match
                        match p_p with
                                Pair p ->
                                        p (fun x y -> T y)
                with
                        T y -> y;;

(* (int, string) pair *)
make_pair 1 "a";;

(* int *)
left(make_pair 1 "a");;

(* string *)
right(make_pair 1 "a");;

(* (bool, int) pair *)
make_pair true 2;;

(************************************************************)
(* we can now actually abstract, and select using an index *)
(* int -> ('a, 'b) pair -> ('a, 'b) u *)
let select =
  fun i ->
    fun p_p ->
      match p_p with
        Pair p ->
          p (fun x y ->
                                                match i with
                                                        1 -> S x
                                                | 2 -> T y);;

(* ('a, 'b) pair -> 'a *)
let left =
  fun p_p ->
    match (select 1) p_p with
      S x -> x;;
 
(* ('a, 'b) pair -> 'b *)
let right =
  fun p_p ->
    match (select 2) p_p with
      T y -> y;;

(* (int, string) pair *)
make_pair 1 "a";;

(* int *)
left(make_pair 1 "a");;

(* string *)
right(make_pair 1 "a");;

(* (bool, int) pair *)
make_pair true 2;;

(************************************************************)
(* now let's replace the index with something about the type, instead
         of using those dirty numbers 1 and 2 - i.e. let's try to do some
   kind of poor man's abstraction over types *)
(* (unit, unit) u -> ('a, 'b) pair -> ('a, 'b) u *)
let select =
        fun i ->
                fun p_p ->
                        match p_p with
                                Pair p ->
                                        p (fun x y ->
                                                match i with
                                                        S () -> S x
                                                | T () -> T y);;

(* ('a, 'b) pair -> 'a *)
let left =
        fun p_p ->
                match (select (S ())) p_p with
                        S x -> x;;

(* ('a, 'b) pair -> 'b *)
let right =
        fun p_p ->
                match (select (T ())) p_p with
                        T y -> y;;

(* (int, string) pair *)
make_pair 1 "a";;

(* int *)
left(make_pair 1 "a");;

(* string *)
right(make_pair 1 "a");;

(* (bool, int) pair *)
make_pair true 2;;

(* too bad we can't abstract over types now, so we could do something
         like:

let meta_select =
        fun U ->
                fun p_p ->
                        match (select (U ())) p_p with
                                U x -> x;;

and have

let left = meta_select S;;
let right = meta_select T;;

Maybe there's a way to do it in ocaml, but type constructors don't
seem to be first class in ocaml anyway...

*)

(************************************************************)
(* we can also put the S and T types when creating the pair, although
         that's not really necessary *)

(* this hasn't changed *)
type ('s, 't) u =
    S of 's
  | T of 't;;

(* this becomes painful. Note that we can't keep the same type for
         pairs as before, becomes ocaml has then no clue what x and y might
         be when we define select below, so it cannot verify that the x and
         y we return inside select have indeed the type u. So we have to
         explicitely say that the two parameters of the function given to p
         have the type (('s, 't) u), so there are no type problems when we
         directly return these parameters as the result of the projections.
         It took me a while to figure out which type I had to change, why,
         and how... *)
type ('s, 't) pair =
                Pair of ((('s, 't) u -> ('s, 't) u -> ('s, 't) u) -> ('s, 't) u);;

(* 'a -> 'b -> ('a, 'b) pair *)
let make_pair =
        fun x y ->
                Pair
                        (fun f ->
                                f (S x) (T y));;

(* (unit, unit) u -> ('a, 'b) pair -> ('a, 'b) u *)
(* this definition fails if we don't restrict the types of x and y by
         modifying the type for pairs:
         "This expression has type 'a but is here used with type ('a, 'a) u"
         with the whole innermost match being underlined... *)
let select =
  fun i ->
    fun p_p ->
      match p_p with
        Pair p ->
          p (fun x y ->
            match i with
              S () -> x
            | T () -> y);;

(* ('a, 'b) pair -> 'a *)
let left =
  fun p_p ->
    match (select (S ())) p_p with
      S x -> x;;

(* ('a, 'b) pair -> 'b *)
let right =
  fun p_p ->
    match (select (T ())) p_p with
      T y -> y;;

(* (int, string) pair *)
make_pair 1 "a";;

(* int *)
left(make_pair 1 "a");;

(* string *)
right(make_pair 1 "a");;

(* (bool, int) pair *)
make_pair true 2;;



This archive was generated by hypermail 2b28 : Mon Feb 11 2002 - 23:41:40 EST