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 8CD0D820A1 for ; Mon, 12 Aug 2013 09:45:52 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel@kerneis.info) identity=pra; client-ip=176.31.113.173; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel@kerneis.info"; x-sender="gabriel@kerneis.info"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gabriel@kerneis.info designates 176.31.113.173 as permitted sender) identity=mailfrom; client-ip=176.31.113.173; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel@kerneis.info"; x-sender="gabriel@kerneis.info"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of postmaster@wanbli.kerneis.info designates 176.31.113.173 as permitted sender) identity=helo; client-ip=176.31.113.173; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel@kerneis.info"; x-sender="postmaster@wanbli.kerneis.info"; x-conformance=sidf_compatible; x-record-type="v=spf1" X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ag4FAImRCFKwH3Gt/2dsb2JhbABaFoJPITXAQBZ0glILAQ0BATg7NAUoiEUDCKQGhEcBBY0ZAgSNY4J1gwV2jluJC4YdizWDHA X-IPAS-Result: Ag4FAImRCFKwH3Gt/2dsb2JhbABaFoJPITXAQBZ0glILAQ0BATg7NAUoiEUDCKQGhEcBBY0ZAgSNY4J1gwV2jluJC4YdizWDHA X-IronPort-AV: E=Sophos;i="4.89,860,1367964000"; d="scan'208";a="29101007" Received: from wanbli.kerneis.info ([176.31.113.173]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES128-SHA; 12 Aug 2013 09:45:51 +0200 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=kerneis.info; s=wanbli-rsa1; h=Content-Transfer-Encoding:Content-Type:MIME-Version:Message-ID:Subject:To:From:Date; bh=gpUjjdnzZ/f6ny1+MtmktVsjXEW3vUnf4+/HzRU1fYE=; b=K7lkdf+7mzyhkq0caH5Uq3yekFom/deue4eHKnzo+85FOagTcYwe5aQ7BsabG7NOncimv41KtUzDyjhTnAUrxNN985AcS7Xuf3Hc0igHTQpGul2N//lIidLHBULjQBT4LgoXqXH9Ji4rH0w3Xb+UQAMMLThAH+Cf9m/SD6iQXCo=; Received: from [2001:0:53aa:64c:30f1:5ee7:4f07:268c] (helo=wacehi.kerneis.info) by wanbli.kerneis.info with esmtpsa (TLS1.2:DHE_RSA_AES_128_CBC_SHA1:128) (Exim 4.80) (envelope-from ) id 1V8mp3-0004mN-Iv for caml-list@yquem.inria.fr; Mon, 12 Aug 2013 07:45:50 +0000 Received: from gabriel by wacehi.kerneis.info with local (Exim 4.80) (envelope-from ) id 1V8moz-0001Eg-LB for caml-list@yquem.inria.fr; Mon, 12 Aug 2013 08:45:45 +0100 Date: Mon, 12 Aug 2013 08:45:45 +0100 From: Gabriel Kerneis To: caml-list@yquem.inria.fr Message-ID: <20130812074545.GA4646@kerneis.info> MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline Content-Transfer-Encoding: 8bit User-Agent: Mutt/1.5.21 (2010-09-15) X-SA-Exim-Connect-IP: 2001:0:53aa:64c:30f1:5ee7:4f07:268c X-SA-Exim-Mail-From: gabriel@kerneis.info X-SA-Exim-Scanned: No (on wanbli.kerneis.info); SAEximRunCond expanded to false X-Validation-by: gabriel@kerneis.info Subject: [Caml-list] Signature substitution and type parameters Dear all, Is there a concise way to instanciate a module containing a parametric type for a particular value of this type parameter? module type Poly = sig type 'a t val f : 'a t -> 'a t end ;; module type Mono = sig type t val f : t -> t end ;; module PolyM : Poly = struct type 'a t let f x = x end ;; The following works but is tedious when Poly contains many functions instead of only one: module MonoM : Mono = struct open PolyM type t = int PolyM.t let f = PolyM.f end ;; My other attempts so far: # module MonoM : (Mono with type t := int PolyM.t) = PolyM ;; Error: Only type constructors with identical parameters can be substituted. # module MonoM : (Mono with type t = int PolyM.t) = PolyM ;; Error: Signature mismatch: Modules do not match: sig type 'a t = 'a PolyM.t val f : 'a t -> 'a t end is not included in sig type t = int PolyM.t val f : t -> t end Type declarations do not match: type 'a t = 'a PolyM.t is not included in type t = int PolyM.t They have different arities. Is this a fundamental limitation of the typechecker, which would otherwise lead to unsafe behaviour? Note: The initial motivation for doing this was to use Jean-Christophe Filliātre's Hset as a drop-in replacement for OCaml's Set in one of my programs, without having to add type parameters all over the place. https://www.lri.fr/~filliatr/ftp/ocaml/ds/hset.mli.html Kind regards, -- Gabriel