Type level sets with GADTs, fundeps etc

[J.Burton-2]

I have a problem with applying a type constraint in the
constructor of a GADT...I wrote some type level code for sets
using empty types and fundeps, along the lines of Conrad Parker's
Instant Insanity and Oleg's Lightweight Static Resources. At this
level things works OK so I have empty types A, B ... Nil with an
infix cons (:::) and fundeps determining constraints like Member,
Disjoint etc. (Links to code at the end of message.) Then I can
evaluate:

> :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.
I got some help with this and existential boxing seems to be the
answer. I got a version that uses this strategy working OK until it
comes to applying constraints (e.g. Member, needed when inserting an
element). My problem is below. Here's one with no constraints that
will type-check:

----------------------
{-box for labels -}
data LBox = forall a. LBox (L a)
{-box for sets of labels-}
data LSetBox = forall t. LSetBox (LSet t)
{-sets of labels -}
data LSet t where
    Nil :: LSet Nil
    -- 'dumb' insertion
    Ins :: L a -> LSet t -> LSet (a ::: t)
insert = Ins

empty :: LSetBox
empty = LSetBox Nil
 
{-take a Char into a boxed LSet-}
insertChar :: Char -> LSetBox -> LSetBox
insertChar c (LSetBox s) =
    case fromChar c of
      LBox t -> LSetBox (insert t s)
 
{-populate a box-}
fromChar :: Char -> LBox
fromChar 'A' = LBox AL
{- ... B, etc -- use Template Haskell to generate alphabet and the
   various instances needed? -}
fromChar _   = error "fromChar: bad Char"
------------------------

With some Show instances then I can evaluate

> insertChar 'A' empty
LSet {A,}

But what about constraints on the Ins constructor, e.g. on insertion,
ignore elements that are already there:

---------------------
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
insert = Ins

[...]

class Member x ys b | x ys -> b
    where member :: x -> ys -> b

instance Member x Nil F
instance (Eq x y b', Member x ys m, If b' T m b) =>
    Member x (y:::ys) b

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

---------------------

But this evidently isn't the way to use fundeps -- here's
the error:

Malformed constructor result type: r
    In the result type of a data constructor: r
    In the data type declaration for `LSet'
Failed, modules loaded: none.

(The other place I tried putting the constraints is in the type
of `insert' rather than the Ins constructor...)

How can I express this constraint? BTW, I would rather be using type
families for this, for forward compatibility and their greater
generality, so if I can also get round this with them I'd love to
know how...

Thanks, and sorry for the long post!

Jim

[1] Purely type level version: http://jim.sdf-eu.org/TypeLevelSets2.hs
[2] Interactive version using GADTs/Existential boxing: http://jim.sdf-eu.org/Set-July08.hs 
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Jeff Polakow]

Hello,

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

-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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[J.Burton-2]

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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Jeff Polakow]

Hello,

> > > 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
>
Type classes are open so there is nothing to prevent you from adding another instance for If, perhaps in a different module, which returns some arbitrary type.

-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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[J.Burton-2]

At Tue, 15 Jul 2008 10:02:23 -0400,
Jeff Polakow wrote:
[...]
> >
> Type classes are open so there is nothing to prevent you from adding another
> instance for If, perhaps in a different module, which returns some arbitrary
> type.

I see what you mean...so I tried to make Ins return an LSet of
"something", like this:

data LSet t where
    Nil :: LSet Nil
    Ins :: (Member a t b
          , If b t (a ::: t) r)
          => L a -> LSet t -> LSet r

/home/jim/sdf-bzr/dsel/TF/Set-July08.hs:44:9:
    No instance for (If b t (a ::: t) r)
      arising from a use of `Ins'
                   at /home/jim/sdf-bzr/dsel/TF/Set-July08.hs:44:9-11
    Possible fix: add an instance declaration for (If b t (a ::: t) r)
    In the expression: Ins
    In the definition of `insert': insert = Ins

/home/jim/sdf-bzr/dsel/TF/Set-July08.hs:68:6:
    Inferred type is less polymorphic than expected
      Quantified type variable `a' is mentioned in the environment:
        insert :: L a -> LSet t -> LSet r
          (bound at /home/jim/sdf-bzr/dsel/TF/Set-July08.hs:44:0)
    When checking an existential match that binds
        t :: L a
    The pattern(s) have type(s): LBox
    The body has type: LSetBox
    In a case alternative: LBox t -> LSetBox (insert t s)
    In the expression:
        case fromChar c of LBox t -> LSetBox (insert t s)
Failed, modules loaded: none.

>
> -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.
> [2  <text/html; US-ASCII (7bit)>]
>

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Jeff Polakow]

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

-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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[J.Burton-2]

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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe