**Subject: **pairs

**From: **Philippe Meunier (*meunier@ccs.neu.edu*)

**Date: **Mon Feb 11 2002 - 23:41:38 EST

**Reply****Next message:**Matthias Felleisen: "presentation"**Previous message:**Matthias Felleisen: "tomorrow"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

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;;

**Next message:**Matthias Felleisen: "presentation"**Previous message:**Matthias Felleisen: "tomorrow"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

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