From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id B64A1BC8C for ; Tue, 25 Jan 2005 19:37:58 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j0PIbwxV028812 for ; Tue, 25 Jan 2005 19:37:58 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id TAA00413 for ; Tue, 25 Jan 2005 19:37:57 +0100 (MET) Received: from mail25.sea5.speakeasy.net (mail25.sea5.speakeasy.net [69.17.117.27]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j0PIbtQm028805 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Tue, 25 Jan 2005 19:37:57 +0100 Received: (qmail 24568 invoked from network); 25 Jan 2005 18:37:54 -0000 Received: from shell1.speakeasy.net ([69.17.110.70]) (envelope-sender ) by mail27.sea5.speakeasy.net (qmail-ldap-1.03) with AES256-SHA encrypted SMTP for ; 25 Jan 2005 18:37:54 -0000 Date: Tue, 25 Jan 2005 10:37:54 -0800 (PST) From: brogoff To: Jim Farrand Cc: caml-list@inria.fr Subject: Re: [Caml-list] Type indexed types? In-Reply-To: <20050125122849.GB15086@draco.xyxyx.org> Message-ID: References: <20050125122849.GB15086@draco.xyxyx.org> MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Miltered: at concorde with ID 41F69206.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 41F69203.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 simonet:01 wrote:01 arbitrarily:01 generalise:01 caml-list:01 beginner's:01 ocaml:01 beginners:01 bug:01 speakeasy:01 cristal:01 bin:01 yquem:01 int:01 X-Spam-Checker-Version: SpamAssassin 3.0.0 (2004-09-13) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.0 X-Spam-Level: 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 >