Re: [Caml-list] GADTs and associative container

[Lukasz Stafiniak <lukstafi@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 1115 bytes --]

On Tue, Jul 9, 2013 at 10:43 PM, Goswin von Brederlow <goswin-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 = 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.

[-- Attachment #2: Type: text/html, Size: 1713 bytes --]