This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

polymorphic recursion with type constraint?
• nakata keiko
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2005-02-07 (03:17) From: nakata keiko Subject: polymorphic recursion with type constraint?
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.