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.