On Sat, 2007-12-01 at 11:33 +1000, Matthew Brecknell wrote: [...]
Seems impossible. With GADTs, you can of course go the other way:
data A data B
data Chr a where AChr :: Chr A BChr :: Chr B
toChar :: Chr a -> Char toChar AChr = 'A' toChar BChr = 'B'
So perhaps insert should have a type something more like:
type family ChrSetIns a t :: *
insert :: Chr a -> ChrSet t -> ChrSet (ChrSetIns a t)
I'm not sure how to make the set type parametric in the element type, though.
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: data A data B data Nil data t ::: ts -- consing the phantom types data Chr a where AChr :: Chr A BChr :: Chr B toChar :: Chr a -> Char toChar AChr = 'A' toChar BChr = 'B' data TInfo t where Nil :: TInfo Nil InsA :: TInfo t -> TInfo (A ::: t) InsB :: TInfo t -> TInfo (B ::: t) data ChrSet t = ChrSet (TInfo t) [Char] type family ChrSetIns c s :: * type instance ChrSetIns (Chr a) (TInfo t) = TInfo (a ::: t) insert :: Chr a -> ChrSet t -> ChrSet (ChrSetIns a t) insert c (ChrSet tinfo cs) = case c of AChr -> ChrSet (InsA tinfo) ((toChar c):cs) _ -> error "not a label" `insert' is still the problem -- how to form the 1st param of ChrSet. (InsA tinfo) isn't an instance of ChrSetIns, but I don't see how to fix that...? The error: ------------------------------------------- Couldn't match expected type `ChrSetIns A t' against inferred type `A ::: t' Expected type: TInfo (ChrSetIns A t) Inferred type: TInfo (A ::: t) In the first argument of `ChrSet', namely `(InsA tinfo)' In the expression: ChrSet (InsA tinfo) ((toChar c) : cs) Failed, modules loaded: none. Thanks, Jim