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 CCF757EE78 for ; Thu, 14 Apr 2016 11:56:52 +0200 (CEST) IronPort-PHdr: 9a23:3rWAvBCY4J8uPOi5nbHwUyQJP3N1i/DPJgcQr6AfoPdwSP7zrsbcNUDSrc9gkEXOFd2CrakU26yL7eu4CSQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTnkb3ssMWDKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46Fp34d6XK77Z6U1S6BDRHRjajhtpZ6jiR6WaAqL730raXkflB1KDhbE51muW5b1uy3hqsJy3SCbOYv9SrViChq46KI+ahbjkToKLHYW+XvNi8NtgeoPrxu7vR1w3oP8ZYiJNLx4d6zabNpfWCxIVYBTT3oSUcuHc4ITAr9Zbq5jpI7nqg5L9EPmCA== Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=garrigue@math.nagoya-u.ac.jp; spf=None smtp.mailfrom=garrigue@math.nagoya-u.ac.jp; spf=None smtp.helo=postmaster@mailhost.math.nagoya-u.ac.jp Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0A+AQAMaA9XigWCBoVEGoQLfQG8LhcLhWwCgXERAQEBAQEBAQERAQEBChYHUIItghUBAQQjHQMBNQEBDgsYAgIYDgICVwaIOw8srlVnhEYCiRqEXwEBAQEBAQEDAQEBAQEBAQERAQZ8hxqCVoQ9gkoLLRMYgiuNV3OJRoV3iBaCNYxbhnKINzaCQYFhXQGJeQEBAQ X-IPAS-Result: A0A+AQAMaA9XigWCBoVEGoQLfQG8LhcLhWwCgXERAQEBAQEBAQERAQEBChYHUIItghUBAQQjHQMBNQEBDgsYAgIYDgICVwaIOw8srlVnhEYCiRqEXwEBAQEBAQEDAQEBAQEBAQERAQZ8hxqCVoQ9gkoLLRMYgiuNV3OJRoV3iBaCNYxbhnKINzaCQYFhXQGJeQEBAQ X-IronPort-AV: E=Sophos;i="5.24,484,1454972400"; d="scan'208";a="214087347" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail2-smtp-roc.national.inria.fr with ESMTP; 14 Apr 2016 11:56:51 +0200 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id D1F256395 for ; Thu, 14 Apr 2016 18:56:48 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (rabbit-172.math.nagoya-u.ac.jp [172.16.254.254]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 7A397414C; Thu, 14 Apr 2016 18:56:48 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= content-type:mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; s=alpha; bh=jYH7F6VSnGgBivX8i2eoe3yauVU=; b=livd95hxJejod1aRutO+I0GuEY5p zNNx1+OgN2NOLlW2N9iQnHOts+gsDvn8OT8O5gi+uH2KSzT8X+dIzrefOq0sgfXF tqbHk1OsgH31iPBNcKiK002Orb4z6cvPFcdhdB7pP76RbZMhUdCARuyUluqlEO4s BPHRyz4DD8mdVj0= DomainKey-Signature: a=rsa-sha1; h=Received:Content-Type:Mime-Version:Subject:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=KfJygDob83k0N4fI3s+T17k3buGp8f1lboKNoX19OlS264LlmJ+OkenT9KJEy0bJz82VrDoD9vlJ8tykqdDfbKI+qiY2PzLpEqRbaPyZA7xKuZsj8SsFPOdcj2aPlcKXg04HRnzaq5H8c+9TCQWQ+P6RvPkFVdkBygFVSiXG/CU=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 5797366A3; Thu, 14 Apr 2016 18:55:02 +0900 (JST) Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) From: Jacques Garrigue In-Reply-To: Date: Thu, 14 Apr 2016 18:56:47 +0900 Cc: OCaML List Mailing Content-Transfer-Encoding: quoted-printable Message-Id: <94AF08A8-C9A5-4D0A-B8A4-4C27DA4F8C9B@math.nagoya-u.ac.jp> References: To: =?utf-8?Q?Milan_Stanojevi=C4=87?= X-Mailer: Apple Mail (2.3124) Subject: Re: [Caml-list] variance/injectivity/uniqueness annotations for types On 2016/03/11 15:53, Milan Stanojevi=C4=87 wrote: >=20 > I ran into some variance/injectivty issues in my code, plus I saw some > recent question here, and I was wondering if there was any progress on > adding syntax so types can be annotated with proper information (as > discussed in http://caml.inria.fr/mantis/view.php?id=3D5985). >=20 > I guess we don't really need new syntax, we can just use attributes > (e.g. [@@unique] or [@@injective]) >=20 > I searched mantis a bit but I don't see anything new (maybe I didn't > search hard enough). The situation seems to be stuck currently, waiting for concrete examples where this is really needed, and also for a good syntax. Indeed, in other discussions, there seemed to be an agreement that attributes were not very good for changing the type system itself, as they are somehow outside of the language. Moreover, injectivity would be rather heavy, as this is a per-parameter property. Concerning uniqueness, Alain Frisch made some interesting suggestion of using a global name or path to make types distinguishable. Jacques Garrigue=