Type Families and enhanced constraints (at run-time)

[Jim Burton]

On Fri, 2007-11-30 at 13:37 +1100, Manuel M T Chakravarty wrote:
[...]
> 
> In other words, first you need to decide what properties you want to  
> enforce and what information you need to decide those properties.   
> Coming back to your set example, what properties do you want to  
> enforce/check and what information do you need to do that?  In the  
> extreme case, you could reflect the entire contents of each set at the  
> type-level using a singleton set type (and corresponding singleton  
> types for the set elements).  However, that also would mean that all  
> your value-level set operations will already have to be completely  
> executed by the type checker at compile time, which is probably not  
> what you want.
> 
> Does this make sense?
> 
Yes, and thanks for your reply. What I really need are both ends of the
spectrum! It's reasoning with these sets that is important to me and the
contents are arbitrary, so operations on them should become
proof-carrying code, but they should be "constructable" at run-time.
This will obviously require that two sets with different elements have
different types so I thought about carrying around the extra info
alongside the regular collection:

> data N ; data A tail ; data B tail
> 
> data TInfo t where
>     Nil  :: TInfo N
>     InsA :: TInfo t -> TInfo (A t)
>     InsB :: TInfo t -> TInfo (B t)
> 
> empty = Nil
> a_empty = InsA empty
> 
> data Set t a = Set (TInfo t) [a]

So a value of type Set t Char might have the type "Set (TInfo (A (B N)))
['a', 'b']" and I can start creating type families to enforce
constraints. But this doesn't work:
 
> insert :: Char -> Set t Char -> Set t Char
> insert c (Set tinfo cs) = case c of
>                             'A' -> Set (InsA tinfo) (c:cs)
>                             _   -> error "not a label"

gives me the error:
>    Occurs check: cannot construct the infinite type: t = A t
>     When generalising the type(s) for `insert'
> Failed, modules loaded: none.

I can see why that would be, but what type should the final t be? Is
there a way to get round it or is this type of thing restricted to the
type-level only?

Thanks,

Jim

> Manuel
> 
> 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
> >
> > _______________________________________________
> > Glasgow-haskell-users mailing list
> > Glasgow-haskell-users at haskell.org
> > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>