Re: [Caml-list] One-value functors

[Arnaud Spiwack <Arnaud.Spiwack@lix.polytechnique.fr>]

[-- 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 --]