Type Families and enhanced constraints (at run-time)
Jim Burton
jb162 at brighton.ac.uk
Fri Nov 30 11:17:00 EST 2007
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
>
More information about the Glasgow-haskell-users
mailing list