[Caml-list] First class modules question

[Caml-list] First class modules question

[Neel Krishnaswami]

Hello,

I'm experimenting with Ocaml's first-class modules feature, and
have run into a problem. I have a record type

   type 'a monoid = {unit : 'a; join : 'a -> 'a -> 'a}

and a signature

   module type APPLICATIVE = sig
     type 'a t
     val map : ('a -> 'b) -> 'a t -> 'b t
     val pure : 'a -> 'a t
     val ( $ ) : ('a -> 'b) t -> 'a t -> 'b t
   end

and I would like to write a function which turns a monoid into
an applicative module, as follows:

   let monoid_to_app (type s) (m : s monoid) =
     let module I = struct
       type 'a t = s
       let map _ x = x
       let pure _ = m.unit
       let ($) x y = m.join x y
     end
     in (module I : APPLICATIVE with type 'a t = s)

Here, I want to constrain the type of APPLICATIVE to be the monoid
element type s. However, Ocaml complains with a syntax error, and
looking at the grammar for type constraints, the annotation on I
is a package-type, which only permits constraints using the
package-constraint production

   package-type ::= modtype-path
                 |  modtype-path with package-constraint
                                 {and package-constraint}

   package-constraint ::= type typeconstr =  typexpr

This does not permit a constraint of the form "type 'a t = s",
unlike the module-constraint production of the grammar.

Is this a fundamental limitation on first-class modules, or is it
just a restriction for ease of implementation?

-- 
Neel Krishnaswami
N.Krishnaswami@cs.bham.ac.uk

Re: [Caml-list] First class modules question

[Gerd Stolpmann]

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

Am Donnerstag, den 10.04.2014, 21:14 +0100 schrieb Neel Krishnaswami:
> Hello,
> 
> I'm experimenting with Ocaml's first-class modules feature, and
> have run into a problem. I have a record type
> 
>    type 'a monoid = {unit : 'a; join : 'a -> 'a -> 'a}
> 
> and a signature
> 
>    module type APPLICATIVE = sig
>      type 'a t
>      val map : ('a -> 'b) -> 'a t -> 'b t
>      val pure : 'a -> 'a t
>      val ( $ ) : ('a -> 'b) t -> 'a t -> 'b t
>    end
> 
> and I would like to write a function which turns a monoid into
> an applicative module, as follows:

But you don't mean the applicative functor feature of OCaml, right? This
doesn't work with first class modules. (Just to avoid
misunderstandings.)

>    let monoid_to_app (type s) (m : s monoid) =
>      let module I = struct
>        type 'a t = s
>        let map _ x = x
>        let pure _ = m.unit
>        let ($) x y = m.join x y
>      end
>      in (module I : APPLICATIVE with type 'a t = s)
> 
> Here, I want to constrain the type of APPLICATIVE to be the monoid
> element type s. However, Ocaml complains with a syntax error, and
> looking at the grammar for type constraints, the annotation on I
> is a package-type, which only permits constraints using the
> package-constraint production
> 
>    package-type ::= modtype-path
>                  |  modtype-path with package-constraint
>                                  {and package-constraint}
> 
>    package-constraint ::= type typeconstr =  typexpr
> 
> This does not permit a constraint of the form "type 'a t = s",
> unlike the module-constraint production of the grammar.
> 
> Is this a fundamental limitation on first-class modules, or is it
> just a restriction for ease of implementation?

I guess the problem is that it is unclear/unexpressable then what the
constraint means for 'a. Imagine you had a constraint
type 'a t = 'a list. This would implicitly mean that any 'a works on the
right side (and thus on the left, too). However, as we don't know
anything about the right side, we cannot conclude that in your example.
If e.g. the right side were int list, you could read this as a
constraint 'a=int. This just means that a parameterized constraint can
also constrain the parameter, but we don't have any means to express
that. So I guess this is the reason why it is not supported. (You
probably need a notation like "type 'a t = s where 'a = u".)

Gerd
-- 
------------------------------------------------------------
Gerd Stolpmann, Darmstadt, Germany    gerd@gerd-stolpmann.de
Creator of GODI and camlcity.org.
Contact details:        http://www.camlcity.org/contact.html
Company homepage:       http://www.gerd-stolpmann.de
------------------------------------------------------------

[-- Attachment #2: This is a digitally signed message part --]
[-- Type: application/pgp-signature, Size: 490 bytes --]

Re: [Caml-list] First class modules question

[Raphael 'kena' Poss]

Hi Neel,

check the mailing list archives for the thread "Polymorphic module type constraints" last month: I asked more or less the same question on March 21st, and was enlightened by Leo White's answer on April 3rd. Maybe you will appreciate his answer as well.

Best regards,

-- 
Raphael 'kena' Poss · r.poss@uva.nl
http://staff.science.uva.nl/~poss/