Variable-argument functions

Thu, 2008/03/20 - 2:41pm — sweeks

Here's another puzzle:

Is it possible in OCaml to define a variable-argument function? For example, can one define a function f and values a and z such that the following assertions hold:

assert (f z = 0);
assert (f a z = 1);
assert (f a a z = 2);
assert (f a a a z = 3);
...

Once you've got that, how about generalizing it to a variable-argument sum, i.e. define f, a, and z such that:

assert (f (a i1) (a i2) ... (a ik) z = i1 + i2 + ... + ik);

Or, if you want to eliminate the parens, define an f, a, and z such that:

assert (f a i1 a i2 ... a ik z = i1 + i2 + ... + ik);

Comments

Thu, 2008/03/20 - 10:26pm — jonathan

Continuation Passing Style

This is very Similar to a typesafe printf solution I've seen.

let a x = 
  fun f -> f (x + 1);;
 
let z x = x;;
 
let f g = g 0;;
For the generalized version, a is instead implemented as:

let a x = 
  fun y f -> f (x + y);;

Continuations are crazy powerful!

Thu, 2008/03/20 - 10:30pm — milanst

nice puzzle

For the first one: 

let z sum = sum
 
let a sum g =
  g (sum + 1)
 
let f g =
  g 0

For the second and third one only a changes: 

let a i sum g =
  g (i + sum)

This works with or without parenthesis.

Fri, 2008/03/21 - 1:30am — n8gray

Good clean fun

I'm enjoying the puzzles! I'm no stranger to Church numerals so this wasn't a major challenge, but no matter how many times I code CN's it always feels like magic when they work. Also, version 3 is a neat trick that I wasn't expecting. :-)

Fri, 2008/03/21 - 9:10am — mshinwell

First part

My solution is the same as the one at the bottom of this page, but here is some intuition. The way I looked at this was to think about "f", "f a" and "(f a) a" as being values Zero, One and Two such that Zero z = 0, One z = 1, Two z = 2, etc. Say that Zero, One and Two all have some type Num; the idea is that each represents the corresponding integer, applying "a" to a Num produces the representation of the next integer, and applying "z" to a Num produces the actual integer to which it corresponds.

One way of representing integers using functions is to use values of type 'a -> ('a -> 'a) -> 'a (the intuition being that given such a value, you supply a base case and an iterator, and the iterator is iterated correspondingly many times starting from the base). That doesn't quite work here; instead an alternative representation seems to be needed, where the representation actually holds the integer itself.

Letting the type Num be (int -> 'a) -> 'a, we can define f (aka Zero) to be 

let f = fun g -> g 0
Such a representation can be "quizzed" by providing a function that accepts the value stored within, does something with it (possibly changing its type), and returns it. In the first case above, "f z", we just want the value unchanged at type int, so define 
let z = fun x -> x
Now all we need is a value "a" such that applying "a" to a value of type Num produces another value of type Num corresponding to the next integer. To do this, we can extract the encapsulated integer from the value of type Num, increment it, and form another value of type Num. This is done by defining: 
let a x = fun g -> g (x + 1)
of type int -> Num, and then applying it to values of type Num as required. Having then done the incrementing ("(f a) a" perhaps) starting from Zero (aka "f"), you then apply "z" to get back the value of type int. Cunning.

Tue, 2008/03/25 - 8:15am — sweeks

Thanks for trying out the puzzle.

It seems we all have the same solution :-). One thing I hadn't noticed until Milan pointed it out was the the solutions to puzzles two and three are the same. It only works becaus the operation is commutative. For a case where it won't work, consider defining f, a, z such that:

assert (f z = []);
assert (f a x1 z = [x1]);
assert (f a x1 a x2 z = [x1; x2]);
assert (f a x1 a x2 a x3 z = [x1; x2; x3]);

The solutions with and without parentheses require different a's.

As for the original problem, the most surprising part to me is that the types work out. Here's some code that helps me understand why.

module type S = sig
  type 'a t
 
  val f : 'a t -> 'a
  val a : ('a t -> 'a) t
  val z : int t
end
 
module F (M : S) = struct
  open M
 
  type 'a f = 'a t -> 'a
  type 'a a = ('a t -> 'a) t
 
  type u0 = int
  type a0 = u0 t
  type u1 = a0 -> u0
  type a1 = u0 a
  type u2 = a1 -> u1
  type a2 = u1 a
  type u3 = a2 -> u2
  type a3 = u2 a
 
  let () =
    let z : a0 = z in
    let a1 : a1 = a in
    let a2 : a2 = a in
    let a3 : a3 = a in
    let ((f0 : u0 f) : a0 -> int) = f in
    let ((f1 : u1 f) : a1 -> a0 -> int) = f in
    let ((f2 : u2 f) : a2 -> a1 -> a0 -> int) = f in
    let ((f3 : u3 f) : a3 -> a2 -> a1 -> a0 -> int) = f in
    assert (f0 z = 0);
    assert (f1 a1 z = 1);
    assert (f2 a2 a1 z = 2);
    assert (f3 a3 a2 a1 z = 3);
  ;;
end
 
module M : S = struct
  type 'a t = int -> 'a
 
  let f g = g 0
  let a i g = g (i + 1)
  let z i = i
end
 
module Z = F (M)

Syndicate content