On Mon, Apr 20, 2009 at 09:44:54PM -0400, Eliot Handelman wrote:
> Consider this:
> 
> type 'a x = { x_v : 'a }
> 
> and 'a y = { y_x : int kind;
>          y_arr : 'a array
>         }
> and 'a kind =
>     X of 'a x
>   | Y of 'a y
>     
> 
> I'd like to write a function _getter_ that's polymorphic over kind. This
> doesn't work, getting int kind -> int:
> 
> let rec getter = function
>     X x -> x.x_v
>   | Y y -> y.y_arr.(getter y.y_x)
>
> which seems surprising to me since getter y.y_x is an intermediate
> value that's never returned. Is this just a limitation of the type system or
> does this result make sense?

The above function requires polymorphic recursion, which OCaml doesn't support
directly. There are several ways to encode it, though, one involving recursive
modules and another rank-2 polymorphism:

# module rec M : sig val getter : 'a kind -> 'a end = struct
  let getter = function
    X x -> x.x_v
  | Y y -> y.y_arr.(M.getter y.y_x)
  end;;
module rec M : sig val getter : 'a kind -> 'a end
# M.getter;;
- : 'a kind -> 'a = <fun>

# type get = { get : 'a. 'a kind -> 'a };;
type get = { get : 'a. 'a kind -> 'a; }
# let rec get = { get = function X x -> x.x_v | Y y -> y.y_arr.(get.get y.y_x) };;
val get : get = {get = <fun>}
# let getter = get.get;;
val getter : 'a kind -> 'a = <fun>

-- 
Mauricio Fernandez  -   http://eigenclass.org