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@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users