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 33C5B7EE51 for ; Sun, 28 Apr 2013 04:45:31 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of markus.mottl@gmail.com) identity=pra; client-ip=209.85.212.170; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="markus.mottl@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of markus.mottl@gmail.com designates 209.85.212.170 as permitted sender) identity=mailfrom; client-ip=209.85.212.170; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="markus.mottl@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-wi0-f170.google.com) identity=helo; client-ip=209.85.212.170; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="postmaster@mail-wi0-f170.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArEEAMCLfFHRVdSqk2dsb2JhbABTDoMvvj0EBAF4CBYOAQEBAQcLCwkUBCSCHwEBBAFAARQHHQEDAQsGBQsNLiEBAREBBQEcBhMIE4doAQMJBqFYjDGCfYNvChknDVmHXgEFDIw4glYHg08DlTqBZIwLgzoWKYN4WyA X-IPAS-Result: ArEEAMCLfFHRVdSqk2dsb2JhbABTDoMvvj0EBAF4CBYOAQEBAQcLCwkUBCSCHwEBBAFAARQHHQEDAQsGBQsNLiEBAREBBQEcBhMIE4doAQMJBqFYjDGCfYNvChknDVmHXgEFDIw4glYHg08DlTqBZIwLgzoWKYN4WyA X-IronPort-AV: E=Sophos;i="4.87,566,1363129200"; d="scan'208";a="15151677" Received: from mail-wi0-f170.google.com ([209.85.212.170]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 28 Apr 2013 04:45:30 +0200 Received: by mail-wi0-f170.google.com with SMTP id l13so1916023wie.5 for ; Sat, 27 Apr 2013 19:45:30 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:x-received:in-reply-to:references:date:message-id :subject:from:to:cc:content-type; bh=vufVYrl/NQQq9Njn35nNzaD5fgbmsAvQ/fMKqEr7SPA=; b=Cfm4PsDE6Qs5BRt3KMXgcIHyDNdGmN5m9YsjgHIQDuIdGGztoSfILwEpKEAh+tRclO ULFPQQmB0wL4YAtsUKiDUk5qNZ+f8WHRYF/DLuP7MiAn0VSO2nCBso+iLIYxKyvKmPJk V5mxBPWJvzqCcVIvTKFOeIt+WtXt585MwsLqTNSVDYlPp0kt9l7/e5+sQ5fbcfFtAmFF 5HYXvP6KqtuW1U+Qn6JJsi6sfacldxyn4L6rwY2Byd/D6msp2uGHtn2jBo1C8/kNycrt lXAZfRJiz7N9//12mgOM3HBFM1imbVqa8rnkDZ/5Go/iki1SPvXj0DnVTp4+Liwpiclp Kkew== MIME-Version: 1.0 X-Received: by 10.180.79.69 with SMTP id h5mr10939840wix.14.1367117130379; Sat, 27 Apr 2013 19:45:30 -0700 (PDT) Received: by 10.194.32.4 with HTTP; Sat, 27 Apr 2013 19:45:30 -0700 (PDT) In-Reply-To: <00C57DF0-C6F0-4EDE-8607-2155F3A17146@math.nagoya-u.ac.jp> References: <00C57DF0-C6F0-4EDE-8607-2155F3A17146@math.nagoya-u.ac.jp> Date: Sat, 27 Apr 2013 22:45:30 -0400 Message-ID: From: Markus Mottl To: Jacques Garrigue Cc: OCaML List Mailing Content-Type: text/plain; charset=ISO-8859-1 Subject: Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs On Sat, Apr 27, 2013 at 8:02 PM, Jacques Garrigue wrote: > The fix is simple enough: we should track injectivity, and assume that abstract > types are not injective by default. > However, this also means that the first type I defined above (using Hashtbl.t) > will be refused. If I understand your proposal correctly, the first type would only be refused unless the standard Hashtbl module were updated with appropriate injectivity annotations. The type variables in the GADT would not need any annotations, because it is assumed that they have to be injective there anyway for soundness. > How many of you are using GADTs in this way, and how dependent are you on > abstract types ? This seems like a "one percenter" problem. OTOH, I guess most people also rarely run into problems where variance annotations matter, but if they do, they have no option. The question should therefore rather be: what's the alternative? Are there workarounds? If not, annotations may just be a necessity to support advanced use cases. > If we need to be able to define GADTs relying on the injectivity of some abstract > types, a straightforward solution is to add injectivity annotations on type parameters, > the same way it was done for variance: > > type #'a t > > would mean that t is injective. Seems concise, but I'm just a little worried that we may be raising the bar for beginners again. The standard library would have to be updated with another annotation that may seem as obscure to beginners as variance annotations. I hope we'll never have to explain to a beginner the meaning of $%^&#-'a. Maybe a more verbose type constraint language would have been the better design choice here, but I guess we've already left this path with variance annotations. > If you are curious about other difficulties of GADTs, the is also branches/abstract-new > which introduces a notion of new types, either concrete or abstract, which are guaranteed > to be distinct from each other, and any other concrete type. This is useful when > checking the exhaustiveness of pattern-matching, as we can then discard impossible > branches. That branch is completely experimental. I haven't looked at this feature yet, but would this require even more annotations in the standard library? If so, maybe it would indeed be time to think about a more accessible syntax for type constraints. Regards, Markus -- Markus Mottl http://www.ocaml.info markus.mottl@gmail.com