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 12BA27F0A6 for ; Thu, 20 Aug 2015 16:12:02 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of kennethadammiller@gmail.com) identity=pra; client-ip=209.85.218.42; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="kennethadammiller@gmail.com"; x-sender="kennethadammiller@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of kennethadammiller@gmail.com designates 209.85.218.42 as permitted sender) identity=mailfrom; client-ip=209.85.218.42; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="kennethadammiller@gmail.com"; x-sender="kennethadammiller@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-oi0-f42.google.com) identity=helo; client-ip=209.85.218.42; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="kennethadammiller@gmail.com"; x-sender="postmaster@mail-oi0-f42.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0D/AAAO39VVmyraVdFdg29pBoMfvCgBCYV7AoEsB0wBAQEBAQESAQEBAQEGCwsJIS6EIwEBAQMBAQIPEQQZARsdAQMBCwYFCwMKKgICIQEBEQEFARwGExoIh3YBAwoIDawGgS8+MYtAgWyCeYptChknDVeFAAEBAQEBAQEDAQEBAQEBAQEUAQEEDotFgk+CNwQHgmmBQwWVKYUFhX2BbYFKkEB5g0+CHRIjgRcXgh0cgW8iM4JMAQEB X-IPAS-Result: A0D/AAAO39VVmyraVdFdg29pBoMfvCgBCYV7AoEsB0wBAQEBAQESAQEBAQEGCwsJIS6EIwEBAQMBAQIPEQQZARsdAQMBCwYFCwMKKgICIQEBEQEFARwGExoIh3YBAwoIDawGgS8+MYtAgWyCeYptChknDVeFAAEBAQEBAQEDAQEBAQEBAQEUAQEEDotFgk+CNwQHgmmBQwWVKYUFhX2BbYFKkEB5g0+CHRIjgRcXgh0cgW8iM4JMAQEB X-IronPort-AV: E=Sophos;i="5.15,714,1432591200"; d="scan'208";a="174316393" Received: from mail-oi0-f42.google.com ([209.85.218.42]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 20 Aug 2015 16:12:01 +0200 Received: by oiew67 with SMTP id w67so23320814oie.2 for ; Thu, 20 Aug 2015 07:12:00 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; bh=5eeKw2IKkAskOhKx1tjtIvthdhhqU1Xo3E9p0aGLGRg=; b=FuuJ6Vk2YrusP/FupYG2vixdISScM9nJEHb2Y2BQ6dqg12vQw8ggHEzoKWXzB2AKYN 9St8Tg65VmeR9MFFQJReYtRMqm/XXuZCQILXoWwZtqQA7RVU6TJyMpMlCykNJtXbGJNq Z8tPQpS2r2owfp/diur8joJQsu6v9oI0HvvIpO5zSHq3R1MIhyOn9OC7Ghc55yYnycOb GgxbWfwoRA+pU+M309Z612KxDW1EePxezCPhYN4JOtPopegZTavuDdd6ijxg3/750KEW nUbHYIs5uhORxz481NG9p8afePtQX7Bzw8HFBdT7zf0FFRuzcRnGt1M9A1J6d7wg+Txj 9NPQ== MIME-Version: 1.0 X-Received: by 10.202.81.12 with SMTP id f12mr2620098oib.130.1440079920004; Thu, 20 Aug 2015 07:12:00 -0700 (PDT) Received: by 10.202.191.8 with HTTP; Thu, 20 Aug 2015 07:11:59 -0700 (PDT) In-Reply-To: References: <20150818185751.GC650@topoi.pooq.com> <20150820091051.GA15458@frosties> Date: Thu, 20 Aug 2015 10:11:59 -0400 Message-ID: From: Kenneth Adam Miller To: David Allsopp Cc: Goswin von Brederlow , caml users Content-Type: multipart/alternative; boundary=001a113d7f1214846e051dbebc05 Subject: Re: [Caml-list] Type Encoding Format Control --001a113d7f1214846e051dbebc05 Content-Type: text/plain; charset=UTF-8 One of the things I had also thought about expressing also is about automatically collapsing such a type instance as part of it's definition with other annotations, but that's complicated and likely a different topic so I didn't mention it. On Thu, Aug 20, 2015 at 10:09 AM, Kenneth Adam Miller < kennethadammiller@gmail.com> wrote: > It expresses intuitively, "Something which is exactly a nothing", so > naturally, I would categorize that as a nothing directly of course. And > you've just done precisely that with your code; foo = Some None => set that > field to NULL could only represent saying that field is just exactly > nothing directly. So, it's just like I said-you have to deal with the > instance because it comes up in practice, and pragmatically we have to > represent such cases in machine code as has been discussed. But in > practicality almost never would an author sensibly keep the expanded form > of Some None directly, it shows up due to code combinations only to be > reduced. > > On Thu, Aug 20, 2015 at 10:05 AM, David Allsopp > wrote: > >> Kenneth Adam Miller wrote: >> > In the case of 2), that's interesting because such a type of >> > Some None is sort of antithetical to describing anything >> > sensical. Not that it's not pragmatic or doesn't occur-I'm sure >> > some functions get combined in ways that stuff like this crops >> > up. But I think of the typing system as being badly exercised >> > if something like this arises- >> >> One example that springs immediately to mind: NULLable field in a >> database, so 'a option is a sensible type to represent it. Now consider a >> function intended to generate SQL UPDATE statements for that field: >> >> val update_record : ?foo:int option -> ?bar:int option -> id:int -> >> baz:string -> bool >> >> where omitting ~foo or ~bar means "don't change foo/bar in the UPDATE >> statement". Within the code for update_record: >> >> foo = None => don't update that field >> foo = Some None => set that field to NULL >> foo = Some (Some i) => set that field's value to i >> >> and all three cases will need different code. >> >> See also https://github.com/ocaml/ocaml/blob/trunk/typing/env.ml#L391 >> >> What's (to you) badly exercised or nonsensical in either of those >> representations? >> >> >> David >> > > --001a113d7f1214846e051dbebc05 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
One of the things I had also thought about expressing also= is about automatically collapsing such a type instance as part of it's= definition with other annotations, but that's complicated and likely a= different topic so I didn't mention it.

On Thu, Aug 20, 2015 at 10:09 AM, Kenneth = Adam Miller <kennethadammiller@gmail.com> wrote:
It expresses intuitively,= "Something which is exactly a nothing", so naturally, I would ca= tegorize that as a nothing directly of course. And you've just done pre= cisely that with your code; foo =3D Some None =3D> set that field to NUL= L could only represent saying that field is just exactly nothing directly. = So, it's just like I said-you have to deal with the instance because it= comes up in practice, and pragmatically we have to represent such cases in= machine code as has been discussed. But in practicality almost never would= an author sensibly keep the expanded form of Some None directly, it shows = up due to code combinations only to be reduced.=C2=A0

On Thu, Aug 20, 2015 at 10:05 AM, David Allsopp &l= t;dra-news@meta= stack.com> wrote:
Ke= nneth Adam Miller wrote:
> In the case of 2), that's interesting because such a type of
> Some None is sort of antithetical to describing anything
> sensical. Not that it's not pragmatic or doesn't occur-I'm= sure
> some functions get combined in ways that stuff like this crops
> up. But I think of the typing system as being badly exercised
> if something like this arises-

One example that springs immediately to mind: NULLable field in a da= tabase, so 'a option is a sensible type to represent it. Now consider a= function intended to generate SQL UPDATE statements for that field:

val update_record : ?foo:int option -> ?bar:int option -> id:int ->= ; baz:string -> bool

where omitting ~foo or ~bar means "don't change foo/bar in the UPD= ATE statement". Within the code for update_record:

foo =3D None =3D> don't update that field
foo =3D Some None =3D> set that field to NULL
foo =3D Some (Some i) =3D> set that field's value to i

and all three cases will need different code.

See also https://github.com/ocaml/ocaml/= blob/trunk/typing/env.ml#L391

What's (to you) badly exercised or nonsensical in either of those repre= sentations?


David


--001a113d7f1214846e051dbebc05--