From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 51D28BC8C for ; Tue, 25 Jan 2005 13:29:52 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j0PCTprR031697 for ; Tue, 25 Jan 2005 13:29:52 +0100 Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id NAA19161 for ; Tue, 25 Jan 2005 13:29:51 +0100 (MET) Received: from xyxyx (caelum.vs.mythic-beasts.com [212.69.37.45]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j0PCTpFs031694 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=NO) for ; Tue, 25 Jan 2005 13:29:51 +0100 Received: from draco.wormhole ([192.168.27.1] helo=draco.xyxyx.org) by xyxyx with esmtp (Exim 4.34) id 1CtPpO-0004p9-Tz for caml-list@inria.fr; Tue, 25 Jan 2005 12:29:51 +0000 Received: from jim by draco.xyxyx.org with local (Exim 4.43) id 1CtPoP-0004M3-WE for caml-list@inria.fr; Tue, 25 Jan 2005 12:28:50 +0000 Date: Tue, 25 Jan 2005 12:28:49 +0000 From: Jim Farrand To: caml-list@inria.fr Subject: Type indexed types? Message-ID: <20050125122849.GB15086@draco.xyxyx.org> Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline X-Mail-Key: JimbosMagicMailKey X-Miltered: at nez-perce with ID 41F63BBF.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 41F63BBF.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; arbitrarily:01 generalise:01 int:01 int:01 match:02 tricky:02 types:02 types:02 string:03 string:03 papers:05 approach:07 space:07 theory:07 function:08 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: 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