[Haskell-cafe] Type level sets with GADTs, fundeps etc
jeff.polakow at db.com
Thu Jul 17 11:17:27 EDT 2008
> Thanks. This sort of works, but shifts the problem to another context.
> seems that I can't hide the extra type information in the existential
> types, which is what I want to do.
I think that you can't abstract over a type context, i.e. you can't expect
type inference to instantiate a type variable to a constrained polymorphic
I get the impression that GADTs are a bit of a distraction for what you
are aiming to do. I'm not sure exactly what you mean by
> > :t insert (undefined::A) (undefined:: A ::: Nil)
> insert (undefined::A) (undefined:: A ::: Nil) :: A ::: Nil
> But what I really want to do is wrap this up so that it can be used
> at runtime, not just in the type-checker, so that (just a sketch)
> I could have
> insert 'A' empty :: Set (A ::: Nil)
> where the runtime value of the set is fully determined by its type.
but it looks like it should be a realtively easy bit of machinery to add
to what you already had.
Also, in case you haven't already seen these, other good sources of type
level programming are the HList paper (
http://homepages.cwi.nl/~ralf/HList/) and the OOHaskell paper (
This e-mail may contain confidential and/or privileged information. If you
are not the intended recipient (or have received this e-mail in error)
please notify the sender immediately and destroy this e-mail. Any
unauthorized copying, disclosure or distribution of the material in this
e-mail is strictly forbidden.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe