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

[J.Burton at brighton.ac.uk]

At Tue, 15 Jul 2008 10:27:59 -0400,
Jeff Polakow wrote:
> 
> [1  <text/plain; US-ASCII (7bit)>]
> 
> [2  <text/html; US-ASCII (7bit)>]
> 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.
> 
>