[Haskell-cafe] Type level sets with GADTs, fundeps etc
J.Burton at brighton.ac.uk
J.Burton at brighton.ac.uk
Tue Jul 15 09:25:14 EDT 2008
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
More information about the Haskell-Cafe
mailing list