From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id B8E89BC57 for ; Fri, 16 Apr 2010 20:22:06 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ai0CAONHyEvUGyoGkWdsb2JhbACbdBUBAQEBCQsKBxEDH79LglqCNAQ X-IronPort-AV: E=Sophos;i="4.52,221,1270418400"; d="scan'208";a="57183989" Received: from smtp6-g21.free.fr ([212.27.42.6]) by mail1-smtp-roc.national.inria.fr with ESMTP; 16 Apr 2010 20:22:05 +0200 Received: from smtp6-g21.free.fr (localhost [127.0.0.1]) by smtp6-g21.free.fr (Postfix) with ESMTP id 5A996E080E9 for ; Fri, 16 Apr 2010 20:22:00 +0200 (CEST) Received: from [192.168.0.3] (rke75-3-82-229-183-156.fbx.proxad.net [82.229.183.156]) by smtp6-g21.free.fr (Postfix) with ESMTP id 6DA0CE08158 for ; Fri, 16 Apr 2010 20:21:58 +0200 (CEST) Message-ID: <4BC8AAC4.40404@lexifi.com> Date: Fri, 16 Apr 2010 20:21:56 +0200 From: Alain Frisch Organization: LexiFi User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.9.1.9) Gecko/20100408 Shredder/3.0.5pre MIME-Version: 1.0 To: caml-list Subject: Subtyping of first-class module types Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; frisch:01 frisch:01 lexifi:01 subtyping:01 ocaml:01 subtyping:01 annotations:01 subtype:01 trivial:01 runtime:01 val:01 subtype:01 annotations:01 caml-list:01 coercion:01 Dear caml-list, During today's ocaml meeting, the question of whether first-class module types could support subtyping was asked. I'd like to give a more detailed answer here. The explicit subtyping construction (e : t1 :> t2) could easily be extended to support subtyping of the form (module S with type t1 = ...) :> (module S) that is, to forget some type annotations. One could also support subtyping of the form: (module S) :> (module S') provided that S is a subtype of S' (as module types), and *moreover* that the coercion from S to S' is the identity. The only real use I could see for it is when S and S' refer to the equal module types but they are just different names (in which case (module S) and module (module S') cannot be unified). The reason to require the coercion S ~~> S' to be trivial is that the explicit subtyping construction is assumed to be a runtime no-op. That said, it is not difficult to use subtyping of module types by hand as in: (module (val x : S) : S') which works as soon as S is a subtype of S'. Concretly, the code generated for this piece of code is simply the coercion from module type S to module type S'. This also work to forget type annotations (in which case the coercion is the identity). Given how simple this construction is, I don't think it is worth extending the ( :> ) relation to support module types in very limited cases. Alain