Re: [Caml-list] GADTs and associative container

[Leo White <lpw25@cam.ac.uk>]

Lukasz Stafiniak <lukstafi@gmail.com> writes:

> 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.

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,

>       let create : type a b . int -> (a b, a) t =
>                      fun x -> Hashtbl.create x

could be written as:

  module Create (B: sig type 'a t end) = struct
    let f x : ('a B.t, 'a) Hashtbl.t = 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