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 c5ff346549e7 (Postfix) with ESMTP id 195585D5 for ; Wed, 8 Jan 2020 20:32:43 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.69,411,1571695200"; d="scan'208,217";a="430511910" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 08 Jan 2020 21:32:39 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id A91557F3CF; Wed, 8 Jan 2020 21:32:38 +0100 (CET) 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 1D89F7F214 for ; Wed, 8 Jan 2020 21:32:33 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ivg@ieee.org; spf=Pass smtp.mailfrom=ivg@ieee.org; spf=None smtp.helo=postmaster@mail-lj1-f180.google.com IronPort-PHdr: =?us-ascii?q?9a23=3AWt2sExGWYMz1VIzrQBUQPZ1GYnF86YWxBRYc798d?= =?us-ascii?q?s5kLTJ78pcuwAkXT6L1XgUPTWs2DsrQY0rGQ6f2wEjVbut6oizMrSNR0TRgLiM?= =?us-ascii?q?EbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVr?= =?us-ascii?q?O+/7BpDdj9it1+C15pbffxhEiCCybL9vIhi6txvdu8kVjIdtN6o8xBXEqWZUdu?= =?us-ascii?q?pLwm9lOUidlAvm6Meq+55j/SVQu/Y/+MNFTK73Yac2Q6FGATo/K2w669HluhfF?= =?us-ascii?q?TQuU+3sTSX4WnQZSAwjE9x71QJH8uTbnu+Vn2SmaOcr2Ta0oWTmn8qxmRgPkhD?= =?us-ascii?q?sBOjUk9mzcl85+g79BoB+5qBN/zYzbboGbOvR9Y63TY88VSHFbUcpNTSFMGJ+w?= =?us-ascii?q?Y5cNAucHIO1Wr5P9p1wLrRamBgesGvngyjlVjXH32q06z+MhER/a0wwgHtIOrG?= =?us-ascii?q?/Up8jyOacTT+C1w7LFzTTdYPxIxzjx8o/IcgouofyVW797bMTfyU4qFwzfj1WQ?= =?us-ascii?q?r5ToPzyU1uQRs2ib8vFvWfizhG4grgF8pCWkyMQ0ioTRmI4Z1lTJ+T96zYs1P9?= =?us-ascii?q?G0VlJ3bN2+HJdNtCyWK417Sd44TW5yoiY10LgGtIa7fCcUzJQnwAbSa/mdfIiJ?= =?us-ascii?q?5hLvTeKRITVliH58drKzmhW//VS6xu3zUcm011lKri5bndXWqn8N0BnT5tCGSv?= =?us-ascii?q?t74EihxS6C2x7P5uxAO0w5lqrWJ4Q/zrIslZcfq1nPEyzqlEnuia+ZbEQk+uym?= =?us-ascii?q?6+T9ZbXmo4eRN45qigHxKakum9KwDvomPQQUWGib4+u82KX5/ULlWLVKkuE2kq?= =?us-ascii?q?7BvZ/GP8sbo6q5DxZR0oYi8Ba/Eyyr0M8YnHkCNFJKYgiLj4nvO1HUIfD3F+2z?= =?us-ascii?q?g1q2kGQj+/eTJLzxD5nlLnHbiKblcK5h6kUazxA8nv5F4JcBK68IJrrcXVP2qt?= =?us-ascii?q?fYDwMie1i13enPCdhw28UZQ23ZUfzRC7/brVLdvrFnGOKLfoJA4G+gechg3Obn?= =?us-ascii?q?iDoCoXFYfaSt2sFJOnWxH/AjJ0fAJHS10o9HHmANsQ4zCuftjQ/aCGIBVzOJR6?= =?us-ascii?q?s5owoDJse+F46aHtKsjbGMmiChEc8OPzEUOhW3CX7tMr68dbIJYSOWLNVml2Vc?= =?us-ascii?q?B7msRoJn0guh5lb3?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0D6CAD4OhZehrTQVdFdCR0BAQEJAREFB?= =?us-ascii?q?QGBfAKDE4EHKoQJgRyNd4IRiW6PToF6CQEDAQwnCAEBhEACgWocBwEENgQNAhA?= =?us-ascii?q?BAQQBAQECAQIDBAETAQEBCAsLCCmFPgyCOyKDAQEBAQECARIRBBkBATcBBAsJA?= =?us-ascii?q?gsNKgICIhIBBQEcGRsHgwABglIFIA+QAo8OgQM9ijF1fzOCfgEBBYE1AYRTgTQ?= =?us-ascii?q?DBhKBJAGFHIZ8GoFBP4ERNoIvLj6CZAEBAoE3V4Jjgl6NSzCJbXeWTIJAhzaFP?= =?us-ascii?q?4ktG5pilyySKg8jgUgBgXd9CDsxBoI1UBgNig2DBRqDWYUUhV0mMAqQcQEB?= X-IPAS-Result: =?us-ascii?q?A0D6CAD4OhZehrTQVdFdCR0BAQEJAREFBQGBfAKDE4EHKoQ?= =?us-ascii?q?JgRyNd4IRiW6PToF6CQEDAQwnCAEBhEACgWocBwEENgQNAhABAQQBAQECAQIDB?= =?us-ascii?q?AETAQEBCAsLCCmFPgyCOyKDAQEBAQECARIRBBkBATcBBAsJAgsNKgICIhIBBQE?= =?us-ascii?q?cGRsHgwABglIFIA+QAo8OgQM9ijF1fzOCfgEBBYE1AYRTgTQDBhKBJAGFHIZ8G?= =?us-ascii?q?oFBP4ERNoIvLj6CZAEBAoE3V4Jjgl6NSzCJbXeWTIJAhzaFP4ktG5pilyySKg8?= =?us-ascii?q?jgUgBgXd9CDsxBoI1UBgNig2DBRqDWYUUhV0mMAqQcQEB?= X-IronPort-AV: E=Sophos;i="5.69,411,1571695200"; d="scan'208,217";a="430511870" X-MGA-submission: =?us-ascii?q?MDEHnBae+Aic0X2m391XTYYWASFLCfqo0gWX7A?= =?us-ascii?q?Szz28t48sj4i+6Y0W3qW5lkRPoM63qdaZ2YBsTRRt6cZoO4WIFORMVJc?= =?us-ascii?q?wODe/bYyBd+67aZGBZGvsy7OKRN+GTkgMasUy8cd2mZLHF/ioqSKtd1R?= =?us-ascii?q?V5LsDxwlYIKC/QQ4M/0OCfhA=3D=3D?= Received: from mail-lj1-f180.google.com ([209.85.208.180]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 08 Jan 2020 21:32:31 +0100 Received: by mail-lj1-f180.google.com with SMTP id u71so4679070lje.11 for ; Wed, 08 Jan 2020 12:32:31 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=ieee.org; s=google; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=q9jb+59menTqucb16xuGz1mtKl5z/04tEhK17ICooks=; b=b0wLrHRNRB/HMwSEchdF7QIP0LSAYpwey5zZOgBRl1XSo73YTj2Cw+h4NKCgzxBfQ9 d2gvG6wUcgDv9U1au27398XmzhAYd1mTwIy0+r4V583Jd9giWySnontig2SKlFSXQIED 7NRhujGmShA+mRR8FRjNs7ellEydZZgd1XU40= 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=q9jb+59menTqucb16xuGz1mtKl5z/04tEhK17ICooks=; b=ge51XWLF/pVvvk+zE5/E3xuR4PKBKFzHViSUgU4sI4nEklcshC8W8YpKegjdcuPd/t be0YgX5rms8W160dih/bsPQKIe5Qh6p4zO/A04bQiToymKlbzRK3a2dEkXQf/LI4AxB5 eBvBjldQX6f3hr7/dmM59IEq8wMu8mut+PIabaVDtjiBTws+BEu9IkGDFxOP3vBY6lOV G1POJCDBTHRKA+hU7/6AqMDlwJqVBP13oiQKFKJNgQsxVRiuPMSLlhbBoFUf1tsQbA+Z yI/lD72EO4TERvjAy1/0DYIru0YyvKqC72ILCd+YuNidLhwnSqHMOGgzjdBhzk8Q19T1 gYDw== X-Gm-Message-State: APjAAAXg/+AYMh/jQX2wz1rxcPe0Z9pTFmUewoMNclpUlIbuzGDZwxs4 lSufVWRiZZuhIsKf/Bcf3DsorSKwOnWUU6uGB6gZAwhCBu4= X-Google-Smtp-Source: APXvYqwV1eY6i13nKv74We5NPNXFL84OtxlubOk5dLY+6qLryh0k2aooQiKKLD1MdhdXT33zFFzSvxgdGWlyWp6aI/I= X-Received: by 2002:a2e:b4cb:: with SMTP id r11mr4040707ljm.68.1578515550366; Wed, 08 Jan 2020 12:32:30 -0800 (PST) MIME-Version: 1.0 References: <4d2b5367-a869-42bc-9547-b58864c10cf8@www.fastmail.com> <41592816-f82e-43a4-b67f-02e69623fe23@www.fastmail.com> In-Reply-To: <41592816-f82e-43a4-b67f-02e69623fe23@www.fastmail.com> From: Ivan Gotovchits Date: Wed, 8 Jan 2020 15:32:58 -0500 Message-ID: To: rixed@happyleptic.org Cc: caml-list Content-Type: multipart/alternative; boundary="000000000000a70eab059ba6ca44" Subject: Re: [Caml-list] Calling a single function on every member of a GADT? Reply-To: Ivan Gotovchits X-Loop: caml-list@inria.fr X-Sequence: 17937 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: --000000000000a70eab059ba6ca44 Content-Type: text/plain; charset="UTF-8" On Wed, Jan 8, 2020 at 1:54 AM wrote: > Hello and thank you for the answer. > > On Tue, Jan 7, 2020, at 21:21, Ivan Gotovchits wrote: > > It is the limitation of the let-bound polymorphism. (...) > > In your case, I would define a visitor type, e.g., > > type 'r visitor = {visit : 'a. 'a term -> 'r -> 'r} > > Oh I see. I've used this trick to force a function to be polymorphic, but > I failed to see that this was the problem because to me `f` is not any more > polymorphic when the `term` is a GADT than when it's not. > > So there is no lighter syntax to specify that `f` should accept any member > of a GADT than the syntax to specify that `f` should accept any type at all? > Only three methods of introducing rank-2 polymorphism are known to me: 1. records 2. objects 3. first-class modules Jacques has demonstrated the solution with objects, which might be a little bit more lightweight, at least as you don't need to define a new data type beforehand. But the invocation is more verbose and requires an annotation from the caller side, which could be confusing. The third solution relies on first-class modules and is even more verbose, at least on the definition side. Just for the sake of completeness, module type Visitor = sig type t val term : t -> 'a term -> t end let rec fold : type a r. r -> (module Visitor with type t = r) -> a term -> r = fun i ((module Visit) as f) t -> match t with | Int _ as t -> Visit.term i t | Add as t -> Visit.term i t | App (x,y) as t -> let i = fold i f x in let i = fold i f y in Visit.term i t let s = fold 0 (module struct type t = int let term x _ = x + 1 end) And again, it is not about GADT. GADT act as a red herring here. As I've demonstrated earlier, using a simple pair will suffice to display the limitation of the prenex polymorphism. Even no ADT is required, just apply one term to another two and you will get them unified, e.g., let f g x y : unit = g x; g y will have type val f : ('a -> unit) -> 'a -> 'a -> unit because 'a is quantified on the scope of `f` not `g`, in other words, it has type (not an OCaml syntax) val f : forall 'a. ('a -> unit) -> 'a -> 'a -> unit while we would like to have a type val f : forall 'b, 'c. (forall 'a. 'a -> unit) -> 'b -> 'c -> unit OCaml doesn't allow us to define types like `('a. 'a -> 'a)` and the reason is not that it is hard to extend the parser it is... I wonder, is this just a limitation of the OCaml parser or is there some > deep reason for these work-around (like is the case, from my understanding, > for the value restriction)? Yep, good catch! It is because of the impurity. Indeed, Haskell has the Rank2Types extension that lets us write types like `(forall a. a -> ()) -> b -> c -> ()`, with no extra syntactic burden (modulo having to provide the type annotation). But functions in Haskell are pure, therefore it is possible. To make the story short and obvious, let me do a simple demonstration of how things can go wrong in a language with side-effects. Let's go back to the simple example of pairs and the identity function. Consider the following nasty identity function, let bad_id () = let cache = ref None in fun x -> match cache.contents with | None -> cache := Some x; x | Some cache -> cache It has type `unit -> 'a -> 'a` therefore, if we would have the rank-1 polymorphism enabled for functions, we could apply it to the function let map2 : fun ('a. 'a -> 'a) -> 'b -> 'c -> 'b * 'c = fun f (x,y) -> f x, f y as let x,y : string * int = map2 (bad_id ()) "hello", 42 and will get a segmentation fault, as `y` will now have type int but hold a string. And here comes the syntax as a savior as it lets us specify functions that are guaranteed to be syntactic values. Indeed, all three solutions syntactically guarantee that the provided argument is a function, not a closure. Indeed, let's introduce the universal identity via a record, type id = { f : 'a. 'a -> 'a} and we can see that our `bad_id` is not accepted due to the value restriction, while good_id, defined as, let good_id x = x is perfectly fine, e.g., let id1 = {f = good_id} (*accepted *) let id2 = {f = bad_id} (* rejected *) moreover, even a fine, but not syntactic, identity is also rejected let fine_id () x = x let id3 = {f = fine_id ()} (* rejected *) with the message This field value has type 'b -> 'b which is less general than 'a. 'a -> 'a The same is true with modules, module type Id = sig val f : 'a -> 'a end module Id1 : Id = struct let f = good_id end (* accepted *) module Id2 : Id = struct let f = bad_id () end (* rejected *) module Id3 : Id = struct let f = fine_id () end (* rejected *) and with objects (left as an exercise). To summarize, in order to enable rank2 polymorphism we need a special kind of values to bear universal functions, as we can't rely on ordinary functions, which could be constructed using partial application. OCaml already had objects and records, which serve as a fine media for universally quantified functions. Later first class modules were introduced, which could also be used for the same purpose. Probably, one could devise a special syntax (or rely on the new attributes and extensions syntax, e.g., `map2 [%rank2 : fun x -> x] ("hello",42)` but probably this will lead to an unnecessary bloating of the language and the implementation, especially since we already have three solutions with a more or less tolerable syntax (and are in the base language, not an extension). Besides, if we will use the `[@@unboxed]` annotation, or visitor will have the same representation as a function, e.g., type 'r visitor = {visit : 'a. 'r -> 'a term -> 'r} [@@unboxed] let count x _ = x + 1 let counter = {visit=count} and # Core_kernel.phys_same count counter;; - : bool = true Concerning rank-n polymorphism, in OCaml is is achieved using functors. Yes, they are a little bit syntactically heavy and force us to write signatures, but this is necessary anyway as rank-n is undecidable (non-inferrable). Finally, as a real-world example [1] of rank-2 polymorphism consider the universal WAVL tree that is a binary tree with each element having a different type (aka heterogeneous map). We use it in BAP as a backing store. You might find a few tricks there, especially using continuation-passing in the recursive cases. Cheers, Ivan [1]: https://github.com/BinaryAnalysisPlatform/bap/blob/b40689e636607b977758af048b79d65684ce48c3/lib/knowledge/bap_knowledge.ml#L847-L1693 --000000000000a70eab059ba6ca44 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable


=
On Wed, Jan 8, 2020 at 1:54 AM <rixed@happyleptic.org> wrote:=
Hello and thank= you for the answer.

On Tue, Jan 7, 2020, at 21:21, Ivan Gotovchits wrote:
> It is the limitation of the let-bound polymorphism. (...)
> In your case, I would define a visitor type, e.g.,
>=C2=A0 type 'r visitor =3D {visit : 'a. 'a term -> '= r -> 'r}

Oh I see. I've used this trick to force a function to be polymorphic, b= ut I failed to see that this was the problem because to me `f` is not any m= ore polymorphic when the `term` is a GADT than when it's not.

So there is no lighter syntax to specify that `f` should accept any member = of a GADT than the syntax to specify that `f` should accept any type at all= ?

Only three methods of introducing rank-2 p= olymorphism=C2=A0are known to me:
1. records
2. obj= ects
3. first-class modules

Jacques has = demonstrated the solution with objects, which might be a little bit more li= ghtweight, at least as you don't need to define a new data type beforeh= and. But the invocation is more verbose and requires an annotation from the= caller side, which could be confusing. The third solution relies on first-= class modules and is even more verbose, at least on the definition side. Ju= st for the sake of completeness,

=C2=A0 module typ= e Visitor =3D sig
=C2=A0 =C2=A0 type t
=C2=A0 =C2=A0 val term : t -&g= t; 'a term -> t
=C2=A0 end

=C2=A0 let rec fold : type a r.= r -> (module Visitor with type t =3D r) -> a term -> r =3D
=C2= =A0 =C2=A0 fun i ((module Visit) as f) t -> match t with
=C2=A0 =C2= =A0 =C2=A0 | Int _ as t -> Visit.term i t
=C2=A0 =C2=A0 =C2=A0 | Add = as t -> Visit.term i t
=C2=A0 =C2=A0 =C2=A0 | App (x,y) as t ->=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 let i =3D fold i f x in
=C2=A0 =C2= =A0 =C2=A0 =C2=A0 =C2=A0 let i =3D fold i f y in
=C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 Visit.term i t

=C2=A0 let s =3D fold 0 (module struct<= br>=C2=A0 =C2=A0 =C2=A0 type t =3D int
=C2=A0 =C2=A0 =C2=A0 let term x _= =3D x + 1
=C2=A0 =C2=A0 end)

And again, it= is not about GADT. GADT act as a red herring here. As I've demonstrate= d earlier, using a simple pair will suffice to display the limitation of th= e prenex polymorphism. Even no ADT is required, just apply one term to anot= her two and you will get them unified, e.g.,

=C2= =A0 =C2=A0 let f g x y=C2=A0: unit =3D g x; g y

wi= ll have type

=C2=A0 =C2=A0val f : ('a -> un= it) -> 'a -> 'a -> unit

because &= #39;a is quantified on the scope of `f` not `g`, in other words, it has typ= e (not an OCaml syntax)=C2=A0

=C2=A0 =C2=A0val f := forall 'a. ('a -> unit) -> 'a -> 'a -> unit

while we would like to have a type

=C2=A0 =C2=A0val f : forall=C2=A0'b, 'c. (forall=C2=A0'= a. 'a -> unit) -> 'b -> 'c -> unit

OCaml doesn't allow us to define types like `('a. 'a -= > 'a)` and the reason is not that it is hard to extend the parser it= is...

I wonder, is this just a limitation of the OCaml parser or is there some de= ep reason for these work-around (like is the case, from my understanding, f= or the value restriction)?

Yep, good catch!= It is because of the impurity. Indeed, Haskell has the Rank2Types extensio= n that lets us write types like `(forall=C2=A0a. a -> ()) -> b -> = c -> ()`, with no extra syntactic burden (modulo having to provide the t= ype annotation). But functions in Haskell are pure, therefore it is possibl= e. To make the story short and obvious, let me do a simple demonstration of= how things can go wrong in a language with side-effects. Let's go back= to the simple example of pairs and the identity function. Consider the fol= lowing nasty identity function,=C2=A0

=C2=A0 l= et bad_id () =3D
=C2=A0 =C2=A0 let cache =3D ref None in
=C2=A0 =C2= =A0 fun x -> match cache.contents with
=C2=A0 =C2=A0 =C2=A0 | None -&= gt; cache :=3D Some x; x
=C2=A0 =C2=A0 =C2=A0 | Some cache -> cache

It has type `unit -> 'a -> 'a` th= erefore, if we would have the rank-1 polymorphism enabled for functions, we= could apply it to the function

=C2=A0 =C2=A0=C2= =A0 let map2 : fun ('a. 'a -> 'a) -> 'b -> 'c = -> 'b * 'c =3D fun f (x,y) -> f x, f y

as

=C2=A0 =C2=A0let x,y : string * int =3D map2= (bad_id ()) "hello", 42

and will get a = segmentation fault, as `y` will now have type int but hold a string.
<= div>
And here comes the syntax as a savior as it lets us spec= ify functions that are guaranteed to be syntactic values. Indeed, all three= solutions syntactically guarantee that the provided argument is a function= , not a closure. Indeed, let's introduce the universal identity via a r= ecord,

=C2=A0 =C2=A0type id =3D { f : 'a. '= ;a -> 'a}

and we can see that our `bad_= id` is not accepted due to the value restriction, while good_id, defined as= ,

=C2=A0 =C2=A0let good_id x =3D x

<= /div>
is perfectly fine, e.g.,

=C2=A0 let id1 = =3D {f =3D good_id} (*accepted *)
=C2=A0 let id2 =3D {f =3D bad_id}=C2= =A0 =C2=A0(* rejected *)

moreover, even a fine= , but not syntactic, identity is also rejected=C2=A0

=C2=A0 let fine_id () x =3D x
=C2=A0 let id3 =3D {f =3D fine_i= d ()} (* rejected *)

with the message

=C2=A0 This field value has type 'b -> 'b which= is less general than 'a. 'a -> 'a

<= div>The same is true with modules,

=C2=A0 module t= ype Id =3D sig
=C2=A0 =C2=A0 val f : 'a -> 'a
=C2=A0 end=C2=A0 module Id1 : Id =3D struct let f =3D good_id end=C2=A0 =C2=A0(* ac= cepted *)
=C2=A0 module Id2 : Id =3D struct let f =3D bad_id () end (* r= ejected *)
=C2=A0 module Id3 : Id =3D struct let f =3D fine_id () end (*= rejected *)

and with objects (left as an exer= cise).

To summarize, in order to enable rank2 poly= morphism=C2=A0we need a special kind of values to bear universal functions,= as we can't rely on ordinary functions, which could be constructed usi= ng partial application. OCaml already had objects and records, which serve = as a fine media for universally quantified functions. Later first class mod= ules were introduced, which could also be used for the same purpose. Probab= ly, one could devise a special syntax (or rely on the new attributes and ex= tensions syntax, e.g., `map2 [%rank2 : fun x -> x] ("hello",42= )` but probably this will lead to an unnecessary bloating of the language a= nd the implementation, especially since we already have three solutions wit= h a more or less tolerable syntax (and are in the base language, not an ext= ension).=C2=A0 Besides, if we will use the `[@@unboxed]` annotation, or vis= itor will have the same representation as a function, e.g.,

<= /div>
=C2=A0 =C2=A0 type 'r visitor =3D {visit : 'a. 'r -&g= t; 'a term -> 'r} [@@unboxed]
=C2=A0 =C2=A0=C2=A0let c= ount x _ =3D x + 1
=C2=A0 =C2=A0 let counter =3D {visit=3Dcount}= =C2=A0 =C2=A0=C2=A0

and

= =C2=A0 # Core_kernel.phys_same count counter;;
=C2=A0 - : bool =3D tru= e

Concerning rank-n polymorphism, in OCaml is is=C2=A0ac= hieved using functors. Yes, they are a little bit syntactically heavy and f= orce us to write signatures, but this is necessary anyway as rank-n is unde= cidable (non-inferrable). Finally, as a real-world example [1] of rank-2 po= lymorphism consider the universal WAVL tree that is a binary tree with each= element having a different type (aka heterogeneous map). We use it in BAP = as a backing store. You might find a few tricks there, especially using con= tinuation-passing in the recursive cases.=C2=A0

Ch= eers,
Ivan



=
=C2=A0 =C2=A0


--000000000000a70eab059ba6ca44--