Type Families and enhanced constraints (at run-time)

[Jim Burton]

On Fri, 2007-11-30 at 13:37 +1100, Manuel M T Chakravarty wrote:
> Whenever you want to maintain type-level assertions of properties of  
> you functions, you need to decide *how much* of the value-level  
> information do you need on the type level to express and check the  
> properties that you are interested in.  

Hope you don't mind me going back to this point Manuel; given that I
want to maintain enough type-level information to provide correctness
checks on the implementations of set operations and on their inputs, is
this _impossible_ except at the extreme end of the spectrum? As you say
below, I was hoping this would not be the case and that it would be
possible to create something with those properties that could be used in
an interactive setting. Your SNat example is a simpler case, but it
pulls off that feat, which made me think it was a question of finding
the right combination of types.

Jim

> My SNat example was at one  
> extreme end of the spectrum: *complete* value-level information is  
> reflected at the type level.  In other case, it is only necessary to  
> reflect partial information; eg, when reasoning about bounds-checks of  
> bounded lists or arrays, only the length, but not the exact elements  
> need to be reflected.
> 
> 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?
> 
> 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
>