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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 124637F1AA for ; Fri, 11 Sep 2015 18:24:28 +0200 (CEST) IronPort-PHdr: 9a23:Xuo4JBCrL1PW9zhmiHAtUyQJP3N1i/DPJgcQr6AfoPdwSP/7o8bcNUDSrc9gkEXOFd2CrakU16yP4+u5ATZIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/ni6brq9aKO18ArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIZoGJ/3dKUgTLFeEC9ucyVsvJWq5lH/Sl6E734YF2EXiQZgAg7f7Ri8UI21+g7zrOlgw2G/OtHqSfhgXD247LpwDhrvlDsDHzE8+WDTzMd3ifQIjgimoklawo3UaYCRfN93eK/HbNAbQyIVW89XWzZQAYK6R4oUF/AIJqBCst+u9BM1sRKiCFz0V6vUwThSiyqzhPVi3g== Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mandrykin@ispras.ru; spf=None smtp.mailfrom=mandrykin@ispras.ru; spf=None smtp.helo=postmaster@smtp.ispras.ru Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of mandrykin@ispras.ru) identity=pra; client-ip=83.149.199.79; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mandrykin@ispras.ru"; x-sender="mandrykin@ispras.ru"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of mandrykin@ispras.ru) identity=mailfrom; client-ip=83.149.199.79; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mandrykin@ispras.ru"; x-sender="mandrykin@ispras.ru"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@smtp.ispras.ru) identity=helo; client-ip=83.149.199.79; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mandrykin@ispras.ru"; x-sender="postmaster@smtp.ispras.ru"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0A2AQA8//JVjU/HlVNdg3dphQ2vA4sjhX0CgVU8EAEBAQEBAQEBEAEBAQEJFgcSPYIdggcBAQQnEz8QCxgJFRAPAUcGARKIMsxXAQEBAQEFAQEBAR6LcIRaMweELAEEjWiHboUKigKGWpINOIQvboofAQEB X-IPAS-Result: A0A2AQA8//JVjU/HlVNdg3dphQ2vA4sjhX0CgVU8EAEBAQEBAQEBEAEBAQEJFgcSPYIdggcBAQQnEz8QCxgJFRAPAUcGARKIMsxXAQEBAQEFAQEBAR6LcIRaMweELAEEjWiHboUKigKGWpINOIQvboofAQEB X-IronPort-AV: E=Sophos;i="5.17,511,1437429600"; d="scan'208";a="145509025" Received: from smtp.ispras.ru ([83.149.199.79]) by mail3-smtp-sop.national.inria.fr with ESMTP; 11 Sep 2015 18:24:26 +0200 Received: from molnar.localnet (unknown [83.149.199.91]) by smtp.ispras.ru (Postfix) with ESMTP id C301820504; Fri, 11 Sep 2015 19:24:24 +0300 (MSK) From: Mikhail Mandrykin To: caml-list@inria.fr, Markus Mottl Cc: OCaml List Date: Fri, 11 Sep 2015 19:24:24 +0300 Message-ID: <4930712.OXrVy1QyIs@molnar> User-Agent: KMail/4.14.6 (Linux/3.19.0-26-generic; KDE/4.14.6; x86_64; ; ) In-Reply-To: References: <1527892.mlrKSESLQ8@molnar> MIME-Version: 1.0 Content-Transfer-Encoding: 7Bit Content-Type: text/plain; charset="us-ascii" Subject: Re: [Caml-list] Late adding of type variable constraints On Friday, September 11, 2015 11:56:33 AM Markus Mottl wrote: > But wouldn't this require making Newtype1 a generative > functor (i.e. adding "()")? Otherwise the type "t" could be seen as > equivalent if Newtype1 is applied to the same module more than once, > which would allow for more than one "Mk" case and could hence cause a > runtime match error. Yes, indeed. module T : sig type t = int end;; module N1 = Newtype0(T);; module N2 = Newtype0(T);; # N1.prj @@ N2.inj 0;; Exception: Match_failure ("//toplevel//", 10, 10). With generative functors this causes a typing error. In this case it's also possible to use even simpler encoding without open types (`('a, ... ('z, nil) app) ...) app) t'): type ('p, 'f) app = App of 'p * 'f type nil module Newtype1 (T : sig type 'a t end) = struct type 'a t = Mk : 'a T.t -> (('a, nil) app) t let inj v = Mk v let prj (Mk v) = v end -- Mikhail Mandrykin Linux Verification Center, ISPRAS web: http://linuxtesting.org e-mail: mandrykin@ispras.ru