[Caml-list] One-value functors

[Caml-list] One-value functors

[Arnaud Spiwack]

[-- Attachment #1: Type: text/plain, Size: 2291 bytes --]

Dear all,

With the advent of first-class modules, I find myself more and more wanting
to write functors with only one (value) component, just to benefit from
type dependencies. Here is an example (randomly) extracted from Oleg
Kiselyov and Jeremy Yallop:

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
>

If this pattern had to become widespread, it would be worth agreeing for a
name on the single component, though it's a bit unnecessary to need a name
at all.
It get very verbose, though, when trying to applying the functor. Supposing
I have a module Subst:Subst :

let module S = Subst(sig type 'a t = 'a list) in
> S.x …
>

Nothing terrible really, but it sort of gets in the way. I can see benefit
in having a special syntax for this sort of definition. I think we could
take advantage of first-class functors to get something quite modular, here
is a mockup syntax:

We could have the type

(X:A) => t
>

stand for (something like)

module F = functor (X:A) -> sig val x : t end
>
(module F)
>

and the definition

let f {{X:A}} = e
>

stand for

let f = let module F (X:A) -> struct let x = e end
>

and finally we'd need an application

e {{M}}
>

would stand for (something like)

let module F = (val e) in let module F' = F(M) in F'.x
>


Clearly the application needs something like OCaml 4.0 and the type
definition some kind of cleverness (I don't know, by the way, why the
syntax for F cannot be inlined in the type).

In this example syntax the above example would look like

type a and b
> module type TC = sig type 'a t end
> val subst : (A:TC) => a A.t -> b B.t
>
> subst {{sig type 'a t = 'a list end}} …
>

I believe this would be something cool to have, so I came with two
questions:
1/ Is there some demand for this kind of things (if not, I'm not sure it's
worth pursuing, though of course demand could appear after supply)
2/ I don't see how to define the type syntax in camlp4, because of the
inlining thing, could it be done?
   (an alternative may be to have (X:A) => t be a module type, but then
(X:A) => (Y:B) => t is not a valid type, so we would need syntaxes for
n-ary abstraction/applications)

[-- Attachment #2: Type: text/html, Size: 3842 bytes --]

Re: [Caml-list] One-value functors

[Goswin von Brederlow]

Arnaud Spiwack <Arnaud.Spiwack@lix.polytechnique.fr> writes:

> Dear all,
>
> With the advent of first-class modules, I find myself more and more wanting to
> write functors with only one (value) component, just to benefit from type
> dependencies. Here is an example (randomly) extracted from Oleg Kiselyov and
> Jeremy Yallop:
>
>
>     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.

> If this pattern had to become widespread, it would be worth agreeing for a name
> on the single component, though it's a bit unnecessary to need a name at all.
> It get very verbose, though, when trying to applying the functor. Supposing I
> have a module Subst:Subst :
>
>
>     let module S = Subst(sig type 'a t = 'a list) in
>     S.x ?

So S.x would be a function that turns for example an int list into a
float list, e.g. let x list = List.map float_of_int list?

How would you write Subst that it takes anything but 'a list (and
Obj.magic doesn't count)? How would the functor look like that would
accept 'a list or 'a array as argument? Seems to me TC needs to also
contain the map function for this to work. And then why not just use
(List.map float_of_int) as closure?

> I believe this would be something cool to have, so I came with two questions:
> 1/ Is there some demand for this kind of things (if not, I'm not sure it's
> worth pursuing, though of course demand could appear after supply)
> 2/ I don't see how to define the type syntax in camlp4, because of the inlining
> thing, could it be done?
>    (an alternative may be to have (X:A) => t be a module type, but then  (X:A)
> => (Y:B) => t is not a valid type, so we would need syntaxes for n-ary
> abstraction/applications)

Hard to say if I can't even understand what "this kind of thing" is.

MfG
        Goswin

Re: [Caml-list] One-value functors

[Nicolas Braud-Santoni]

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.

Is there some syntax extension providing such a feature ?
If not, are there plans to have syntax for typeclass-like functor operations ?

Regard,
Nicolas

2012/5/11 Arnaud Spiwack <Arnaud.Spiwack@lix.polytechnique.fr>:
> Dear all,
>
> With the advent of first-class modules, I find myself more and more wanting
> to write functors with only one (value) component, just to benefit from type
> dependencies.
>[...]
>
> We could have the type
>> (X:A) => t
>
> stand for (something like)
>> module F = functor (X:A) -> sig val x : t end
>> (module F)
>
> and the definition
>> let f {{X:A}} = e
>
> stand for
>> let f = let module F (X:A) -> struct let x = e end
>
> and finally we'd need an application
>> e {{M}}
>
> would stand for (something like)
>> let module F = (val e) in let module F' = F(M) in F'.x
>
> Clearly the application needs something like OCaml 4.0 and the type
> definition some kind of cleverness (I don't know, by the way, why the syntax
> for F cannot be inlined in the type).
> [...]

Re: [Caml-list] One-value functors

[Arnaud Spiwack]

[-- Attachment #1: Type: text/plain, Size: 3517 bytes --]

On 17 May 2012 18:23, Nicolas Braud-Santoni <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 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 <goswin-v-b@web.de> wrote:

> Arnaud Spiwack <Arnaud.Spiwack@lix.polytechnique.fr> 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

[-- Attachment #2: Type: text/html, Size: 5170 bytes --]

Re: [Caml-list] One-value functors

[Arnaud Spiwack]

[-- Attachment #1: Type: text/plain, Size: 4720 bytes --]

Here is another kind of example I've boiled down as much as I could (it is
somewhat related to the Leibniz equality).
Oleg Kiselyov and Jeremy Yallop (
http://okmij.org/ftp/ML/first-class-modules/ ) have noticed that
first-class modules could be leveraged to produce an variant of the Finally
Tagless approach (which consist in replacing the use of a gadt by a
typeclass signature, in Haskell, to denote expressions). I like to call it
Initially Tagless.

The idea is to start with a signature representing your language, a field
for each language construct. Here, the language admits two types (int and
bool) and one operation on each:

module type S = sig
  type 'a t

  val int : int -> int t
  val bool : bool -> bool t
  val (+) : int t -> int t -> int t
  val if_ : bool t -> 'a t -> 'a t -> 'a t
end

An interpreter for the language is a module of type S. The type of
expressions [a Expr.t] is, then, defined as that of things which, for any
interpretor X, can be interpreted into an [a X.t]. Here goes the code in
OCaml 3.12, you might notice it is very repetitive:

module Expr : sig
  include S

  module Interp (X:S) : sig
    val x : 'a t -> 'a X.t
  end
end = struct

  module type T = sig
    type a

    module Interp (X:S) : sig
      val x : a X.t
    end
  end

  type 'a t = (module T with type a = 'a)

  module Interp (X:S) = struct
    let x (type w) (e:w t) : w X.t=
      let module E = (val e : T with type a = w) in
      let module IE = E.Interp(X) in
      IE.x
  end

  let int x =
    let module M = struct
      type a = int

      module Interp (X:S) = struct
        let x = X.int x
      end
    end in
    (module M : T with type a = int)

  let bool x =
    let module M = struct
      type a = bool

      module Interp (X:S) = struct
        let x = X.bool x
      end
    end in
    (module M : T with type a = bool)

  let (+) n p =
    let module M = struct
      type a = int

      module Interp (X:S) = struct
        let x =
          let module MN = (val n : T with type a=int) in
          let module IN = MN.Interp(X) in
          let n' = IN.x in
          let module MP = (val p : T with type a=int) in
          let module IP = MN.Interp(X) in
          let p' = IP.x in
          X.(n'+p')
      end
    end in
    (module M : T with type a = int)

  let if_ (type w) b (t:w t) (e:w t) =
    let module M = struct
      type a = w

      module Interp (X:S) = struct
        let x =
          let module MB = (val b : T with type a=bool) in
          let module IB = MB.Interp(X) in
          let b' = IB.x in
          let module MT = (val t : T with type a=w) in
          let module IT = MT.Interp(X) in
          let t' = IT.x in
          let module ME = (val e : T with type a=w) in
          let module IE = ME.Interp(X) in
          let e' = IE.x in
          X.if_ b' t' e'
      end
    end in
    (module M : T with type a = w)
end

My proposition of syntax aims at dealing gracefully with some of the
repetitive parts. It would look something like :

module Expr : sig
  include S

  val interp : (X:S) => 'a t -> 'a X.t
end = struct

  module type T = sig
    type a
    val interp : (X:S) => a X.t
  end

  type 'a t = (module T with type a = 'a)

  let interp {{X:S}} (type w) (e:w t) : w X.t =
    let module E = (val e : T with type a = w) in
    E.interp {{X}}

  let int x =
    let module M = struct
      type a = int
      let interp {{X:S}} = X.int x
    end in
    (module M : T with type a = int)

  let bool x =
    let module M = struct
      type a = bool
      let interp {{X:S}} = X.bool x
    end in
    (module M : T with type a = bool)

  let (+) n p =
    let module M = struct
      type a = int

      let interp {{X:S}} =
         let module MN = (val n : T with type a=int) in
         let module MP = (val p : T with type a=int) in
         X.((MN.interp {{X:S}})+(MP.interp {{X:S}})
      end
    end in
    (module M : T with type a = int)

  let if_ (type w) b (t:w t) (e:w t) =
    let module M = struct
      type a = w

      let interp {{X:S}} =
        let module MB = (val b : T with type a=bool) in
        let module MT = (val t : T with type a=w) in
        let module ME = (val e : T with type a=w) in
        X.if_ (MB.interp{{X:S}}) (MT.interp{{X:S}}) (ME.interp{{X:S}})
    end in
    (module M : T with type a = w)
end

The code could be shrinked even more dramatically if we were allowed to
define [Expr.t] directly as

type 'a t = (X:S) => 'a t

But I doubt it would be easy to make that possible. In my proposition, this
is the same as

type 'a t = (X:S) => 'b t

Which is unfortunate, but at least is quite compatible with how first-class
modules are dealt with in the current versions of OCaml.


--
Arnaud

[-- Attachment #2: Type: text/html, Size: 6186 bytes --]