[Haskell-cafe] Type level sets with GADTs, fundeps etc

[Jeff Polakow]

Hello,

> Thanks. This sort of works, but shifts the problem to another context. 
Now it
> 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 
type.

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 (
http://homepages.cwi.nl/~ralf/OOHaskell/)

-Jeff



---

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...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20080717/52faa450/attachment.htm