Type Families and enhanced constraints (at run-time)

[Jim Burton]

Hi, I hope this is the right place to ask about working with type
families...I want to make a library of Set operations that carries
proofs at the type level, e.g. to make things like this possible,

> insert :: Member e s' T => e -> Set s -> Set s'
> union  :: Union s t u => Set s -> Set t -> Set u

The trouble is designing the Set datatype so it can be used in type
constraints *and* in run-time functions....Something similar is of
course possible with fun deps, and I knocked something up following the
example of Conrad Parker's 'Instant Insanity' but, crucially, that code
is 'trapped' in the type system with no populated types. I want
term-level/run-time functions with enhanced constraints, such as in the
example Manuel posted in haskell-cafe:

> data Z
> data S a
>
> data SNat n where
>     Zero :: SNat Z
>     Succ :: SNat n -> SNat (S n)
>
> zero = Zero
> one  = Succ zero
>
> type family (:+:) n m :: *
> type instance Z :+: m     = m
> type instance (S n) :+: m = S (n :+: m)
> 
> add :: SNat n -> SNat m -> SNat (n :+: m)
> add Zero m     = m
> add (Succ n) m = Succ (add n m) 

This seems like "the best of both worlds" -- maybe it could be a general
strategy for making for making these enhanced constraints at the
term-level? Make a (populated) GADT and parameterise it with a phantom
type (perhaps amongst other things). Make a type operator that can be
used to express the constraint on the phantom types carried around by
the "regular" populated type. When the type operator appears in the
codomain of the function it's a compile-time check on the implementation
of that function and when in the domain it checks the user at run-time.

However, (SNat n) can be put very succinctly because it doesn't need to
carry a value around other than the Peano number in the phantom type.
What about Sets? In my case the values in the sets are just labels and
could well be empty:

> data A ; data B ; data C

And I also need to express the cons-ness -- I don't think that needs
fancy constraints so it can be done with terms, e.g., an underlying
sequence such as in the Collects example. Generally I need to work out
what needs to be run-time and what compile-time but I think that would
follow from getting the combinations of types and terms in the Set
abstraction right...could someone give me a pointer with this?

Many thanks,

Jim