From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 2B8F3820A1 for ; Mon, 12 Aug 2013 13:02:05 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of rossberg@mpi-sws.org) identity=pra; client-ip=139.19.1.49; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="rossberg@mpi-sws.org"; x-sender="rossberg@mpi-sws.org"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of rossberg@mpi-sws.org designates 139.19.1.49 as permitted sender) identity=mailfrom; client-ip=139.19.1.49; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="rossberg@mpi-sws.org"; x-sender="rossberg@mpi-sws.org"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@hera.mpi-klsb.mpg.de) identity=helo; client-ip=139.19.1.49; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="rossberg@mpi-sws.org"; x-sender="postmaster@hera.mpi-klsb.mpg.de"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkkCAI2/CFKLEwExgGdsb2JhbABaDsJRgTAOAQELBwQJCRQFI4IkAQEBBCcRCAEBMAYBAQ8LDgoJFg8JAwIBAgEjBR0GDQEHAQGIDJh6iwyERwEFjTQGkDsHhBGeD44GQA X-IPAS-Result: AkkCAI2/CFKLEwExgGdsb2JhbABaDsJRgTAOAQELBwQJCRQFI4IkAQEBBCcRCAEBMAYBAQ8LDgoJFg8JAwIBAgEjBR0GDQEHAQGIDJh6iwyERwEFjTQGkDsHhBGeD44GQA X-IronPort-AV: E=Sophos;i="4.89,861,1367964000"; d="scan'208";a="29127687" Received: from hera.mpi-sb.mpg.de (HELO hera.mpi-klsb.mpg.de) ([139.19.1.49]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES256-SHA; 12 Aug 2013 13:02:04 +0200 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=mpi-sb.mpg.de; s=mail200803; h=Content-Transfer-Encoding:Content-Type:In-Reply-To:References:Subject:CC:To:MIME-Version:From:Date:Message-ID; bh=FGn3W8pPeX5/sS9YbY+ReltcBFGW2ImoHdyimll12pc=; b=XgvW2ZtrQPe+RN83ngG+kJhya88u8jJuYtg4osAKBZGbTDa2jJjvvTbFVbnfOj9mef8PhM8u8MikvrblifimYtzJ22XWbmD/ExtKuOkV2qD2jvYX7K0d7wV55x16D1A5Rp74w2lnsU4rIWvzD/OGhws5gr9OkEujDXVLzNL2T1k=; Received: from zak.mpi-klsb.mpg.de ([139.19.1.29]:50385) by hera.mpi-klsb.mpg.de (envelope-from ) with esmtp (Exim 4.72) id 1V8psu-00049M-Py; Mon, 12 Aug 2013 13:02:02 +0200 Received: from [74.125.57.233] (port=10755 helo=bozo.muc.corp.google.com) by zak.mpi-klsb.mpg.de (envelope-from ) with esmtpsa (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.72) id 1V8psu-0007zr-CO; Mon, 12 Aug 2013 13:02:00 +0200 Message-ID: <5208C0A7.2040906@mpi-sws.org> Date: Mon, 12 Aug 2013 13:01:59 +0200 From: Andreas Rossberg User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130804 Thunderbird/17.0.8 MIME-Version: 1.0 To: Leo White CC: David Sheets , Caml List References: <1407E74D-EDC8-4638-8917-4CAC80B4C682@mpi-sws.org> <9D61A8E2-D0B4-452A-B372-401E499423AE@mpi-sws.org> <86bo549sv9.fsf@cam.ac.uk> In-Reply-To: <86bo549sv9.fsf@cam.ac.uk> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-MPI-Local-Sender: true Subject: Re: [Caml-list] First-class Functor Forgetting for Free On 08/11/2013 04:58 PM, Leo White wrote: >>>> There is no implicit subtyping in OCaml's core language. The reason for that is not code generation, but type inference. For example, what type should the following function be given if the subtyping you ask for could apply? >>>> >>>> let g x = let module X = (val x : D) in X.(f x) >>> >>> Something like val g : [< (module D)] or simply val g : (module D) >>> where the type constraint relation is implicit seems reasonable. I >>> don't know if you consider polymorphic variant types as part of the >>> core language (or perhaps they aren't implicit because they propagate >>> inequalities?). >> >> I don't think type inference for polymorphic variants works the way you think it does. Inference for both variants and objects is based on row polymorphism, not subtyping. A type like [< A] is actually a polymorphic type with a hidden type variable, not a subtype bound, even though the surface syntax intentionally hides that fact (which isn't always helpful). Module signatures are totally different beasts, where matching _is_ a form of subtyping. > > I think David is suggesting that "with-constraints" on first-class > modules could be handled with row polymorphism, and I don't know of any > reason why they couldn't. It would certainly be a more flexible way to > type them. So, > > let g x = let module X = (val x : D) in X.(f x) > > would have a type: > > (module D with ..) -> int This certainly is a nice suggestive syntax, but it is assuming an underlying semantic similarity that does not exist. Semantically, the type sharing equations on signatures have very little in common with rows, and I have a hard time imagining what interpreting the above as a row would even mean, or how it would fit in with either core or module typing. (I could go into boring technical details here, but I'll leave it at that. :) ) /Andreas