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

At Tue, 15 Jul 2008 10:27:59 -0400, Jeff Polakow wrote:
[1
] [2
] Hello, data LSet t where Nil :: LSet Nil Ins :: (Member a t b , If b t (a ::: t) r) => L a -> LSet t -> LSet r
Try replacing both original occurrences of r, i.e. (untested)
Ins :: (Member a t b, If b t (a ::: t) (LSet r)) => L a -> LSet t -> LSet r
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. In the function `insertChar' below I want the type LSetBox to be opaque (i.e. it will be called by users who don't need to know about the fancy types): data LSet t where Nil :: LSet Nil Ins :: (Member a t b , If b t (a ::: t) (LSet r)) => L a -> LSet t -> LSet r -- I have to supply a type for `insert' now and it must include the constraints insert :: (Member a t b , If b t (a ::: t) (LSet r)) => L a -> LSet t -> LSet r insert = Ins --insertChar (and the boxing) doesn't work insertChar :: Char -> LSetBox -> LSetBox insertChar c (LSetBox s) = case fromChar c of LBox t -> LSetBox (insert t s) The error: Could not deduce (If b t1 (a ::: t1) (LSet t), Member a t1 b) from the context () arising from a use of `insert' at /home/jim/sdf-bzr/dsel/TF/Set-July08.hs:54:25-34 Possible fix: add (If b t1 (a ::: t1) (LSet t), Member a t1 b) to the context of the constructor `LBox' or add an instance declaration for (If b t1 (a ::: t1) (LSet t)) In the first argument of `LSetBox', namely `(insert t s)' In the expression: LSetBox (insert t s) In a case alternative: LBox t -> LSetBox (insert t s) Failed, modules loaded: none. Jim
-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.

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.
participants (2)
-
J.Burton@brighton.ac.uk
-
Jeff Polakow