Re: [Caml-list] polymorphic recursion with type constraint?

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

From: nakata keiko <keiko@kaba.or.jp>
> 
> Can I make the following function 'subst' well-behave,
> so that it can be used in the contexts where:
> 1) 'p' (the first argument) is assumed of type 'path', and 
>   'env' (the first argument)is assumed of type '(string * tau) list;
> and 
> 2)'p' is assumed of type 'tau', and 
>   'env' is assumed of type '(string * tau) list;
> 
> 
>     type tau = [`Root | `Apply of path * tau |`Var of string]  
>     and  path = [`Root | `Apply of path * tau] 
>     
>     let rec subst p env = 
>     	 match p with 
>     	    `Root -> `Root
>     	  | `Apply (p1, p2) -> `Apply(subst p1 env , subst p2 env)
>     	  | `Var s -> List.assoc s env
> 
> Yet 'subst' is well-typed, 
> 
>     let sub (p : path) (env : (string * tau)) = subst p env
> 
> fails.

To make the problem setting more explicit, you want to use the above
function as both
   tau -> (string * tau) list -> tau
and
   path -> (string * tau) list -> path

Independently of recursion problems, this is impossible because usual
variant typing assumes that all branches in a pattern matching will be
used, so that the typing will at least be
   path -> (string * tau) list -> tau
due to the `Var case.

Maximal sharing of code is obtained by the following program:

let rec subst_path env = function
    `Root -> `Root
  | `Apply (p1, p2) -> `Apply (subst_path env p1, subst_tau env p2)
and subst_tau env = function
    #path as p -> (subst_path env p :> tau)
  | `Var s -> List.assoc s env

Your first program would be typable assuming both "conditional typing
of branches" and polymorphic recursion. The second is available
inderectly, but the first was only implemented in an experimental
version of the compiler.

Jacques Garrigue