polymorphic recursion with type constraint?

polymorphic recursion with type constraint?

[nakata keiko]

Hello.

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.


At first I tried to make 'subst' explicitly typed, but I could not.
'subst' would have type 'a -> (string * tau) list -> 'a,
where the type variable 'a is only instantiated to either 'tau' or 'path'.
Then, the second clause of match
	| `Apply (p1, p2) -> `Apply(subst p1 env , subst p2 env)
would be well-typed.
It seems that I need polymorphic recursion with type constraint....

Or such encoding is inherently wrong, 
and should I define 2 mutually recursive functions?


 
Best regards,
Keiko.

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

[Jacques Garrigue]

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