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