[Haskell-cafe] Typeclasses and GADT [Was: Regular Expressions without GADTs]

[oleg at pobox.com]

Ralf Hinze wrote:
> To me replacing a GADT by class and instance declarations seems the
> wrong way round. We should not forget that the DT in GADT stands for
> `data type'.

Francois Pottier enumerated some problems with type inference of GADT
code during his ICFP'05 invited talk. Various extensions turn out
necessary, such as local inference, shape inference, ad hoc
elaboration. GADT implementation in GHC 6.4 uses a different
extension, wobbly types. However well these new type system extensions
may work on their own, they must co-exist with the other features of
the language, in particular type classes. The lifting of type class
constraints out of the clauses that pattern-match GADT might no longer
be a good idea: legitimate code can no longer type check because the
combined constraints are contradictory. One may think that GADTs
subsume the regular algebraic data types (ADT), but they do not:
irrefutable pattern matching is not possible with GADT in their
current implementation. Otherwise, unsoundness ensues. One may feel
that type classes are more mature and safer.

> One could certainly argue that the gist of functional programming is
> to define a collection of data types and functions that operate on
> these types. The fact that with GADTs constructors can have more
> general types just allows us to use the functional design pattern more
> often

It seems that type classes offer just the same programming pattern,
only more type-explicit. Indeed, we can compare code that
pattern-match over GADT

 > empty :: RegExp tok a -> Maybe a
 > empty Zero         = mzero
 > empty (Plus r1 r2) = (return Left  `ap` empty r1) `mplus`
 >                      (return Right `ap` empty r2)


with the corresponding type-class based code:

> instance RegExp Zero tok Empty where
>     empty  _ _ = mzero
> instance (RegExp r1 tok a, RegExp r2 tok b) 
>     => RegExp (Plus r1 r2) tok (Either a b) where
>     empty (Plus r1 r2) t = (liftM Left  $ empty r1 t) `mplus`
>                            (liftM Right $ empty r2 t)

which does essentially the same pattern-match, and which also
associates constraints with various alternatives. Because
typeclass-based pattern-matching is `type explicit', we get a better
feedback from the typechecker. For example, `type-pattern-match'
failure becomes a type error rather than a run-time error. The
typeclass-based `pattern matching' is also more expressive, because we
can match on higher-order types and the patterns may be non-linear.
Regular-expression `patterns' implemented with the help of type
classes have more explicit types, e.g.,

  *RX> :t p
  p :: Star (Mult (Star (Check Char)) (Star (Check Char)))

We can easily extend these types with Digit, Alphabetic, etc.

I'm glad Martin Sulzmann mentioned extensibility. The day after the
generic value parser code was posted, Huong Nguyen asked to extend it
for his particular data type:

> data HType = 
>     C1
>     { x :: [String]
>     , y :: HType}
>  | C2 {x1 :: String}
>  | C3 {y1 :: Bool} deriving Show

The extension was quite straightforward and required no modifications
to the previously written code:

> instance Type HType where parse = parseHType
> instance Type Bool  where parse = reads
>
> parseHType  
>     =   readParen True (C1   <$$> (parseList (unStr <$> parse),parse))
>     <+> C2   <$> (unStr <$> parse)
>     <+> C3   <$> parse
>
> (f <$$> (p1,p2)) s  =  [ (f a b, t') | (a, t) <- p1 s, (b,t') <- p2 t ]


Ralf Hinze wrote:
> freeing us from the need or temptation
> to resort to type class hackery with multiple parameter type
> classes, undecidable instances, functional dependencies etc.

Incidentally none of the parsing code posted recently used
undecidable instances let alone functional dependencies. Some of the
pieces of code under discussion was Haskell98.

One should note that P. J. Stuckey and Martin Sulzmann's paper ``A
theory of overloading'' (the journal version) has formalized
multi-parameter type classes with functional dependencies and even
overlapping instances, and developed their meta-theory. The paper
proved various useful properties such as coherence. One can't help but
recall the saying by John Reynolds that the pointer XORing trick is no
longer a disgusting hack because he had a clean proof of correctness
for it.

   Multi-parameter type classes with functional dependencies and
   overlapping instances are not a hack!!

Conor McBride wrote:
> So what's the point? GADTs are a very convenient way to provide data
> which describe types. Their encoding via type classes, or
> whatever, may be possible, but this encoding is not necessarily as
> convenient as the GADT.

First of all, the precise relationship between GADTs and the
typeclasses may be a legitimate topic. Do GADTs bring new expressive
power or mere convenience? Another interesting question concerns
type-checking: if GADTs are so closely related with type classes,
there may exist a deep relationship between typeclass overloading
resolution (a quite mature topic) and wobbly types, shape inference,
etc.

I never argued about convenience of GADTs. They can be quite handy
when dealing with existentials: GADT embody a safe cast and so spare
us form writing the boring casting code ourselves. And perhaps this is
the only compelling case for GADTs.