Type Families and enhanced constraints (at run-time)

[Matthew Brecknell]

Jim Burton said:
> Thanks -- I think I see your point but I'm not sure how to make 
> use of it...(perhaps I'm trying to run before I can walk). 
> The way I was picturing things, the A, B ... types would 
> need to take a parameter so they can be collected/consed, 
> so my next attempt tries to incorporate both ideas:
> 
> [...]

I was imagining something more along the lines of this:

> data A
> data B
> 
> data Chr a where
>   AChr :: Chr A
>   BChr :: Chr B
> 
> toChar :: Chr a -> Char
> toChar AChr = 'A'
> toChar BChr = 'B'
> 
> data Nil
> data t ::: ts
> 
> data ChrSet t where
>   Nil :: ChrSet Nil
>   Ins :: Chr a -> ChrSet t -> ChrSet (a ::: t)
> 
> insert :: Chr a -> ChrSet t -> ChrSet (a ::: t)
> insert = Ins

That, by itself, doesn't require type families. I imagine you'll need
type families if you want to do things like implement a tree structure,
perform membership tests, deletions, etc.

Note that if you want to reason about the correctness of code in this
way, your data structures need to carry proofs. For example, the ChrSet
data type I've given above enforces the correspondence between the
value-level representation and the type-level representation, so given
any ChrSet, I know the type-level decomposition will reflect the
value-level decomposition, regardless of where that ChrSet came from.

On the other hand, the ChrSet you proposed in your previous post doesn't
have this property:

data ChrSet t = ChrSet (TInfo t) [Char]

Given one of these, I can't be confident that the type reflects the
value, without inspecting all of the code that might have contributed to
its construction. And that defeats the purpose of your endeavours. So
you should defer the call to toChar until the last possible moment, if
you call it at all.

Another thought occurred to me: you might want to construct a ChrSet
from user input, which brings us back to the problem I described in my
previous post. All is not lost, though. You'll just need to keep your
Chr and ChrSet values inside existential boxes:

> data ChrBox = forall a . ChrBox (Chr a)
> 
> fromChar :: Char -> ChrBox
> fromChar 'A' = ChrBox AChr
> fromChar 'B' = ChrBox BChr
> fromChar _ = error "fromChar: bad Char"
> 
> data ChrSetBox = forall t . ChrSetBox (ChrSet t)
> 
> insertChar :: Char -> ChrSetBox -> ChrSetBox
> insertChar c (ChrSetBox s) = case fromChar c of
>   ChrBox c -> ChrSetBox (insert c s)

BTW, I think you might get more interesting responses to theses
questions in haskell-cafe.