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 5FE7E81792 for ; Tue, 9 Jul 2013 22:52:42 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lukstafi@gmail.com) identity=pra; client-ip=209.85.212.53; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lukstafi@gmail.com"; x-sender="lukstafi@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of lukstafi@gmail.com designates 209.85.212.53 as permitted sender) identity=mailfrom; client-ip=209.85.212.53; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lukstafi@gmail.com"; x-sender="lukstafi@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-vb0-f53.google.com) identity=helo; client-ip=209.85.212.53; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lukstafi@gmail.com"; x-sender="postmaster@mail-vb0-f53.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ApYBAIt33FHRVdQ1k2dsb2JhbABbhAjBEIESCBYOAQEBAQcLCwkUBCSCIwEBBAEnGQEbHQEDAQsGBQQHOyIBEQEFARwGE4d8AQMJBpxjjE6Cf4Q3ChknDRVDh3MBBQyPXweDdAOXVI9kFimEOTo X-IPAS-Result: ApYBAIt33FHRVdQ1k2dsb2JhbABbhAjBEIESCBYOAQEBAQcLCwkUBCSCIwEBBAEnGQEbHQEDAQsGBQQHOyIBEQEFARwGE4d8AQMJBpxjjE6Cf4Q3ChknDRVDh3MBBQyPXweDdAOXVI9kFimEOTo X-IronPort-AV: E=Sophos;i="4.87,1030,1363129200"; d="scan'208";a="20564828" Received: from mail-vb0-f53.google.com ([209.85.212.53]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 09 Jul 2013 22:52:41 +0200 Received: by mail-vb0-f53.google.com with SMTP id p12so4722158vbe.40 for ; Tue, 09 Jul 2013 13:52:40 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=bZj8tjozASfXPdZBT4aIti3XHXqwo76h6JskBsgrQkA=; b=BOTHDEN/CTuVVCp3bRilR/cEUaMpdlKgqBqUxPiyPy7dOB01pNAk+lNXAJeuwWPY+1 OE+tgFg8/Su7wV0JvUmASRAuiB7t4tYycr1dx/UdqeVG1rfP2OfSE92C34yM7lhOkRCY /c7yjZ6V7ixz7ZCvxWvYujhCmjB7vnMoMgZ5eYd9taz0Axmzau8Girbc3TR5/E1GxUYH 79HNTsOIthOzBhMGn5GKkKp8XTpabNxew3vUS+YiI3xmad2epb47/HxI/t47LlpLtYxQ 2XYdWF0AFKEJXWEKZaHpwvXIfG+WnLMQxvpgEEyNbIynQm3Vgqf1GpxH8m11FY8oI1Sh KIfQ== X-Received: by 10.52.17.115 with SMTP id n19mr14356290vdd.113.1373403160364; Tue, 09 Jul 2013 13:52:40 -0700 (PDT) MIME-Version: 1.0 Received: by 10.58.226.231 with HTTP; Tue, 9 Jul 2013 13:52:20 -0700 (PDT) In-Reply-To: <20130709204312.GA30194@frosties> References: <20130709204312.GA30194@frosties> From: Lukasz Stafiniak Date: Tue, 9 Jul 2013 22:52:20 +0200 Message-ID: To: Goswin von Brederlow Cc: Caml Content-Type: multipart/alternative; boundary=bcaec502dc2682013f04e11a57d3 Subject: Re: [Caml-list] GADTs and associative container --bcaec502dc2682013f04e11a57d3 Content-Type: text/plain; charset=ISO-8859-1 On Tue, Jul 9, 2013 at 10:43 PM, Goswin von Brederlow wrote: > Hi, > > I'm wondering if one can have an ascociative container, like a Hashtbl.t > with dependent types (GADTs as the key, value depending on the key). > Something like this: > > module H = struct > type ('a, 'b) t = ('a, 'b) Hashtbl.t > let create : type a b . int -> (a b, a) t = > fun x -> Hashtbl.create x > let add : type a b . (a b, a) t -> a b -> a -> unit = > fun h k v -> Hashtbl.add h k v > let find : type a b . (a b, a) t -> a b -> a = > fun h k -> Hashtbl.find h k > end > > BUT: > > let create : type a b . int -> (a b, a) t = > ^^^ > 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 example you can write code that only depends on the type class of "b" (which is parameterized by "a"), and "b" has signature "* -> *" or something like that. --bcaec502dc2682013f04e11a57d3 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
On Tue, Jul 9, 2013 at 10:43 PM, Goswin von Brederlow <go= swin-v-b@web.de> wrote:
Hi,

I'm wondering if one can have an ascociative container, like a Hashtbl.= t
with dependent types (GADTs as the key, value depending on the key).
Something like this:

module H =3D struct
=A0 type ('a, 'b) t =3D ('a, 'b) Hashtbl.t
=A0 let create : type a b . int -> (a b, a) t =3D
=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0fun x -> Hashtbl.create x
=A0 let add : type a b . (a b, a) t -> a b -> a -> unit =3D
=A0 =A0 =A0 =A0 =A0 =A0 =A0 fun h k v -> Hashtbl.add h k v
=A0 let find : type a b . (a b, a) t -> a b -> a =3D
=A0 =A0 =A0 =A0 =A0 =A0 =A0 fun h k -> Hashtbl.find h k
end
=A0
BUT:

=A0 =A0 let create : type a b . int -> (a b, a) t =3D
=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 ^^^=
Error: Unbound type constructor b


Is there some special syntax I'm missing or is it simply impossible to<= br> declare such a container in the abstract?

I think = you need higher kinded types, not GADTs. Haskell has them, for example you = can write code that only depends on the type class of "b" (which = is parameterized by "a"), and "b" has signature "*= -> *" or something like that.
--bcaec502dc2682013f04e11a57d3--