Re: [Caml-list] First class modules question

[Gerd Stolpmann <info@gerd-stolpmann.de>]

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