Type Families and enhanced constraints (at run-time)
jb162 at brighton.ac.uk
Mon Dec 3 15:24:34 EST 2007
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,
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 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.
More information about the Glasgow-haskell-users