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

[J.Burton at brighton.ac.uk]

At Tue, 15 Jul 2008 09:43:40 -0400,
Jeff Polakow wrote:
> Hello,

Hi Jeff,

> 
> > data LSet t where
> >     Nil :: LSet Nil
> >     --either add the new element or do nothing
> >     Ins :: (Member a t b
> >           , If b (LSet t) (LSet (a ::: t)) r)
> >           => L a -> LSet t -> r
> >
> The constructor Ins needs to return an LSet. Maybe try replacing occurrences of r with (LSet r).
> 

I expected that r would be an LSet, as its the output of If which
returns its 2nd or 3rd argument:

class If p x y z | p x y -> z
    where if' :: p -> x -> y -> z
instance If T x y x 
instance If F x y y 

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.
> 
>