From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p38BPL0O015654 for ; Fri, 8 Apr 2011 13:25:21 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgcCAOrvnk3RVdg0kGdsb2JhbACmDQgUAQEBAQkJDQcUBCGIep07imiCI4UAMIhdAQEDBoVnBI1OiTY6 X-IronPort-AV: E=Sophos;i="4.63,322,1299452400"; d="scan'208";a="92528040" Received: from mail-qw0-f52.google.com ([209.85.216.52]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 08 Apr 2011 13:25:15 +0200 Received: by qwb8 with SMTP id 8so2967305qwb.39 for ; Fri, 08 Apr 2011 04:25:13 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:in-reply-to:references:date :message-id:subject:from:to:cc:content-type; bh=UUtq2rYrQtsTi8R8RIyNTKNf7Y7BsXPBCwRv+XFtnOU=; b=G6D7xogW8d4HU+56BPKOcqPjXTErqHt4Ri/DNIzj5t6KfG+1UqDRQEgUFtPmF/4bFG 5O/rddqr8/1L4v8dBTgI+Sgd9Tnot0agmkgD4NLznP91kpqWzyZ0BPAZUYQgW9QgEIn7 I+89T/5O72WYRFWEJ/qCY+1Y/BEe53tqhiS3E= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; b=wR5kaNo0uOjgDQVzbhiN16xm43axiXjk66YD4X0w6EVzyJxhZ0s66mwx3uNHTBvaj4 P7Dx57VmFHEPY6gmuR/94w0b6zBZQ9mr4kl4FDCU2alVXznTSiOeU5XR59q+cMHLaGGb WBPT/Gw3e/h5ehinpDPFdwNBOIl9lMlw+B30k= MIME-Version: 1.0 Received: by 10.229.141.11 with SMTP id k11mr1595496qcu.195.1302261913350; Fri, 08 Apr 2011 04:25:13 -0700 (PDT) Received: by 10.229.250.5 with HTTP; Fri, 8 Apr 2011 04:25:13 -0700 (PDT) In-Reply-To: <4D9ECAF2.7070300@lexifi.com> References: <4D9E28D2.1050808@wp.pl> <1302212990.8429.1150.camel@thinkpad> <0F248A34-05CF-4640-B122-75C4CE7C2CD2@mpi-sws.org> <4D9EC172.1060205@lexifi.com> <4D9ECAF2.7070300@lexifi.com> Date: Fri, 8 Apr 2011 13:25:13 +0200 Message-ID: From: Julien Signoles To: Alain Frisch Cc: Jacques Garrigue , caml-list Content-Type: multipart/alternative; boundary=90e6ba10aa75bff54a04a0667aec Subject: Re: [Caml-list] What is an applicative functor? --90e6ba10aa75bff54a04a0667aec Content-Type: text/plain; charset=ISO-8859-1 Hello, 2011/4/8 Alain Frisch > On 04/08/2011 10:20 AM, Jacques Garrigue wrote: > >> Applicative functors have other advantages, like the fact you can refer to >> a >> type produced by a functor without having really applied it. >> >> For instance think of the following functor definition >> >> module F(O : Set.OrderedType)(S : sig type t = Set.Make(O).t val union >> : t -> t -> t end) = ... >> >> If you want to do the same thing with generative functors, I believe you >> have to >> pass the result of Set.Make(O) around physically. >> I do think this is a significant weakness. >> > > I can imagine uses for: > > module F(O : Set.OrderedType)(S : Set.S with type elt = O.t) = > > but I don't see a real-life case where one would want functor F to know > that the type S.t was really produced by applying Set.Make. Do you have a > specific example in mind? > I just try to compile Frama-C (http://frama-c.com) with the option -no-app-funct in order to discover where/why we need applicative functors (I knew that we use them somewhere). I found three different patterns: 1) module M = F(G(X)) Without applicative functors, we get the error "The parameter cannot be eliminated in the result type. Please bind the argument to a module identifier.". That is easy to fix by introducing an intermediate module. 2) module F(X:...) = G(H(X)) Without applicative functors, we again get the error about parameter elimination. But I see no workaround to eliminate it without changing the signature of F. So IMHO that is a use case where applicative functors are useful. 3) type t = F(X).t type u = { a: t } These declarations are in a single .mli file without a corresponding .ml file. G(X).t is an abstract type. Generators of values of type u are in a module F while users of type u are others modules. Also we have to solve an usual issue with mutual dependencies between F and its users. But the type u is one of the most useful type in Frama-C. Thus standard solution to the mutual dependencies issues which use polymorphism or functor are too heavy here. That is the lightweight solution that we found. To summarize: - case 1 may be easily solved by writting 2 lines of code instead of 1 - case 2 and 3 may be circumvented for sure, but the solutions that I have in mind are heavy To conclude, there are only few use case where applicative functors are useful in an application like Frama-C (where there are thousands of functor applications). But IMHO that are enough cases to answer: yes applicative functors are (sometimes) useful. -- Julien --90e6ba10aa75bff54a04a0667aec Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Hello,

2011/4/8 Alain Frisch <alain.frisch@lexifi.co= m>
On 04/08/2011 10:20 AM, Jacques Garrigue wrote:
Applicative functors have other advantages, like the fact you can refer to = a
type produced by a functor without having really applied it.

For instance think of the following functor definition

=A0 =A0module F(O : Set.OrderedType)(S : sig type t =3D Set.Make(O).t val = union : t -> =A0t -> =A0t end) =3D ...

If you want to do the same thing with generative functors, I believe you ha= ve to
pass the result of Set.Make(O) around physically.
I do think this is a significant weakness.

I can imagine uses for:

module F(O : Set.OrderedType)(S : Set.S with type elt =3D O.t) =3D

but I don't see a real-life case where one would want functor F to know= that the type S.t was really produced by applying Set.Make. =A0Do you have= a specific example in mind?

I just try to compile= Frama-C (http://frama-c.com) with the o= ption -no-app-funct in order to discover where/why we need applicative func= tors (I knew that we use them somewhere).
I found three different patterns:

1) module M =3D F(G(X))

Wit= hout applicative functors, we get the error "The parameter cannot be e= liminated in the result type. Please bind the argument to a module identifi= er.". That is easy to fix by introducing an intermediate module.

2) module F(X:...) =3D G(H(X))

Without applicative functors, we = again get the error about parameter elimination. But I see no workaround to= eliminate it without changing the signature of F. So IMHO that is a use ca= se where applicative functors are useful.

3) type t =3D F(X).t
=A0=A0=A0 type u =3D { a: t }
These declara= tions are in a single .mli file without a corresponding .ml file. G(X).t is= an abstract type. Generators of values of type u are in a module F while u= sers of type u are others modules. Also we have to solve an usual issue wit= h mutual dependencies between F and its users. But the type u is one of the= most useful type in Frama-C. Thus standard solution to the mutual dependen= cies issues which use polymorphism or functor are too heavy here. That is t= he lightweight solution that we found.

To summarize:
- case 1 may be easily solved by writting 2 lines of = code instead of 1
- case 2 and 3 may be circumvented for sure, but the s= olutions that I have in mind are heavy

To conclude, there are only f= ew use case where applicative functors are useful in an application like Fr= ama-C (where there are thousands of functor applications). But IMHO that ar= e enough cases to answer: yes applicative functors are (sometimes) useful.<= br> =A0
--
Julien
--90e6ba10aa75bff54a04a0667aec--