From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 0BB5CE01D2 for ; Mon, 4 Jan 2021 13:43:18 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=matthew@o1labs.org; spf=Pass smtp.mailfrom=matthew@o1labs.org; spf=None smtp.helo=postmaster@mail-wm1-f46.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of matthew@o1labs.org) identity=pra; client-ip=209.85.128.46; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="matthew@o1labs.org"; x-sender="matthew@o1labs.org"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of matthew@o1labs.org designates 209.85.128.46 as permitted sender) identity=mailfrom; client-ip=209.85.128.46; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="matthew@o1labs.org"; x-sender="matthew@o1labs.org"; 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-wm1-f46.google.com) identity=helo; client-ip=209.85.128.46; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="matthew@o1labs.org"; x-sender="postmaster@mail-wm1-f46.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3ARs/DjBEvltNfhGsSofuGz51GYnF86YWxBRYc798d?= =?us-ascii?q?s5kLTJ7yp8+wAkXT6L1XgUPTWs2DsrQY0rWQ6fu7EjBYqb+681k6OKRWUBEEjc?= =?us-ascii?q?hE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRo?= =?us-ascii?q?LerpBIHSk9631+ev8JHPfglEnjWwba5wIRmsswncuMcbjYRtJ6ot1xDEvmZGd+?= =?us-ascii?q?NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLD?= =?us-ascii?q?TRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljj?= =?us-ascii?q?oMOiUn+2/LlMN/kKNboAqgpxNhxY7UfJqVP+d6cq/EYN8WWXZNUsNXWidcAI2z?= =?us-ascii?q?cpEPAvIOMuZWrYbzp1UAoxijCweyGOzi0SVHimPs0KAgz+gtDQPL0Qo9FNwOqn?= =?us-ascii?q?TUq9D1Ob8VX++v0KnI0TXDYO1Y2Dzg9IbJcgouofeRVr93dMre01UvFx/FjlqO?= =?us-ascii?q?p43oJDSV2vkJs2eB9OVgTviji2k9qwF+uzWiwNonhYbViIwP0F/E6Tl5z5gvJd?= =?us-ascii?q?2+UEN2ZcCoHpVMui2GKod6Xt4uTm5rtSg6ybAKpZG1cSkExZko2hPSdfOJfoyU?= =?us-ascii?q?7h/hVuufLip1iXFldr+whBu+71Wtx+vhXce611ZKqzBKktjKtn0V1hzT7NKHSv?= =?us-ascii?q?pn8Uu71zaPzRjf6u5FIUAolarbNoUuzqQsmZoUtETOGDL9lkbujKKOaEko5uyl?= =?us-ascii?q?5/7kb7jmvJOQKpF4hwLkPqkhm8GyB/kzPBIUUGiB4+u80aXu/U3nT7VOif07iq?= =?us-ascii?q?zZv4rbJcQfv6K4DQpV3ps65xaxADqr0c4UnXYALFJCdxKHi5bmN0vSL/D/CPez?= =?us-ascii?q?m1WskDF1yPDaJrDtHInBI3zZnLrifbtx8VNQxBQwwNxF6J9ZC6kNIPfpVU/wsN?= =?us-ascii?q?zYAAU5Mwuxw+v/DdVyzJ8eWX6PAqCHPqLfqliI6v8rI+aWf4AVoyzxK/8/5/7h?= =?us-ascii?q?lXM5g0MSfbG13ZsLb3C1BuhpLF+cYXrom9sBFWYKvhEiTOHxk12DUTtTZ26oUK?= =?us-ascii?q?4m5zE7DpimDYbZSYy3jryBxnTzIpoDQ2lcCU2XWVrseZ+FXfhEPAebOMx8iXop?= =?us-ascii?q?Uba7Soku/Q6jvkn2xuw0APDT/3g9vI7/1NVqr9fCnBd6oTl9E9id3n6lSDhwl2?= =?us-ascii?q?kTATgs0/Ys8gRG1l6f3P0g0LRjHttJ6qYMC19ibMOO/6lBE9n3Hzn5UJKJRVKh?= =?us-ascii?q?GIj0BDgwSpcuxoZLbRojXdqliR/H0myhBLpHz+XXVqxxybrV2j3KH+g402zPjf?= =?us-ascii?q?NziAAiS8FUc2q8ifwnrlmBN8vyi0yc0p2SW+EZ1S/J+n2EyDPU7kYBVAd6SuPC?= =?us-ascii?q?R39NP0Y=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DAAQA6DPNffy6AVdFihXlXMy6EP4Eek?= =?us-ascii?q?BEDlBuIHAsBAwENIwwEAQGBVYJ1AoFvAh0HAQQ0EwIQAQEFAQEBAgEDAwQBEwE?= =?us-ascii?q?BDQsLCCeFagyCOCkBgxEBAQEDARIRBBkBASwLAQQLCwsNKgICIhIBBQEcBhMig?= =?us-ascii?q?wQBglUDDiAPomOBBD2KPnZ/MxMBgnABAQaBMwEDAoNJIk2BOQMGEoEmhWESPIZ?= =?us-ascii?q?6JhuCAIERNoI1Lj6CXQKCDIJrgj4ighUzLlEHBRQQCIFJGR1Ij08dpyqBEYMAg?= =?us-ascii?q?RyHBYEJki4igSKCB4orlHydJIF3kU8EHIRNECOBSoF6MxoIKAg7MQaBfgEBMlA?= =?us-ascii?q?ZDY5YgzqBPoNWhUREMDcCBgEJAQEDCY4aAQE?= X-IPAS-Result: =?us-ascii?q?A0DAAQA6DPNffy6AVdFihXlXMy6EP4EekBEDlBuIHAsBAwE?= =?us-ascii?q?NIwwEAQGBVYJ1AoFvAh0HAQQ0EwIQAQEFAQEBAgEDAwQBEwEBDQsLCCeFagyCO?= =?us-ascii?q?CkBgxEBAQEDARIRBBkBASwLAQQLCwsNKgICIhIBBQEcBhMigwQBglUDDiAPomO?= =?us-ascii?q?BBD2KPnZ/MxMBgnABAQaBMwEDAoNJIk2BOQMGEoEmhWESPIZ6JhuCAIERNoI1L?= =?us-ascii?q?j6CXQKCDIJrgj4ighUzLlEHBRQQCIFJGR1Ij08dpyqBEYMAgRyHBYEJki4igSK?= =?us-ascii?q?CB4orlHydJIF3kU8EHIRNECOBSoF6MxoIKAg7MQaBfgEBMlAZDY5YgzqBPoNWh?= =?us-ascii?q?UREMDcCBgEJAQEDCY4aAQE?= X-IronPort-AV: E=Sophos;i="5.78,474,1599516000"; d="scan'208,217";a="485281053" X-MGA-submission: =?us-ascii?q?MDFPyYHwjjcCEPa490oT4p3C5a6eSjvw/SBMOy?= =?us-ascii?q?XZQr5FkrlQbUAU0XZ0ya5tfDDUObkd7V/LAhlPwnZxi8w98lvs+t+OiK?= =?us-ascii?q?xaBUzP0wE+vlNoeXuHdE0zdn6S0UYmjgMtrAaR5+qNiKRAeZ1cbIOs0p?= =?us-ascii?q?uM8gA1FgMSjR3OjlFpp7VU9A=3D=3D?= Received: from mail-wm1-f46.google.com ([209.85.128.46]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES256-GCM-SHA384; 04 Jan 2021 13:43:16 +0100 Received: by mail-wm1-f46.google.com with SMTP id 3so19163307wmg.4 for ; Mon, 04 Jan 2021 04:43:16 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=o1labs.org; s=google; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=DYzCR58bL4vf1rx9823/mMBFysOv7AxxKRkfemm4+mM=; b=IRebG0bs68mN6izjpxuwgQG2xz94vIBDHpEFj6Tigwsp0phJd9bdKuNUe9liGgLi/o jOrFGp21NCwR2pzrzCb2oHDMJSVELHTWauiG8wCvsHxWjNvmIebIGbLscMmMBOo1fUM/ RNhKfazzuRrVR2sgvOTZfXe8PEk+nDGCAdb9Dj6Uart+K1SyIjoEQ6Ujj1LVaCQdAIf+ 2nfrX53a8OHe6hNAC99acnBS3+2rgM+Nf2JoUwvyQa9qtIcPjtc2TryWaVkKxnVmd+Wa NuRZ8FsJgYtJdzont50bnSbU1cbKrYrHIo/co90jiKkypOkspC2haMB1jf2z1L5+Oj9W irhA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc; bh=DYzCR58bL4vf1rx9823/mMBFysOv7AxxKRkfemm4+mM=; b=QXX+7isX2qF8VDNZLR3rvj61LROZKQyW+0Tf9f/mVaJGErM4ncfglKK6yTb0+9MmF7 qmqjQVHPPLWxZWm53+NOqXVsfZRUrgYgQiZBIZtIg2iZ2G0fxHukzsDHvzmtz3mA7rFn YMUqwmRr6a5hgbqsuxnLIZ1gO+BJpRwLxJ5uKY4h6Dn6m8lF+UF+CsZ7rLcwC1gTzjDl Ab536o2vlDEKog5QlVdjV83binRogOumQzLpFH+mjsPXi+Bguj3ozvNmx9fgTS8WHyxT VJFAWTlJaUsenqzwoGxJk0gUAaEvXYazp7OB3Wj2El+y6wu18f2mjtjJPSNshv9++24s SWsA== X-Gm-Message-State: AOAM531Zae0iNjWIiZ8vcDr2skSKiVhe3caRjohveBGuO7wHuwrIryV5 uYExU/osw/Lz1q5d8TenbjQr4D6NsE6RUF8SKXK7EpBn4HU= X-Google-Smtp-Source: ABdhPJyybTs3usNiim5p/i0koVTL+cQ963EKrc4A22/fM1ZaovslUx1sFl4uf3Y2JLQDCW7gg5bGvtDcqBk5MsUd3SE= X-Received: by 2002:a05:600c:2188:: with SMTP id e8mr27013179wme.182.1609764196512; Mon, 04 Jan 2021 04:43:16 -0800 (PST) MIME-Version: 1.0 References: <9315a69b-5512-7968-2804-785add2d14ea@web.de> In-Reply-To: <9315a69b-5512-7968-2804-785add2d14ea@web.de> From: Matthew Ryan Date: Mon, 4 Jan 2021 12:43:05 +0000 Message-ID: To: Markus Elfring Cc: caml users Content-Type: multipart/alternative; boundary="0000000000001b099d05b8126fcd" Subject: Re: [Caml-list] Documentation challenges for the application of comparison functions --0000000000001b099d05b8126fcd Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable It's not equivalent per se, since you lose the flexibility to call the function with e.g. let find_float_int ~(cmp : float -> int -> int) (index : float) (map : (int, 'c)) =3D find ~cmp index map;; where 'a =3D float and 'b =3D int. However, it is valid -- and arguably describes the function's contract better -- to narrow the function's type by combining the type variables: let find : cmp:('a -> 'a -> int) -> 'a -> ('a, 'b) t =3D find;; > It would have been nice if this information can be shared also by the mailing list. Apologies, I misclicked reply instead of reply-all. I have copied the list on this reply, with the earlier messages quoted below. > Would you get into the mood to add comments for any further evolution according to affected software libraries? I'm happy to discuss or comment on any proposals you have. Please feel free to tag me @mrmr1993 on GitHub if there are relevant conversations there. Regards, Matthew On Sun, 3 Jan 2021, 15:26 Markus Elfring, wrote: > > For backwards-compatibility reasons, this over-general type is unlikely > to change, and the compiler has no way otherwise to infer that the ~cmp > argument represents a comparison. Modifying the definition to > > > > let rec find ~(cmp : 'a -> 'a -> int) x =3D ... > > Is it really equivalent to replace the automatically determined type =E2= =80=9C'b=E2=80=9D > by the type annotation =E2=80=9C'a=E2=80=9D? > > (I assume that it can occasionally be more important to distinguish > between the specified letters.) > > > > val find : {C : Comparable} ->C.t -> (C.t, 'a) t -> 'a > > > > I hope this helps, or is at least informative. > > Thanks for such constructive feedback. > > It would have been nice if this information can be shared also by the > mailing list. > https://sympa.inria.fr/sympa/arc/caml-list/2021-01/ > > > Would you get into the mood to add comments for any further evolution > according to > affected software libraries? > > Example: > https://github.com/elfring/OTCL/ > > Regards, > Markus > > On Sun, 3 Jan 2021, 07:54 Matthew Ryan, wrote: > > Hello Markus, > > OCaml infers the most general type for an expression. For example, > > let rec fold_left acc xs ~f =3D > match xs with > | [] -> acc > | x :: xs -> f acc x > > will infer the type > > val fold_left : 'a -> 'b list -> f:('a -> 'b -> 'a) -> 'a > > where the distinct types for the accumulator and list elements are > inherently more powerful than if they were unified. > > For identifying comparison functions, it could be argued that the type of > Stdlib.compare is over-general, and perhaps should be > > type comparison_result =3D Lt | Eq | Gt > > val compare : 'a -> 'a -> comparison_result > > For backwards-compatibility reasons, this over-general type is unlikely t= o > change, and the compiler has no way otherwise to infer that the ~cmp > argument represents a comparison. Modifying the definition to > > let rec find ~(cmp : 'a -> 'a -> int) x =3D ... > > and using the heuristic that 'a -> 'a -> int is likely a comparison is > probably the easiest way to proceed for now. > > There is a proposal for modular implicits (and a proposed pull request fo= r > modular explicits) which may make it easier to infer this in the distant > future. The syntax there is approximately > > module type Comparable =3D sig > type t > val compare : t -> t -> int > end > > let rec find {C : Comparable} (x : C.t) =3D ... > > val find : {C : Comparable} ->C.t -> (C.t, 'a) t -> 'a > > I hope this helps, or is at least informative. > > Regards, > Matthew > > On Sat, 2 Jan 2021, 15:42 Markus Elfring, wrote: > > Hello, > > I have taken another look at a few functions of a software library > where comparison functions should be passed. > > =E2=80=A6 > let rec find ~cmp x =3D function > Empty -> raise Not_found > | =E2=80=A6 > > let not_found_default_action ~value ?compare:(cmp=3DStdlib.compare) =3D > raise Not_found > =E2=80=A6 > > > Interface descriptions can be generated then in a known format for OCaml > 4.11.1. > > =E2=80=A6 > val find : cmp:('a -> 'b -> int) -> 'a -> ('b, 'c) t -> 'c > val not_found_default_action : value:'a -> ?compare:('b -> 'b -> int) -> = 'c > =E2=80=A6 > > > Now I find two details interesting for further clarification. > > 1. The first reference for a comparison function seems to express a need > for > different data types =E2=80=9C'a=E2=80=9D and =E2=80=9C'b=E2=80=9D whi= le a single type might be > sufficient > for the comparison function according to the second function. > > 2. The specification of =E2=80=9CStdlib.compare=E2=80=9D looks clear acco= rding to the > semantics > for a default parameter in a ML source file while the OCaml arrow > representation > can look more challenging. > How would you recognise that such a function parameter should be appli= ed > for comparison calls? > > Regards, > Markus > > --0000000000001b099d05b8126fcd Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
It's not equivalent per se, since y= ou lose the flexibility to call the function with e.g.

let find_float_int ~(cmp : float -> i= nt -> int) (index : float) (map : (int, 'c)) =3D
=C2=A0 find ~cmp index map;;

where 'a =3D float and 'b =3D int. However, it is valid -= - and arguably describes the function's contract better -- to narrow th= e function's type by combining the type variables:

let find : cmp:('a -> 'a -> in= t) -> 'a -> ('a, 'b) t =3D find;;
=
>=C2=A0It would have been nice if this information can be shared also by the mai= ling list.

Apologies, I misclicked reply instead of reply-all. I have copied the l= ist on this reply, with the earlier messages quoted below.

>=C2=A0Would you get into the mood to add comment= s for any further evolution according to
affected software libraries?

I'm happy to discuss or comment on any proposals you have. Pleas= e feel free to tag me @mrmr1993 on GitHub if there are relevant conversatio= ns there.

Regards,
Matthew

On Sun, 3 Jan 2021, 15:26 Markus Elfring, <Markus.Elfring@w= eb.de> wrote:
> For backw= ards-compatibility reasons, this over-general type is unlikely to change, a= nd the compiler has no way otherwise to infer that the ~cmp argument repres= ents a comparison. Modifying the definition to
>
> let rec find ~(cmp : 'a -> 'a -> int) x =3D ...

Is it really equivalent to replace the automatically determined type =E2=80= =9C'b=E2=80=9D
by the type annotation =E2=80=9C'a=E2=80=9D?

(I assume that it can occasionally be more important to distinguish
between the specified letters.)


> val find : {C : Comparable} ->C.t -> (C.t, 'a) t -> '= a
>
> I hope this helps, or is at least informative.

Thanks for such constructive feedback.

It would have been nice if this information can be shared also by the maili= ng list.
https://sympa.inria.fr/symp= a/arc/caml-list/2021-01/


Would you get into the mood to add comments for any further evolution accor= ding to
affected software libraries?

Example:
https://github.com/elfring/OTCL/

Regards,
Markus

On Sun, = 3 Jan 2021, 07:54 Matthew Ryan, <m= atthew@o1labs.org> wrote:
Hello Markus,

OCaml infers the most general type for an ex= pression. For example,

l= et rec fold_left acc xs ~f =3D
=C2=A0 match xs with<= /div>
=C2=A0 | [] -> acc
=C2=A0 = | x :: xs -> f acc x

= will infer the type

val = fold_left : 'a -> 'b list -> f:('a -> 'b -> = 9;a) -> 'a

where = the distinct types for the accumulator and list elements are inherently mor= e powerful than if they were unified.

For identifying comparison functions, it could be argued that= the type of Stdlib.compare is over-general, and perhaps should be

type comparison_result =3D Lt | = Eq | Gt

val compare : &#= 39;a -> 'a -> comparison_result

=
For backwards-compatibility reasons, this over-general ty= pe is unlikely to change, and the compiler has no way otherwise to infer th= at the ~cmp argument represents a comparison. Modifying the definition to

let rec find ~(cmp : '= ;a -> 'a -> int) x =3D ...

<= div dir=3D"auto">and using the heuristic that 'a -> 'a -> int= is likely a comparison is probably the easiest way to proceed for now.

There is a proposal for mod= ular implicits (and a proposed pull request for modular explicits) which ma= y make it easier to infer this in the distant future. The syntax there is a= pproximately

module type= Comparable =3D sig
=C2=A0 type t
=C2=A0 val compare : t -> t -> int
end

let rec find {C : Comparab= le} (x : C.t) =3D ...

va= l find : {C : Comparable} ->C.t -> (C.t, 'a) t -> 'a
=

I hope this helps, or is at l= east informative.

Regard= s,
Matthew

On Sat, 2 Jan 2021, 15:42 Markus= Elfring, <Markus.Elfring@web.d= e> wrote:
Hello,

I have = taken another look at a few functions of a software library
where compar= ison functions should be passed.

=E2=80=A6
let rec find ~cmp x = =3D function
=C2=A0 =C2=A0 Empty -> raise Not_found
=C2=A0 | =E2= =80=A6

let not_found_default_action ~value ?compare:(cmp=3DStdlib.co= mpare) =3D
=C2=A0 =C2=A0 raise Not_found
=E2=80=A6


Interfa= ce descriptions can be generated then in a known format for OCaml 4.11.1.
=E2=80=A6
val find : cmp:('a -> 'b -> int) -> = 9;a -> ('b, 'c) t -> 'c
val not_found_default_action := value:'a -> ?compare:('b -> 'b -> int) -> 'c=E2=80=A6


Now I find two details interesting for further clari= fication.

1. The first reference for a comparison function seems to = express a need for
=C2=A0 =C2=A0different data types =E2=80=9C'a=E2= =80=9D and =E2=80=9C'b=E2=80=9D while a single type might be sufficient=
=C2=A0 =C2=A0for the comparison function according to the second functi= on.

2. The specification of =E2=80=9CStdlib.compare=E2=80=9D looks c= lear according to the semantics
=C2=A0 =C2=A0for a default parameter in = a ML source file while the OCaml arrow representation
=C2=A0 =C2=A0can l= ook more challenging.
=C2=A0 =C2=A0How would you recognise that such a f= unction parameter should be applied
=C2=A0 =C2=A0for comparison calls?
Regards,
Markus
--0000000000001b099d05b8126fcd--