polymorphic recursion with type constraint?

nakata keiko
 Jacques Garrigue
[
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:  20050207 (04:33) 
From:  Jacques Garrigue <garrigue@m...> 
Subject:  Re: [Camllist] polymorphic recursion with type constraint? 
From: nakata keiko <keiko@kaba.or.jp> > > 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. 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