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 CCF237F214 for ; Tue, 7 Jan 2020 21:20:36 +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-f171.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of ivg@ieee.org) identity=pra; client-ip=209.85.208.171; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="ivg@ieee.org"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of ivg@ieee.org designates 209.85.208.171 as permitted sender) identity=mailfrom; client-ip=209.85.208.171; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="ivg@ieee.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-lj1-f171.google.com) identity=helo; client-ip=209.85.208.171; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="postmaster@mail-lj1-f171.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AqLxolRC85ogCLikxOjMMUyQJP3N1i/DPJgcQr6Af?= =?us-ascii?q?oPdwSPrzocbcNUDSrc9gkEXOFd2Cra4d0KyM7v6rADNIyK3CmUhKSIZLWR4BhJ?= =?us-ascii?q?detC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+?= =?us-ascii?q?KPjrFY7OlcS30P2594HObwlSizexfL1/IA+ooQjRt8QajpZuJ6QswRbVv3VEfP?= =?us-ascii?q?hby3l1LlyJhRb84cmw/J9n8ytOvv8q6tBNX6bncakmVLJUFDspPXw7683trhnD?= =?us-ascii?q?UBCA5mAAXWUMkxpHGBbK4RfnVZrsqCT6t+592C6HPc3qSL0/RDqv47t3RBLulS?= =?us-ascii?q?wKMSMy/mPKhcxqlK9UrxyhqB5/zYDaY4+bKeRwcb/GcNwAWWZMRNxcWzBdDo6+?= =?us-ascii?q?aYYEEuoPPfxfr4n4v1YArgW+ChOqBOjyyzFIgWP23aok0+s9EQHG3RAgH8kTu3?= =?us-ascii?q?nTrdX1KqgSXPu0zKbW0zrMcela2TDn6IjHax0sp+yHU7FoccfJ10UjCwfIgk+T?= =?us-ascii?q?pIHlJT+ZyPgBvmuB4+Z9V++jlmgqoBxrrDe13McjkIzJi5oVyl/a8SV5x544Jd?= =?us-ascii?q?iiR056Zd6oCZ9QtyOHO4dvTMMuXmNltDsgxr0Jvp67eycKyJA5yBLFd/OHdI2I?= =?us-ascii?q?7griVOaXPzh4mGpodKyjixu260Stye3xWtOq3FpWrSdJiMTAu3IQ2xDL78iIUP?= =?us-ascii?q?p9/kOv2TaV0ADT7/lJIUEqlarUMJMhw6A/mYQNvkjZGS/2gkr2gLeMdko44uio?= =?us-ascii?q?9/jnYrL+q5CALYB0jwX+Pr0qmsy+GuQ4LhMDX3Ob+OS5zL3s51f1QLRMjv0sk6?= =?us-ascii?q?nWqorWJcoBpv3xPwgAyIcz5hqXDz6+yMUckGEbLVkDfwiI3KbzPFSbAe7xC7+Q?= =?us-ascii?q?hEirjjxrxuzddungHJrlL3XOnfHmZ7kruB0U8xY60d0Kv8EcMboGOv+mAhat5u?= =?us-ascii?q?ydNQcwNkmP+8iiEM90j9tMWG+CD+meKqyA6QbZtNJqGPGFYcougBi4LvEk4/D0?= =?us-ascii?q?inpgwQ0ccKSkm5wNZyLhR6k0EwCieXPpx+w5PyIKsw45FrK4jVSDVXtXZS/3Uf?= =?us-ascii?q?tjv3c0D4WpCYqFTYeo0uSM?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0B4BADb5hRehqvQVdFlhiszKoQJgRyOA?= =?us-ascii?q?Yt/kUgJAQMBDC8BAYRAAoFpHAcBBDQTAhABAQQBAQECAQIDBAETAQEBCAsLCCm?= =?us-ascii?q?FPgyCOyKDAgIBAxIRBBkBATcBDwkCBAc3AgIiEgEFARwZGweDAIJTJZEkjw6BA?= =?us-ascii?q?z2LJn8zgn4BAQWFfIE0CRKBJIwZGoFBP4ERNoIvLj6HWYJel2OXQIJAlhwbml+?= =?us-ascii?q?pTQ8jgUaBen0IOzEGgjVQGA2NLIhthV0mMJB8AQE?= X-IPAS-Result: =?us-ascii?q?A0B4BADb5hRehqvQVdFlhiszKoQJgRyOAYt/kUgJAQMBDC8?= =?us-ascii?q?BAYRAAoFpHAcBBDQTAhABAQQBAQECAQIDBAETAQEBCAsLCCmFPgyCOyKDAgIBA?= =?us-ascii?q?xIRBBkBATcBDwkCBAc3AgIiEgEFARwZGweDAIJTJZEkjw6BAz2LJn8zgn4BAQW?= =?us-ascii?q?FfIE0CRKBJIwZGoFBP4ERNoIvLj6HWYJel2OXQIJAlhwbml+pTQ8jgUaBen0IO?= =?us-ascii?q?zEGgjVQGA2NLIhthV0mMJB8AQE?= X-IronPort-AV: E=Sophos;i="5.69,407,1571695200"; d="scan'208,217";a="430300483" X-MGA-submission: =?us-ascii?q?MDFMWGwXV881xGZE/LJEUfPicovN8Fm4nTiD7c?= =?us-ascii?q?HarDitzZolpuw2o68iH6FPnfqOEmK1AzFUq0V5Rp67PXfkSIJG+RazHZ?= =?us-ascii?q?ofh7zHbHnqyVzHaBrb5ctfwZd1GjmS8BSyUVc1J405jxuANdUi1GAU27?= =?us-ascii?q?ZcUQGcx/rWaNdQlLCWiYIozA=3D=3D?= Received: from mail-lj1-f171.google.com ([209.85.208.171]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 07 Jan 2020 21:20:35 +0100 Received: by mail-lj1-f171.google.com with SMTP id m26so860602ljc.13 for ; Tue, 07 Jan 2020 12:20:35 -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=PZpjPMqn6l/GQ9NlYomnwjk/I/Ebh6/AJ3bRYMPb3To=; b=XIJK56S9rdHlVJC6OaL5vrk5IBhzHbqgKyQUIFmmjH3U68upuWmrLOBffKrLhf6E9H heMDuu9wLu9zvfyYTK8usBlyglkY+ytFUmkUw4skNgA2Y+ePAq5Sby+zgY8UfT+bCw7e ZyQ1ZMz9OL7+Lllg2H3WRNEHDCxQq1jTjZcYs= 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=PZpjPMqn6l/GQ9NlYomnwjk/I/Ebh6/AJ3bRYMPb3To=; b=WHG67aP2UR7ljXTPhe/7OXEriBmN7NWJBbRQl1zR+apRCjyOpj5ww0PtIspQsV1IMH 7X+blSCeMPSExXXQIYztMC6HMcNFJLtlO2gp8v+AUAc9ff2ZSVVzXBZSlkd5vkY5utkM 6Lh0MW1QmqQHyLlHCSR5/vNLsWLS0mH3m4+VUL6fkFrgCHOXm/6CFVTALrBYDTfbA0FB YKIqsY0Alm959I2Vb4fDdC39kSTWvWX9fgar3mqIh1jWcLlXWF6LY96UJiAqNN5hCBis xiaZNQekj9C6LJSo5rOLGM25Kx0kRg654nBaUu5JpCJNqtR8lLW3ysJeYuO5Gb+g5e5l cZzg== X-Gm-Message-State: APjAAAUs5cEoBCd3wiwnmauV9VQXRYTpgICiYwwEzO/y5D0BCCW6mMud GdKTAemxGPKtlmgAHItR3BU7M4QGzmTPdgCEQe/RSZoxTL0= X-Google-Smtp-Source: APXvYqx/X5SQJ4ptBHJXz/NwyoCav9L2osoUElzOnfqgVAO/IdbHL110Z+YmuvHCATkY+teYFYTHWEwyle3hsAYhBnM= X-Received: by 2002:a2e:9691:: with SMTP id q17mr720921lji.91.1578428434441; Tue, 07 Jan 2020 12:20:34 -0800 (PST) MIME-Version: 1.0 References: <4d2b5367-a869-42bc-9547-b58864c10cf8@www.fastmail.com> In-Reply-To: <4d2b5367-a869-42bc-9547-b58864c10cf8@www.fastmail.com> From: Ivan Gotovchits Date: Tue, 7 Jan 2020 15:21:03 -0500 Message-ID: To: rixed@happyleptic.org Cc: caml-list Content-Type: multipart/alternative; boundary="000000000000237f46059b928226" Subject: Re: [Caml-list] Calling a single function on every member of a GADT? --000000000000237f46059b928226 Content-Type: text/plain; charset="UTF-8" On Tue, Jan 7, 2020 at 2:25 PM wrote: > ... but using a GADT: > > --- > module Gadt = > struct > type _ term = > | Int : int -> int term > | Add : (int -> int -> int) term > | App : ('b -> 'a) term * 'b term -> 'a term > > let rec fold : type a. 'r -> ('r -> _ term -> 'r) -> 'r = fun i f -> > function > | Int _ as t -> f i t > | Add -> f i Add > (* > ^ Error: This pattern matches values of type (int -> int -> int) term > but a pattern was expected which matches values of type int term > Type int -> int -> int is not compatible with type int > *) > | App (x, y) as t -> f (fold (fold i f x) f y) t > end > --- > > I've tried other variants of the syntax and got many encouragements but no > green flag from the type-checker. > Why is the compiler expecting an int term in there? I though the whole > point of the `type a. ...` syntax was to allow the matched type to vary > from one pattern to the next? > Is there a way to do this? > It is the limitation of the let-bound polymorphism. A parameter of a function is monomorphic in its body. The classical example doesn't even reference any GADT, let example f = f "hello", f 42 It won't compile even though we can provide a polymorphic function that can applied both to integers and to strings, e.g., `exampe (fun x -> x)` should be possible, but not, because of the let-bounded polymorphism. There are a few solutions available in OCaml, the simplest is to use records, e.g., type app = {apply : 'a. 'a -> 'a} let example {apply} = apply "hello", apply 42;; val example : app -> string * int = Now we have `app` that is polymorphic. In your case, I would define a visitor type, e.g., type 'r visitor = {visit : 'a. 'a term -> 'r -> 'r} let rec fold : type a. 'r -> 'r visitor -> a term -> 'r = fun i f t -> match t with | Int _ as t -> f.visit i t | Add as t -> f.visit i t | App (x,y) as t -> let i = fold i f x in let i = fold i f y in f.visit i t Cheers, Ivan Gotovchits --000000000000237f46059b928226 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable


=
On Tue, Jan 7, 2020 at 2:25 PM <rixed@happyleptic.org> wrote:=
... but using a GADT:

---
module Gadt =3D
struct
=C2=A0 type _ term =3D
=C2=A0 =C2=A0 =C2=A0| Int : int -> int term
=C2=A0 =C2=A0 =C2=A0| Add : (int -> int -> int) term
=C2=A0 =C2=A0 =C2=A0| App : ('b -> 'a) term * 'b term -> = 'a term

=C2=A0 let rec fold : type a. 'r -> ('r -> _ term -> '= r) -> 'r =3D fun i f -> function
=C2=A0 =C2=A0 | Int _ as t -> f i t
=C2=A0 =C2=A0 | Add -> f i Add
(*
=C2=A0 =C2=A0 =C2=A0^ Error: This pattern matches values of type (int ->= int -> int) term
=C2=A0 =C2=A0 =C2=A0 =C2=A0 but a pattern was expected which matches values= of type int term
=C2=A0 =C2=A0 =C2=A0 =C2=A0 Type int -> int -> int is not compatible = with type int
*)
=C2=A0 =C2=A0 | App (x, y) as t -> f (fold (fold i f x) f y) t
end
---

I've tried other variants of the syntax and got many encouragements but= no green flag from the type-checker.
Why is the compiler expecting an int term in there? I though the whole poin= t of the `type a. ...` syntax was to allow the matched type to vary from on= e pattern to the next?
Is there a way to do this?
=C2=A0
It is the = limitation of the let-bound polymorphism. A parameter of a function is mono= morphic in its body. The classical example doesn't even reference any G= ADT,

=C2=A0 =C2=A0 let example f=C2=A0 =3D f "= ;hello", f 42

It won't compile even thoug= h we can provide a polymorphic function that can applied both to integers a= nd to strings, e.g., `exampe (fun x -> x)` should be possible, but not, = because of the let-bounded polymorphism. There are a few solutions availabl= e in OCaml, the simplest is to use records, e.g.,

= =C2=A0 =C2=A0 type app =3D {apply : 'a. 'a -> 'a}

=C2=A0 =C2=A0 let example {apply} =3D apply "hello", appl= y 42;;=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0= =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0=C2=A0
=C2=A0 =C2=A0 val example : ap= p -> string * int =3D <fun>
=C2=A0
Now we = have `app` that is polymorphic.=C2=A0
In your case, I would defin= e a visitor type, e.g.,

=C2=A0 type 'r visitor= =3D {visit : 'a. 'a term -> 'r -> 'r}

=
=C2=A0 let rec fold : type a. 'r -> 'r visitor -> = a term -> 'r =3D
=C2=A0 =C2=A0 fun i f t -> match t with
= =C2=A0 =C2=A0 =C2=A0 | Int _ as t -> f.visit i t
=C2=A0 =C2=A0 =C2=A0= | Add as t -> f.visit 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 f.visit i t


Cheers,<= /div>
Ivan Gotovchits
=C2=A0

--000000000000237f46059b928226--