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