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 8D8E77EE9C for ; Fri, 25 Nov 2016 14:47:22 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gabriel.scherer@gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer@gmail.com; spf=None smtp.helo=postmaster@mail-io0-f174.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.223.174; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.223.174 as permitted sender) identity=mailfrom; client-ip=209.85.223.174; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@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-io0-f174.google.com) identity=helo; client-ip=209.85.223.174; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-io0-f174.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3ABgDbdhXiVGogpwTsLUOAL022fwHV8LGtZVwlr6E/?= =?us-ascii?q?grcLSJyIuqrYZhaGt8tkgFKBZ4jH8fUM07OQ6PG7Hzdaqsvb+DBaKdoXCE9D0Z?= =?us-ascii?q?1X1yUbQ+e7SmTDZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5y?= =?us-ascii?q?O/inUtWK15f//6mI9pbSewRFgiamKfM3dU3u7FaZis5Do5ZmK6s3gjHNpX1EM7?= =?us-ascii?q?BU2GdpKFTVlRL74MuY85tq8iAWsPUkoZ1uS6L/KosxR6ZZATBuCGs16dfmr1GX?= =?us-ascii?q?QgKF/HoRViMNmRpFGQXfxB7/V5b19CD9s7wui2GhIcTqQOVsCnyZ5KBxRUqt0X?= =?us-ascii?q?9fOg=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BKAAD8PzhYhq7fVdFeHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBgw0BAQEBAXdyEAeNPpcYlHSCCB0LhXkCgXEHPxQBAQEBAQEBAQE?= =?us-ascii?q?BARIBAQEICwsJHTCCMwQBFQEEghcBAQQBAg8RBBkBGx0BAwwGBQsNAgIjAwICI?= =?us-ascii?q?QEBEQEFAQsRBhMaCIgwAQMXDp1OgTI/MotQgWwYBQEfgw0Fg1YKGScNVIM2AQE?= =?us-ascii?q?BAQEBAQECAQEBAQEBGQIBBRJ5hTOEW4JIhQWCXQWPbYoyNYF2hFKGaINWkDKJQ?= =?us-ascii?q?IQxgkgTHoETHoEsQBGDFyCCBiA0AYZngU8BAQE?= X-IPAS-Result: =?us-ascii?q?A0BKAAD8PzhYhq7fVdFeHAEBBAEBCgEBFwEBBAEBCgEBgw0?= =?us-ascii?q?BAQEBAXdyEAeNPpcYlHSCCB0LhXkCgXEHPxQBAQEBAQEBAQEBARIBAQEICwsJH?= =?us-ascii?q?TCCMwQBFQEEghcBAQQBAg8RBBkBGx0BAwwGBQsNAgIjAwICIQEBEQEFAQsRBhM?= =?us-ascii?q?aCIgwAQMXDp1OgTI/MotQgWwYBQEfgw0Fg1YKGScNVIM2AQEBAQEBAQECAQEBA?= =?us-ascii?q?QEBGQIBBRJ5hTOEW4JIhQWCXQWPbYoyNYF2hFKGaINWkDKJQIQxgkgTHoETHoE?= =?us-ascii?q?sQBGDFyCCBiA0AYZngU8BAQE?= X-IronPort-AV: E=Sophos;i="5.31,547,1473112800"; d="scan'208";a="246713722" Received: from mail-io0-f174.google.com ([209.85.223.174]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 25 Nov 2016 14:47:21 +0100 Received: by mail-io0-f174.google.com with SMTP id c21so120928243ioj.1 for ; Fri, 25 Nov 2016 05:47:21 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=40GZ2WVGAztgaom34dTRC72CZEUrkbYQXCfM3BwOjGU=; b=fz8IviElPQqDQQKmjV97Jn0MwCekEnIQi6pHrNzGycFXzzos93zxauqekXyYYbfWLm 7PN6C80DButEewRV1rslLBwmhj8qBxX2XIRg+5QBY0JTMyvIN2p1VHh/qZmdt+4YL7Rj 7BFPtOOxlBnxalY1l+8WPgKZsWqWIxa185a6QJ1HDax/5I/ulyaPTuMcvsq2E9QTaRu/ E0J5ShEdikmUMfSgr2zMl52SlEiFX6BLqe6uzyge6MIi7cogIKTVaL1csUyxAT5qaLrN wTAt9kP1TeehtWSpyfoQL3uQ28xu2/arrwoGhohbGP4RaVaYVlQogDg1dAxtoq+Xldcf 7KyQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc; bh=40GZ2WVGAztgaom34dTRC72CZEUrkbYQXCfM3BwOjGU=; b=AUATX+BuJW1Ara3belpwakN2Vn8lIZ0m4GbG1kDqHeHOY6rNWxU3CH9qW94b5frreV LTHEMLIpz5U+TuCFGnnWP5/KD0GtMSk3y2MJDbLq2r8U18A5lpXq25FjD5FVLLp0XOLB iaAYqZRqIvaEHU7jgl+FBXH/f5niJNRGNgvCUmgqYywK8wTxcoThCZv7BWqdtVnYRQps gfX+0W8v8lFsxGHKmBlfmokMlSMWOm3KlyjaxnTSz1kgECk46V+utbkdJZqx+D20AO18 yylMc0dlpXxql0g2/U62C9xstFa9yOgZU6ugkARaoX2YL2CVnvpk8DQRFpzo53hFg4vP QSbQ== X-Gm-Message-State: AKaTC02DvdQv+a7q4+ofyWqG+wIyZsaHnAAYMNJKpFVIqhr/LTuhSDp2SIJDsGNHnKp4l4yUzCFgyWkku9Q2jQ== X-Received: by 10.36.215.70 with SMTP id y67mr7059222itg.16.1480081640320; Fri, 25 Nov 2016 05:47:20 -0800 (PST) MIME-Version: 1.0 Received: by 10.79.18.131 with HTTP; Fri, 25 Nov 2016 05:46:39 -0800 (PST) In-Reply-To: References: From: Gabriel Scherer Date: Fri, 25 Nov 2016 08:46:39 -0500 Message-ID: To: Julien Blond Cc: David Allsopp , OCaml mailing-list Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] Empty polymorphic variant set I would agree that OCaml lacks a convenient way to define the empty type. (It used to be possible using the revised syntax, which uses braces to delimit (non-polymorphic) variant definitions, but this was ruled out by sanity checks introduced in OCaml 4.02). One way is to use GADTs to create an impossible type: type 'a onlybool = Bool : bool onlybool type empty = int onlybool let extract : ('a, empty) result -> 'a = function Ok x -> x Since 4.03 (April 2016), it is possible to explicitly write a so-called "refutation case", of the form " -> .", to say that a given case cannot happen -- it is an error if the type-checker cannot verify it: https://caml.inria.fr/pub/docs/manual-ocaml/extn.html#sec241 let extract : ('a, empty) result -> 'a = function | Ok x -> x | Error _ -> . I would support the idea of having a built-in "empty" type to represent a variant type with no constructor -- but then I am probably biased in favor of the empty type. On Fri, Nov 25, 2016 at 8:01 AM, Julien Blond wrote: > Yes, i knew the variant constructor but, somehow i didn't realize i was > precisely using it for my mind was focused on the polymorphic variant list > :) > > In fact, i wondered if a generic result type like this > > type ('a, 'b) result = Ok of 'a | Error of 'b > > that we can see in several library could be used to specify a "safe" result > which could have type something like ('a, []) result. One could encode 'b as > some error list at type level but it needs some complicated type management > and i'm targeting OCaml beginners for which i just want them to be careful > about non nominal results. > > > 2016-11-25 12:22 GMT+01:00 David Allsopp : >> >> Julien Blond wrote: >> > 2016-11-25 9:39 GMT+01:00 Julien Blond : >> > Hi, >> > Let's try something : >> > $ ocaml >> > OCaml version 4.03.0 >> > >> > # let _ : [] list = [];; >> > Characters 9-10: >> > let _ : [] list = [];; >> > Error: Syntax error >> > # type empty = [];; >> > type empty = [] >> > # let _ : empty list = [];; >> > - : empty list = [] >> > # >> > >> > Does anyone know if there is a reason to forbid the empty polymorphic >> > variant >> > set in type expressions or if it's a bug ? >> >> As you've observed, [] is a variant constructor since 4.03.0 - see GPR#234 >> (https://github.com/ocaml/ocaml/pull/234). The GPR contains references and >> comments as to the motivation for this. >> >> What's your desired use for the type of the non-extensible empty >> polymorphic variant? >> >> Possibly related, you can define a general type for a list of polymorphic >> variants: >> >> let (empty : [> ] list) = [] >> >> or >> >> let (length : [> ] list -> int) = List.length;; >> length [`Foo; `Bar];; >> length [42];; >> >> if that's what you were after? >> >> >> David > >