* Type indexed types? @ 2005-01-25 12:28 Jim Farrand 2005-01-25 17:01 ` [Caml-list] " skaller 2005-01-25 18:37 ` brogoff 0 siblings, 2 replies; 6+ messages in thread From: Jim Farrand @ 2005-01-25 12:28 UTC (permalink / raw) To: caml-list Hi, This is what I need to do: Given a type, u, and a collection of types, ts, find a type t such that: * t is a member of ts * t can be unified with u * There is no type v in ts, which unifies with u and is more general than t. (In other words, find the most specific type in ts that is still equal to or a generalisation of u.) For example: ts = list int, int, list 'a, 'a For u = list int, the result would be list int. For u = list string, the result would be list 'a, and for u = string the result would be 'a. Note that I already have a function which can compute if type a is a specialisation of type b. I think that in theory, I could do a brute force approach: * Grab all types in ts that are generalisations of u. * Order the results according to how specific they are. * Arbitrarily choose one of the most specific. But there must be a smarter way! Eg, I think that I should be able to start with the type u, and incrementally generalise it until I find a match. It is tricky to find a method of generalisation that will cover the entire search space, and find the most specific type first. I am sure there must be papers on this, but I am having trouble coming up with the right search terms - references appreciated! :) Thanks in advance, Jim -- Jim Farrand ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [Caml-list] Type indexed types? 2005-01-25 12:28 Type indexed types? Jim Farrand @ 2005-01-25 17:01 ` skaller 2005-01-25 17:24 ` skaller 2005-01-25 18:37 ` brogoff 1 sibling, 1 reply; 6+ messages in thread From: skaller @ 2005-01-25 17:01 UTC (permalink / raw) To: Jim Farrand; +Cc: caml-list On Tue, 2005-01-25 at 23:28, Jim Farrand wrote: > Hi, > > This is what I need to do: > > Given a type, u, and a collection of types, ts, find a type t such that: > * t is a member of ts > * t can be unified with u > * There is no type v in ts, which unifies with u and is more general > than t. > > (In other words, find the most specific type in ts that is still equal > to or a generalisation of u.) This is the overload resolution problem? Shouldn't that last condition be reversed? You're looking for the most specialised, not most general type that matches u. > For example: > > ts = list int, int, list 'a, 'a > > For u = list int, the result would be list int. For u = list string, > the result would be list 'a, and for u = string the result would be 'a. > > Note that I already have a function which can compute if type a is a > specialisation of type b. > > I think that in theory, I could do a brute force approach: > * Grab all types in ts that are generalisations of u. > * Order the results according to how specific they are. > * Arbitrarily choose one of the most specific. > > But there must be a smarter way! Not really. Here is what Felix does: first, find all the matches. Now we need the most specialised. My notes say: (* start with an empty list, and fold one result at a time into it, as follows: if one element of the list is greater (more general) than the candidate, then add the candidate to the list and remove all element greater than the candidate, otherwise, if one element of the list is less then the candidate, keep the list and discard the candidate. The list starts off empty, so that all elements in it are vacuously incomparable. It follows either the candidate is not less than all the list, or less than all the list: that is, there cannot be two element a,b such that a < c < b, since by transitivity a < c would follow, contradicting the assumption the list contains no ordered pairs. If in case 1, all the greater element are removed and c added, all the elements must be less or not comparable to c, thus the list remains without comparable pairs, otherwise in case 2, the list is retained and c discarded and so trivially remains unordered. *) So basically, you keep a list of incomparable types, and fold one of the candidates into it at a time, retaining the invariant. If the candidate compares with any element in the list, you either chuck out the candidate because it is too general (the list remains the same), or you chuck out all the elements in the list that it is comparable with, and then add it to the list (so the list ends up with all incomparable elements again). Here's my actual algorithm, cleaned up a bit. As far as I know this is the best possible algorithm. let candidates = fold_left (fun oc r -> match r with Unique (j,c,_,_) -> let rec aux lhs rhs = match rhs with | [] -> r::lhs (* return all non-greater elements plus candidate *) | (Unique(i,typ,mgu,ts) as x)::t -> begin match compare_sigs syms.dfns typ c with | `Less -> lhs @ rhs (* keep whole list, discard c *) | `Equal -> ERROR "[resolve_overload] Ambiguous call" | `Greater -> aux lhs t (* discard greater element *) | `Incomparable -> aux (x::lhs) t (* keep element *) end | Fail::_ -> assert false in aux [] oc | Fail -> assert false ) [] candidates in match candidates with | [Unique (i,t,mgu,ts)] -> Some (i,t,mgu,ts) | [] -> None | _ -> ERROR "More than one match" -- John Skaller, mailto:skaller@users.sf.net voice: 061-2-9660-0850, snail: PO BOX 401 Glebe NSW 2037 Australia Checkout the Felix programming language http://felix.sf.net ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [Caml-list] Type indexed types? 2005-01-25 17:01 ` [Caml-list] " skaller @ 2005-01-25 17:24 ` skaller 2005-01-25 17:49 ` skaller 0 siblings, 1 reply; 6+ messages in thread From: skaller @ 2005-01-25 17:24 UTC (permalink / raw) To: Jim Farrand; +Cc: caml-list On Wed, 2005-01-26 at 04:01, skaller wrote: > On Tue, 2005-01-25 at 23:28, Jim Farrand wrote: > > Note that I already have a function which can compute if type a is a > > specialisation of type b. The algorithm I have requires a comparison with 4 possible results: less, greater, equal or incomparable. You can derive that from just less-equal: match a <= b, b <= a with | true, true -> Equal | true, false -> Less | false, true -> Greater | false, false -> Incomparable Unfortunately this requires two unification steps. To use you own comment "There must be a better way" but I don't know what it is. BTW: I obtain this result by adding a constraint to the unification algorithm that it only permits equations of the form: 'a = t in the MGU, where 'a is a variable taken from the LHS of the input equation (there is only a single equation when you're measuring 'less') This is essential matching an function argument against a function signature (we want to reduce the signature to make it equal to the argument). However, when we're trying to order all the match candidates, it would be nicer to get one of the above four results in one unification step. However it just won't work for an arbitrary MGU, which might have the LHS variables coming from either side of the equation. This can happen if you get matching type variables. Unfortunately, you can't just pick the LHS one every time, since after substitution, an RHS variable can end uo on the LHS .. :( So I'd like to know if there is a better way to calculate the four value partial ordering relation between two types than two comparisons for less.. any hints? -- John Skaller, mailto:skaller@users.sf.net voice: 061-2-9660-0850, snail: PO BOX 401 Glebe NSW 2037 Australia Checkout the Felix programming language http://felix.sf.net ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [Caml-list] Type indexed types? 2005-01-25 17:24 ` skaller @ 2005-01-25 17:49 ` skaller 2005-01-25 18:36 ` skaller 0 siblings, 1 reply; 6+ messages in thread From: skaller @ 2005-01-25 17:49 UTC (permalink / raw) To: Jim Farrand; +Cc: caml-list On Wed, 2005-01-26 at 04:24, skaller wrote: > > However, when we're trying to order all the match > candidates, it would be nicer to get one of the > above four results in one unification step. Argg .. sorry for answering my own post, but now it is obvious how to do it. 1) Set the result to Equal 2) if you have an equation 'a = T or T = 'a where T is not a type variable, and then: if the current result is Equal reset it to 'less' or 'greater' depending which side of the original pair of terms 'a is on, otherwise return Incomparable 3) if you get a mismatch, return Incomparable 4) Otherwise you have an equation between two type variables, which doesn't change the current result Provided you haven't returned incomparable, you continue unifying in the usual way, returning the result when the MGU is found. -- John Skaller, mailto:skaller@users.sf.net voice: 061-2-9660-0850, snail: PO BOX 401 Glebe NSW 2037 Australia Checkout the Felix programming language http://felix.sf.net ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [Caml-list] Type indexed types? 2005-01-25 17:49 ` skaller @ 2005-01-25 18:36 ` skaller 0 siblings, 0 replies; 6+ messages in thread From: skaller @ 2005-01-25 18:36 UTC (permalink / raw) To: Jim Farrand; +Cc: caml-list On Wed, 2005-01-26 at 04:49, skaller wrote: > On Wed, 2005-01-26 at 04:24, skaller wrote: > > > > > However, when we're trying to order all the match > > candidates, it would be nicer to get one of the > > above four results in one unification step. > > Argg .. sorry for answering my own post, > but now it is obvious how to do it. > > 1) Set the result to Equal > > 2) if you have an equation > > 'a = T > or > T = 'a > > where T is not a type variable, and then: > > if the current result is Equal reset it > to 'less' or 'greater' depending which side > of the original pair of terms 'a is on, > > otherwise return Incomparable Argg .. bug .. this should read: otherwise if the result is not 'less' or 'greater' consistent with which side of the original pair 'a is on, return incomparable (otherwise continue) > > 3) if you get a mismatch, return Incomparable > > 4) Otherwise you have an equation between > two type variables, which doesn't change > the current result > > Provided you haven't returned incomparable, > you continue unifying in the usual way, > returning the result when the MGU is found. -- John Skaller, mailto:skaller@users.sf.net voice: 061-2-9660-0850, snail: PO BOX 401 Glebe NSW 2037 Australia Checkout the Felix programming language http://felix.sf.net ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [Caml-list] Type indexed types? 2005-01-25 12:28 Type indexed types? Jim Farrand 2005-01-25 17:01 ` [Caml-list] " skaller @ 2005-01-25 18:37 ` brogoff 1 sibling, 0 replies; 6+ messages in thread From: brogoff @ 2005-01-25 18:37 UTC (permalink / raw) To: Jim Farrand; +Cc: caml-list You are close, I think, to related things that would probably interest you Try googling these "type indexed data types" "guarded algebraic data types" in particular, see Simonet and Pottier's work available from the project Cristal web site. I think the application of constraint solving to type systems is a popular topic these days in the type theory community. -- Brian On Tue, 25 Jan 2005, Jim Farrand wrote: > Hi, > > This is what I need to do: > > Given a type, u, and a collection of types, ts, find a type t such that: > * t is a member of ts > * t can be unified with u > * There is no type v in ts, which unifies with u and is more general > than t. > > (In other words, find the most specific type in ts that is still equal > to or a generalisation of u.) > > For example: > > ts = list int, int, list 'a, 'a > > For u = list int, the result would be list int. For u = list string, > the result would be list 'a, and for u = string the result would be 'a. > > Note that I already have a function which can compute if type a is a > specialisation of type b. > > I think that in theory, I could do a brute force approach: > * Grab all types in ts that are generalisations of u. > * Order the results according to how specific they are. > * Arbitrarily choose one of the most specific. > > But there must be a smarter way! Eg, I think that I should be able to > start with the type u, and incrementally generalise it until I find a > match. It is tricky to find a method of generalisation that will cover > the entire search space, and find the most specific type first. > > I am sure there must be papers on this, but I am having trouble coming > up with the right search terms - references appreciated! :) > > Thanks in advance, > Jim > > -- > Jim Farrand > > _______________________________________________ > Caml-list mailing list. Subscription management: > http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > ^ permalink raw reply [flat|nested] 6+ messages in thread
end of thread, other threads:[~2005-01-25 18:37 UTC | newest] Thread overview: 6+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2005-01-25 12:28 Type indexed types? Jim Farrand 2005-01-25 17:01 ` [Caml-list] " skaller 2005-01-25 17:24 ` skaller 2005-01-25 17:49 ` skaller 2005-01-25 18:36 ` skaller 2005-01-25 18:37 ` brogoff
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).