polymorphic recursion with type constraint?
 nakata keiko
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  nakata keiko <keiko@k...> 
Subject:  polymorphic recursion with type constraint? 
Hello. Can I make the following function 'subst' wellbehave, 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 welltyped, 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 welltyped. 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.