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 mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by sympa.inria.fr (Postfix) with ESMTPS id 7229A7ED1A for ; Mon, 21 May 2012 11:26:13 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AqABAB4Juk/RVdW2kGdsb2JhbAA7CYUtpReJSAgiAQEBAQkJDQcUBCOCFQEBAQIBARICDwQZARIZCgQDAQsBBQULNwICIhIBBQEcBhMihXCBbgMGBQugcAkDi1KDQoRmJw0ViTcBBQyKeRCEKYEUA5UbgQ+NBj2BU4I2gV0 X-IronPort-AV: E=Sophos;i="4.75,629,1330902000"; d="scan'208";a="159134049" Received: from mail-yx0-f182.google.com ([209.85.213.182]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-MD5; 21 May 2012 11:26:10 +0200 Received: by yenl8 with SMTP id l8so6360473yen.27 for ; Mon, 21 May 2012 02:26:09 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:content-type; bh=KUVNB+gN3i3iBC7u3oStsAczsV76Xsru2V1Sov9eCM4=; b=MU0vnor/YYbWhy3To75rvGYZ5UloWrNQ3bcaZfJZff4I1mv4fxI5B7CiJpkQwarNgQ p97TuOA7BllPkrg9lj9+/N/c6hQlmhjv5FOG9FM130eOP/73O64bCpiN2OGGzPKVRIsW Ufr7fGupT9qfFuc/ocT12RrA/dsfwsZI56V97jGtHZXKcn+hiwJbGlm4bBl3VCbScbN+ oeynrxYQpYSN6Zj5Z1/UP/W0c3ePUMaeA5Uj01McMyNT5yOabNpHNtudQBzVdDWJMWSV 8Y8HezKHtfv/atb2M6l7N9RmtR0h00z+uOaD2dRjTMBYTKjpcRb5xXH/t+cZO1cwrxlu fflw== Received: by 10.50.140.5 with SMTP id rc5mr6169241igb.40.1337592369588; Mon, 21 May 2012 02:26:09 -0700 (PDT) MIME-Version: 1.0 Sender: arnaud.spiwack@gmail.com Received: by 10.64.38.6 with HTTP; Mon, 21 May 2012 02:25:29 -0700 (PDT) In-Reply-To: References: From: Arnaud Spiwack Date: Mon, 21 May 2012 11:25:29 +0200 X-Google-Sender-Auth: hU0et6Rm7Ka8Iw-XrlgloA0BavI Message-ID: To: OCaml Mailing List Content-Type: multipart/alternative; boundary=e89a8f83a34b0b282204c0887ea6 Subject: Re: [Caml-list] One-value functors --e89a8f83a34b0b282204c0887ea6 Content-Type: text/plain; charset=UTF-8 On 17 May 2012 18:23, Nicolas Braud-Santoni wrote: > Hi, > > If I'm not mistaken, you want something like Haskell's typeclasses. > I agree that it's a feature I often find myself wanting in OCaml, and > -as you point out- is trivial to encode with module and functors, so > it shouldn't be highly problematic. > Well, there is a superficial similarity with typeclasses, in that it may be used for similar patterns, and that without first-class functors, we are bound to some prefix abstractions (first all the functor abstractions, then the regular type). With first-class functors, however, we can, in principle be much freer. But really, my reason for using these one-value functors (monofunctors?) is to gain access to higher kinding (like, in my above example, function abstracted over type families). On 17 May 2012 16:52, Goswin von Brederlow wrote: > Arnaud Spiwack writes: > > type a and b > > module type TC = sig type 'a t end > > module type Subst = functor (A:TC) -> sig val x : a A.t -> b A.t end > > What are you trying to do there? Why do you need a functor for that at > all? TC just having a type doesn't make sense to me. > This is part of the definition of Leibniz equality in [ http://okmij.org/ftp/ML/first-class-modules/first-class-modules.pdf ]. The idea is that a and b must be the same type et Subst.x the identity. Hard to say if I can't even understand what "this kind of thing" is. > Well, you probably never needed such a pattern, otherwise you would have recognised it. Let me try to give you a more concrete example. The simplest case, I believe, where one would want higher-kinding is linked to interruptible List.fold_left, using option to report errors (you can use it, for instance, to define List.for_all exiting as soon as you know the answer is "false"). Let's proceed : val i_iter : ('a -> 'b -> 'a option) -> 'a -> 'b list -> 'a option let rec i_iter f seed = function | [] -> Some seed | b::l -> match f seed b with | None -> None | Some a -> i_iter f a l This was quite direct, but is part of a bigger story, which involves monads. The above definition can be abstracted over monads in the following manner module type Monad = sig type 'a t val return : 'a -> 'a t val (>>=) : 'a t -> ('a -> 'b t) -> 'b t end module MIter (M:Monad) = struct let rec x f seed = function | [] -> M.return seed | b::l -> M.(f seed b >>= fun a -> x f a l) end The proposed syntax would let me write the MIter as a val, rather than a module : val m_iter : (M:Monad) => ('a -> 'b -> 'a M.t) -> 'a -> 'b list -> 'a M.t Then you can get the traditional fold_left as let fold_left = m_iter {{struct type 'a t = 'a let return x = x let (>>=) x k = k x end}} The interruptible fold_left as let i_iter = m_iter {{struct type 'a t = 'a option let return x = Some x let (>>=) x k = match x with | None -> None | Some x' -> k x' end}} You can also get a lazy fold_left as let l_iter = m_iter {{struct type 'a t = 'a Lazy.t let return x = Lazy.lazy_from_val x let (>>=) x k = lazy (k (force x)) end}} One that is particularly useful for me is a fold_left compatible with state passing style let s_iter (type state) = m_iter {{struct type 'a t = state -> ('a*state) let return x s = (x,s) let (>>=) x k s = let (x',s') = x s in k x' s' end}} What matters is that I need to abstract over a type family, which cannot be done without functors in OCaml. -- Arnaud --e89a8f83a34b0b282204c0887ea6 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

On 17 May 2012 18:23, Nicolas Braud-Santoni <<= a href=3D"mailto:nicolas@braud-santoni.eu" target=3D"_blank">nicolas@braud-= santoni.eu> wrote:
Hi,

If I'm not mistaken, you want something like Haskell's typeclasses.=
I agree that it's a feature I often find myself wanting in OCaml, and -as you point out- is trivial to encode with module and functors, so
it shouldn't be highly problematic.

Well, there is = a superficial similarity with typeclasses, in that it may be used for simil= ar patterns, and that without first-class functors, we are bound to some pr= efix abstractions (first all the functor abstractions, then the regular typ= e). With first-class functors, however, we can, in principle be much freer.= But really, my reason for using these one-value functors (monofunctors?) i= s to gain access to higher kinding (like, in my above example, function abs= tracted over type families).



On 17 May 2012 16:52, Goswin von Brederlow &l= t;goswin-v-b@web.de<= /a>> wrote:
Arnaud Spiwack <Arnaud.Spiwack@lix.polytechnique.fr> writes: > =C2=A0 =C2=A0 type a and b
> =C2=A0 =C2=A0 module type TC =3D sig type 'a t end
> =C2=A0 =C2=A0 module type Subst =3D functor (A:TC) -> sig val x : a= A.t -> b A.t end

What are you trying to do there? Why do you need a functor for that a= t
all? TC just having a type doesn't make sense to me.
This is part of the definition of Leibniz equality in=C2=A0 [ http://okmij.org/ftp/ML/first-class-modules/first-class-modules= .pdf ]. The idea is that a and b must be the same type et Subst.x the i= dentity.

Hard to say if I can&= #39;t even understand what "this kind of thing" is.

Well, you probably never needed such a pattern, otherwise you would hav= e recognised it. Let me try to give you a more concrete example.

The= simplest case, I believe, where one would want higher-kinding is linked to= interruptible List.fold_left, using option to report errors (you can use i= t, for instance, to define List.for_all exiting as soon as you know the ans= wer is "false"). Let's proceed :

val i_iter : ('a -> 'b ->= 'a option) -> 'a -> 'b list -> 'a option
let r= ec i_iter f seed =3D function
=C2=A0 | [] -> Some seed
=C2=A0 | b:= :l -> match f seed b with | None -> None | Some a -> i_iter f a l<= br>

This was quite direct, but is part of a bigger story, which invol= ves monads. The above definition can be abstracted over monads in the follo= wing manner

module type Monad =3D si= g
=C2=A0 type 'a t

=C2=A0 val return : 'a -> 'a t
= =C2=A0 val (>>=3D) : 'a t -> ('a -> 'b t) -> = 9;b t
end

module MIter (M:Monad) =3D struct
=C2=A0 let rec x f= seed =3D function
=C2=A0=C2=A0=C2=A0 | [] -> M.return seed
=C2=A0=C2=A0=C2=A0 | b::l -> M.(f seed b >>=3D fun a -> x f a l= )
end


The proposed syntax would let me write the MIter = as a val, rather than a module :

val= m_iter : (M:Monad) =3D> ('a -> 'b -> 'a M.t) -> &#= 39;a -> 'b list -> 'a M.t

Then you can get the traditional fold_left as

let fold_left =3D m_iter {{struct type 'a t =3D &= #39;a=C2=A0 let return x =3D x let (>>=3D) x k =3D k x end}}

The interruptible fold_left as

let i_iter =3D m_iter {{struct type = 9;a t =3D 'a option let return x =3D Some x let (>>=3D) x k =3D m= atch x with | None -> None | Some x' -> k x' end}}
<= br>You can also get a lazy fold_left as

let l_iter =3D m_iter {{struct type = 9;a t =3D 'a Lazy.t=C2=A0 let return x =3D Lazy.lazy_from_val x let (&g= t;>=3D) x k =3D lazy (k (force x)) end}}

One that is partic= ularly useful for me is a fold_left compatible with state passing style

let s_iter (type state) =3D m_iter {{st= ruct type 'a t =3D state -> ('a*state) let return x s =3D (x,s) = let (>>=3D) x k s =3D let (x',s') =3D x s in k x' s' = end}}

What matters is that I need to abstract over a type family, which canno= t be done without functors in OCaml.


--
Arnaud
--e89a8f83a34b0b282204c0887ea6--