Type Families and enhanced constraints (at run-time)
haskell at brecknell.org
Fri Nov 30 20:33:45 EST 2007
> > 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.
To do what you are trying to do, it seems that you would also need to be
able to write a function whose return type depended on a simple
foo :: Char -> ???
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,
More information about the Glasgow-haskell-users