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.