Type Families and enhanced constraints (at run-time)

[Manuel M T Chakravarty]

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