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 4B78F820A1 for ; Sun, 11 Aug 2013 15:29:22 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of kosmo.zb@gmail.com) identity=pra; client-ip=209.85.215.47; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="kosmo.zb@gmail.com"; x-sender="kosmo.zb@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of kosmo.zb@gmail.com designates 209.85.215.47 as permitted sender) identity=mailfrom; client-ip=209.85.215.47; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="kosmo.zb@gmail.com"; x-sender="kosmo.zb@gmail.com"; 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@mail-la0-f47.google.com) identity=helo; client-ip=209.85.215.47; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="kosmo.zb@gmail.com"; x-sender="postmaster@mail-la0-f47.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AmwCAPuQB1LRVdcvjWdsb2JhbABahAusQJIggRAIFg4BAQEBBwsLCRIGJIIkAQEEAUABMQcBAwELAQUFCw0uIhIBBQEcBhOHfgMJBplgj1ODbicNV4gBAQUMjnOBCYRLA5dkj2wWKYFdgmU7gSw X-IPAS-Result: AmwCAPuQB1LRVdcvjWdsb2JhbABahAusQJIggRAIFg4BAQEBBwsLCRIGJIIkAQEEAUABMQcBAwELAQUFCw0uIhIBBQEcBhOHfgMJBplgj1ODbicNV4gBAQUMjnOBCYRLA5dkj2wWKYFdgmU7gSw X-IronPort-AV: E=Sophos;i="4.89,856,1367964000"; d="scan'208";a="29053050" Received: from mail-la0-f47.google.com ([209.85.215.47]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 11 Aug 2013 15:29:21 +0200 Received: by mail-la0-f47.google.com with SMTP id eo20so4067935lab.20 for ; Sun, 11 Aug 2013 06:29:20 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:sender:in-reply-to:references:date:message-id:subject :from:to:cc:content-type:content-transfer-encoding; bh=QuebSBZqXXVkC0zaQWRDTJajfMCATr9BXjswx4VFbbM=; b=njibjrgFnCYA13Ummv6hUInni8pBY8SGP2IV6ubDVPHZ2r5YKTDg7Xk+5Ka1Lf1Ba4 FlqCnVZz0qSnY0LYDY2wLGMShh/4Bapejed0HVv8tPZivPG7nNfNXcNzdxVoraeqlQm6 AAqdpO1SDA5YsLgOBOcGLOq/KV1ZqX3NAKOuwt4ipXJkZ2wfen3G1AMbDaJ/Z6wReMfB 2yNNzdYcedQOyYTFQWvNG6dVuhtwXFAfhm262yIMSGsi1L9wcGXH11Y72m1UX+Bcl/dU K3yB/Zb6/QGugRk1Kis/O8UHFVgtfNK0k723c2yrNFIqaRaDKpR6uuR+7KWttXVaUqLk ZcpA== MIME-Version: 1.0 X-Received: by 10.112.188.165 with SMTP id gb5mr3619984lbc.38.1376227760868; Sun, 11 Aug 2013 06:29:20 -0700 (PDT) Sender: kosmo.zb@gmail.com Received: by 10.112.61.130 with HTTP; Sun, 11 Aug 2013 06:29:20 -0700 (PDT) In-Reply-To: <1407E74D-EDC8-4638-8917-4CAC80B4C682@mpi-sws.org> References: <1407E74D-EDC8-4638-8917-4CAC80B4C682@mpi-sws.org> Date: Sun, 11 Aug 2013 14:29:20 +0100 X-Google-Sender-Auth: qktwFsWRMNZyonW6Nqvm7RxJyOM Message-ID: From: David Sheets To: Andreas Rossberg Cc: Caml List Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] First-class Functor Forgetting for Free On Sun, Aug 11, 2013 at 8:53 AM, Andreas Rossberg wr= ote: > On Aug 11, 2013, at 03:55 , David Sheets wrote: >> I understand why structural subtyping requires a module cast but I >> don't see why type relaxation would. >> I looked at the generated assembly and this line seems to disappear. >> >> Why is it needed? > > There is no implicit subtyping in OCaml's core language. The reason for t= hat is not code generation, but type inference. For example, what type shou= ld the following function be given if the subtyping you ask for could apply? > > let g x =3D let module X =3D (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 guess the module system isn't part of the core as it does implicit structural subtyping. This makes the embedding of the module type system into the value type system surprising. > That said, as usual in OCaml, you can force subtyping explicitly. That is= , you are able to just say > > let module M' =3D (val f (x :> (module D)) : C) in =85 Good to know! I looked briefly and did not see this mentioned in the manual. > in your example. (Explicit subtyping on package types is still very limit= ed, though, i.e. only allows forgetting type equations on the same named si= gnature.) This seems somewhat strange. Why are aliases not followed? David