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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 92D7D7F89E for ; Thu, 3 Apr 2014 18:52:36 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=pra; client-ip=131.111.8.151; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=mailfrom; client-ip=131.111.8.151; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@ppsw-51.csi.cam.ac.uk) identity=helo; client-ip=131.111.8.151; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="postmaster@ppsw-51.csi.cam.ac.uk"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AhsEAHSRPVODbwiXgWdsb2JhbABYg0HETYEfFg4BARYmKIIlAQEBAgEBJxM/BQsLISUPAQRDBi6HVggNyDuGXxMEjnGEPwSuSg X-IPAS-Result: AhsEAHSRPVODbwiXgWdsb2JhbABYg0HETYEfFg4BARYmKIIlAQEBAgEBJxM/BQsLISUPAQRDBi6HVggNyDuGXxMEjnGEPwSuSg X-IronPort-AV: E=Sophos;i="4.97,788,1389740400"; d="scan'208";a="66276890" Received: from ppsw-51.csi.cam.ac.uk ([131.111.8.151]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 03 Apr 2014 18:52:20 +0200 X-Cam-AntiVirus: no malware found X-Cam-ScannerInfo: http://www.cam.ac.uk/cs/email/scanner/ Received: from kingston.cl.cam.ac.uk ([128.232.64.15]:44811) by ppsw-51.csi.cam.ac.uk (smtp.hermes.cam.ac.uk [131.111.8.159]:587) with esmtpsa (PLAIN:lpw25) (TLSv1.2:DHE-RSA-AES128-SHA:128) id 1WVksG-0005XX-Y4 (Exim 4.82_3-c0e5623) (return-path ); Thu, 03 Apr 2014 17:52:20 +0100 From: Leo White To: "Raphael 'kena' Poss" Cc: caml-list@inria.fr References: X-Face: "XWxb[u_Z\PA_Y?9@|IA!!+jTb(/290-*ea/Un$I0B98.$n%eL.;2w*,z]WR#T:,p[ NBd++M7l]#7zj7!{~iw $W-"/=|dVjhT[D{4~gE}gK<2`.6fs!;uqqud]vs2N/3^m7{aS1V, Date: Thu, 03 Apr 2014 17:52:20 +0100 Message-ID: User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.4 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Subject: Re: [Caml-list] Polymorphic module type constraints > To show what I want, here is an example that "works fine" but uses regular types: > > module type Eq = sig > type t > val (=) : t -> t -> bool > val (<>) : t -> t -> bool > end > > let makeEq (type a) eq = > let module S = struct > type t = a > let (=) = eq > let (<>) x y = not (x = y) > end > in (module S : Eq with type t = a) > > (* val eq1: int -> int -> bool *) > let eq1 a b = (a mod 3) = (b mod 3) > module Eq1 = (val makeEq eq1) > > Here, I encounter the first issue: > > (* val eq2: 'a option -> 'a option -> bool *) > let eq2 a b = match (a, b) with > | (None, None) -> true > | (Some x, Some y) -> x = y > | _ -> false > > module Eq2 = (val makeEq ~eq2) > > => > Error: The type of this packed module contains variables: > (module Eq with type t = 'a option) > > Is there any way to generalize? It is not clear what module type you expect `Eq2` to have. The following type does not make any sense: sig type t = 'a option val (=) : t -> t -> bool val (<>) : t -> t -> bool end because the type variable `'a` is not bound. On the other hand: sig type 'a t = 'a option val (=) : 'a t -> 'a t -> bool val (<>) : 'a t -> 'a t -> bool end is not an instance of `Eq` which is the module type of `makeEq eq1`. In addition `makeEq eq2` has type `(module Eq with type t = '_a option)`. Note that the type variable '_a is weakly polymorphic. This is due to the value restriction: `makeEq` may create some state which is used in its returned module, meaning it cannot safely be polymorphic. > My first try: > > let makeMappable1 (type s) (module O : Poly with type t = s) map = > let module S : Mappable with type 'a t = 'a O.t = struct > include O > let map : ('a -> 'b) -> 'a t -> 'b t = map > end > in (module S) > > => > Error: In this `with' constraint, the new definition of t > does not match its original definition in the constrained signature: > Type declarations do not match: type t is not included in type 'a t > > Ok, fair enough: > > let makeMappable2 (type s) (module O : Poly with type 'a t = s) map = > let module S : Mappable with type 'a t = 'a O.t = ... > > => > Error: Syntax error: module-expr expected. (location: with type ... on first line) > > So, I try to fix this with: > > let makeMappable3 (module O : Poly) map = > let module S : Mappable with type 'a t = 'a O.t = struct > include O > let map : ('a -> 'b) -> 'a t -> 'b t = map > end > in (module S) > > => > Error: This expression has type ('a -> 'b) -> 'a O.t -> 'b t > but an expression was expected of type ('a -> 'b) -> 'a O.t -> 'b t > The type constructor O.t would escape its scope > > Any suggestion as to how to define makeMappable? The function `makeMappable` that you are trying to write is polymorphic in a type constructor (`O.t`), in other words it is higher-kinded. The core OCaml type system does not support higher-kinded polymorphism, and the traditional solution is to use functors: module MakeMappable (O : Poly) (M : Mappable with type 'a t := 'a O.t) = struct type 'a t = 'a O.t let map = M.map end Of course, this particular functor is pretty redundent. (A possible alternative is to use the higher library with the approach described in: https://github.com/ocamllabs/higher/raw/paper/higher.pdf) Regards, Leo