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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id DC7D481792 for ; Wed, 10 Jul 2013 11:52:35 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=pra; client-ip=131.111.8.152; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=mailfrom; client-ip=131.111.8.152; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@ppsw-52.csi.cam.ac.uk) identity=helo; client-ip=131.111.8.152; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="postmaster@ppsw-52.csi.cam.ac.uk"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ao0BACQu3VGDbwiYnGdsb2JhbABahxG+B4EQFg4BAQEBAQYNCQkUKIIjAQEEASMEUgULCQIOCgICBSECAg8BBA08E4d9AwkGjF+bQIhADRU2iAaBJotSgjgzB4JWgR8DlW+ODIg4 X-IPAS-Result: Ao0BACQu3VGDbwiYnGdsb2JhbABahxG+B4EQFg4BAQEBAQYNCQkUKIIjAQEEASMEUgULCQIOCgICBSECAg8BBA08E4d9AwkGjF+bQIhADRU2iAaBJotSgjgzB4JWgR8DlW+ODIg4 X-IronPort-AV: E=Sophos;i="4.87,1035,1363129200"; d="scan'208";a="20647654" Received: from ppsw-52.csi.cam.ac.uk ([131.111.8.152]) by mail3-smtp-sop.national.inria.fr with ESMTP; 10 Jul 2013 11:52:35 +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]:43998) by ppsw-52.csi.cam.ac.uk (smtp.hermes.cam.ac.uk [131.111.8.158]:587) with esmtpsa (PLAIN:lpw25) (TLSv1.2:DHE-RSA-AES128-SHA:128) id 1Uwr4c-0001A1-Ei (Exim 4.80_167-5a66dd3) (return-path ); Wed, 10 Jul 2013 10:52:34 +0100 From: Leo White To: Lukasz Stafiniak Cc: Goswin von Brederlow , Caml References: <20130709204312.GA30194@frosties> 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: Wed, 10 Jul 2013 10:52:34 +0100 In-Reply-To: (Lukasz Stafiniak's message of "Tue, 9 Jul 2013 22:52:20 +0200") Message-ID: <87ehb6lp25.fsf@kingston.cl.cam.ac.uk> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.4 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] GADTs and associative container Lukasz Stafiniak writes: > On Tue, Jul 9, 2013 at 10:43 PM, Goswin von Brederlow = wrote: > > Hi, >=20=20=20=20 > I'm wondering if one can have an ascociative container, like a Hashtb= l.t > with dependent types (GADTs as the key, value depending on the key). > Something like this: >=20=20=20=20 > module H =3D struct > =C2=A0 type ('a, 'b) t =3D ('a, 'b) Hashtbl.t > =C2=A0 let create : type a b . int -> (a b, a) t =3D > =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0fun x -= > Hashtbl.create x > =C2=A0 let add : type a b . (a b, a) t -> a b -> a -> unit =3D > =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 fun h k v -> Hashtbl= .add h k v > =C2=A0 let find : type a b . (a b, a) t -> a b -> a =3D > =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 fun h k -> Hashtbl.f= ind h k > end > > =C2=A0 > > BUT: >=20=20=20=20 > =C2=A0 =C2=A0 let create : type a b . int -> (a b, a) t =3D > =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0= =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 ^^^ > Error: Unbound type constructor b > > Is there some special syntax I'm missing or is it simply impossible to > declare such a container in the abstract? > > I think you need higher kinded types, not GADTs. Haskell has them, for ex= ample you can write code that only depends on > the type class of "b" (which is parameterized by "a"), and "b" has signat= ure "* -> *" or something like that. That type is indeed higher-kinded. OCaml does support higher-kinded types but not in the core type system: you need to use functors. For example, > =C2=A0 let create : type a b . int -> (a b, a) t =3D > =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0fun x -= > Hashtbl.create x could be written as: module Create (B: sig type 'a t end) =3D struct let f x : ('a B.t, 'a) Hashtbl.t =3D Hashtbl.create x end;; Note that this is not actually the correct type for writing an associative container. See Jeremy's post for details. Regards, Leo