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 24FBD7FA5E for ; Wed, 26 Apr 2017 22:09:33 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=yallop@gmail.com; spf=Pass smtp.mailfrom=yallop@gmail.com; spf=None smtp.helo=postmaster@mail-qt0-f181.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of yallop@gmail.com) identity=pra; client-ip=209.85.216.181; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="yallop@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of yallop@gmail.com designates 209.85.216.181 as permitted sender) identity=mailfrom; client-ip=209.85.216.181; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="yallop@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-qt0-f181.google.com) identity=helo; client-ip=209.85.216.181; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="postmaster@mail-qt0-f181.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3A/tnQ9B+eDw1xUv9uRHKM819IXTAuvvDOBiVQ1KB4?= =?us-ascii?q?0uMcTK2v8tzYMVDF4r011RmSDNmds6oMotGVmpioYXYH75eFvSJKW713fDhBt/?= =?us-ascii?q?8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1?= =?us-ascii?q?Ifn+FpLPg8it2e2//5Lebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+?= =?us-ascii?q?RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTF?= =?us-ascii?q?UACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRx3miC?= =?us-ascii?q?kHOTA383zZhNJsg69AvBKtuwZyz5LIbI2JNvdzeL7Wc9MARWpGW8ZcTyhPDZ2m?= =?us-ascii?q?b4QRCuoAPftToIvnqFsKqRu+AhGsD/7oxz5InHD22ak60+M5EQzd0wwgGsgBsH?= =?us-ascii?q?XQrNnvKKgSVuW1wbDOwD7ebP1WwS/w5JbUfh0lu/2BXrJ9fdDPxUUyFg7JlEic?= =?us-ascii?q?pI/4Mz6Ty+8DqXKU7/B6WuKqk2Mnqx9+ojyoxso0j4nGnIMVylTd+SVg3IY5Oc?= =?us-ascii?q?S0SEBmbdOnDZdcrS6aN4xxQsMtR2Fnpjw2xaEBuZ6+ZCQKyZInyADDa/GfbYSE?= =?us-ascii?q?/hbuWPySLDp4nn5pZq+ziheo/US9yeDwS9G40FNQoSpEltnMuGoN1xvW6sWfSv?= =?us-ascii?q?py5EOh2TKI1wDL8exELkU0mrDaK54l2LI/ip0TsUHbEi/shEr2lLOWdlkj+uWw?= =?us-ascii?q?9+voeLDmppuFO49wiwH+Kbgul9ekAeU4NwgOR3KU9f691L3l5035Qa9Fguc4kq?= =?us-ascii?q?nD49jmIpE+r7K0AUd21Z0i6F7rUmj4jN9AxygNcgIVc0uM14SzZ1iULaGnBvvg?= =?us-ascii?q?3QiiuDhuzvHCeLbmB8OeAGLEleLDcKxw7l8U+QM3yddHr8ZFA7UFJ+rbVUr4td?= =?us-ascii?q?ieBRg8ZV/ni937Aclwg9tNEVmEBbWUZfvf?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AHAwAb/gBZf7XYVdFcGwEBAQMBAQEJA?= =?us-ascii?q?QEBFgEBAQMBAQEJAQEBhQUSB4Nhm1+XeoYkAoQjB0MUAQEBAQEBAQEBAQESAQE?= =?us-ascii?q?JCwsIJjFCDoFjIIJDAQIDIwQZARsdAQMMBgULDQICJgICIQEBEQEFARwGE4oCA?= =?us-ascii?q?QMVnmY/jAiBbBgFARyDCgWDYgoZJw1WgwkBAQEBAQUBAQEBARsCBhJ5hyeDGoJ?= =?us-ascii?q?ThRKCXwWdFTuOQIRMkV6LGYdGFB+BFTaBKCcdCBkVRBmERYIPPzWCaYYMAQEB?= X-IPAS-Result: =?us-ascii?q?A0AHAwAb/gBZf7XYVdFcGwEBAQMBAQEJAQEBFgEBAQMBAQE?= =?us-ascii?q?JAQEBhQUSB4Nhm1+XeoYkAoQjB0MUAQEBAQEBAQEBAQESAQEJCwsIJjFCDoFjI?= =?us-ascii?q?IJDAQIDIwQZARsdAQMMBgULDQICJgICIQEBEQEFARwGE4oCAQMVnmY/jAiBbBg?= =?us-ascii?q?FARyDCgWDYgoZJw1WgwkBAQEBAQUBAQEBARsCBhJ5hyeDGoJThRKCXwWdFTuOQ?= =?us-ascii?q?IRMkV6LGYdGFB+BFTaBKCcdCBkVRBmERYIPPzWCaYYMAQEB?= X-IronPort-AV: E=Sophos;i="5.37,255,1488841200"; d="scan'208";a="270669000" Received: from mail-qt0-f181.google.com ([209.85.216.181]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 26 Apr 2017 22:09:32 +0200 Received: by mail-qt0-f181.google.com with SMTP id c45so10411189qtb.1 for ; Wed, 26 Apr 2017 13:09:32 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=WnhXTEo+IcIDpMWVgNTrowruwt0fho5bftu8/nEnt3o=; b=tkRoUyTyk/yN5inAYVhb9ZiEHm8oSymGpNPfctvS1JX8Lw88UIBSA8wxPk4c9P79IE 4HjIAaEeZlkKDqPjMlYmDOVNOquAVe0/x+pCvhnw9Z0+ULP4xiA+9a1oZTq0PnG/bC+h bKjvAjMBxjIG7ZBlajC4wxBFxp/cnh/HELziinPbIv2NqVEo5YYckXdX0YBPfp+2qvb5 rG/fxlIn0Pp+vtxOUznQN6lgi9kKHdS4iugW+XKCbXPqopwscpdJieJCc0rRw+JMhNDC VkVQ967mbgGOsUoJGWW6Rtiw3Vy9u2nJhFiiEV7zK8V2MyQisQk6xmH0WXO9f1oOu8SK EX8A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc; bh=WnhXTEo+IcIDpMWVgNTrowruwt0fho5bftu8/nEnt3o=; b=OG8+KhajN3ZhTP31cUCi8ljTVasD3zn1iYfYELVSfHCUIk0ck2y2nA2T1p2C7+l6Sj OMJyU8ZJuI6xtyMSuMy73ANplLkb8uyjMIox+c+F8HKPT2DH8gyNDnM7atbLXIRKvcYN WUsUA3eNP4kXZz7Q9DjNX5NqKvZ2gMb8VzJPytnTJx0sj/sxjHBKaP15SThKVgnbolCK IwA0pvutBDh9nm8FWcrFbidMLsVtMadnU5K5Foui9IIzSb5w/whX5mxNvbGzIJ00I3g/ uTaiWVw7OVM68CbEX9XhIEyQbs3DBQ8mVnEG54nEb7Xfs+/3na/St6pPWW8Sm03w6Hbg TfLg== X-Gm-Message-State: AN3rC/5gURFUzvVbrdpUIVUEBz7Ckx+R8RmNxt1xC3qCZR6dwbXaHVyr kDzoB/KFMUuxOTUmitMMN75cZtjXag== X-Received: by 10.237.36.5 with SMTP id r5mr1538921qtc.253.1493237371062; Wed, 26 Apr 2017 13:09:31 -0700 (PDT) MIME-Version: 1.0 Received: by 10.55.185.70 with HTTP; Wed, 26 Apr 2017 13:09:30 -0700 (PDT) In-Reply-To: <7b36d78d-f20f-f504-db11-b95dd1df2bf9@gmail.com> References: <7b36d78d-f20f-f504-db11-b95dd1df2bf9@gmail.com> From: Jeremy Yallop Date: Wed, 26 Apr 2017 21:09:30 +0100 Message-ID: To: Matej Kosik <5764c029b688c1c0d24a2e97cd764f@gmail.com> Cc: caml-list Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] a question about Ocaml semantics Dear Matej, On 26 April 2017 at 15:26, Matej Kosik <5764c029b688c1c0d24a2e97cd764f@gmail.com> wrote: > I am not sure I understand particular aspect of Ocaml semantics. > > In the context of an *.ml file, can > > struct include A end > > be in general (i.e. unconditionally always) be rewritten to > > A > > ? The answer depends a bit on exactly what you consider semantics as opposed to implementation details, but there are a few cases where the rewriting you describe either changes the behaviour of programs or changes whether the programs are accepted by the type checker. Since 'struct include A end' allocates in the current implementation, while 'A' does not allocate, any program that detects allocation behaviour will be able to tell the difference between the two. Physical equality (whose behaviour on package types is implementation-dependent) is a simple example. If you have the following definitions module type T = sig val x : int end module M = struct let x = 0 end then this expression evaluates to 'false': # (module struct include A end :T) == (module A);; - : bool = false but rewriting 'struct include A end' to 'A' changes the result to 'true': # (module A :T) == (module A);; - : bool = true There are other ways to detect allocation, but most or all of them are similarly implementation-dependent. There's a second difference, related to typing. The module type expression 'module type of A' does not add equalities to the types of A, while 'module type of struct include A end' does include the equalities: # module A = struct type t end;; module A : sig type t end # module type S = module type of A;; module type S = sig type t end # module type S = module type of struct include A end;; module type S = sig type t = A.t end Since changing 'struct include A end' to 'A' removes some type equalities, there are programs that are well-typed before the change but ill-typed after. For example, if you have the following definition module A : sig type t val x : t end = struct type t = int let x = 0 end then the following program is well-typed, because M1.t is equal to A.t module M1 : module type of struct include A end = A M1.x = A.x but the following program is ill-typed, because M2.t is not equal to A.t module M2 : module type of A = A M2.x = A.x With a bit more effort it's possible to come up with an example where the program remains well-typed but the behaviour changes. In many cases types are just a check that a program won't go wrong, and type-checking doesn't change the behaviour of a program. But in a few cases the OCaml implementation uses type information to decide how to compile and execute a program. For example, if the OCaml compiler can tell that all the fields in a record type are floats then the record will be given an unboxed layout. The following example shows how the layout of records can change according to whether 'struct include A end' or 'A' is used in a particular location. Suppose you have a GADT that tells you whether a type is equal to float: type _ is_float = Is_float : float is_float and an existential type that can hold any value: type box = Box : _ -> box and a module with an abstract type 't' together with a value of type 't' and a proof that 't' is equal to float: module A : sig type t val x : t val is_float : t is_float end = struct type t = float let x : t = 0.0 let is_float = Is_float end Then the behaviour of the following program changes if you replace 'struct include A end' with 'A': match A.is_float with Is_float -> let module X = struct module N : module type of struct include A end = A type t1 = {x:float} and t2 = {y:N.t} end in assert (X.(Box {x=0.0} = Box {y=N.x})) When the program above is compiled N.t is known to be equal to A.t and A.t is known to be equal to float under the match, so both the 't1' and 't2' records are given identical unboxed layouts and the assertion succeeds. However, if you change 'struct include A end' to 'A' then N.t is no longer equal to A.t, and so 't2' does not have an unboxed layout. Since the polymorphic equality function '=' compares values by their layout, the difference between 't1' and 't2' is observable. Kind regards, Jeremy.