Re: [Caml-list] GADTs and associative container

[Alain Frisch <alain@frisch.fr>]

Hi,

This thread might of interest to you:
https://sympa.inria.fr/sympa/arc/caml-list/2013-02/msg00037.html


Alain


On 07/09/2013 10:52 PM, Lukasz Stafiniak wrote:
> On Tue, Jul 9, 2013 at 10:43 PM, Goswin von Brederlow <goswin-v-b@web.de
> <mailto: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.