[Haskell] Conditional typechecking with GADTs

Taral taralx at gmail.com
Wed Dec 28 15:03:07 EST 2005

On 12/27/05, oleg at pobox.com <oleg at pobox.com> wrote:
> data a  :+: bb                          -- Conj assertion a and assertions bb
> data aa :@: bb                          -- Conjunction of assertions aa and bb

Why is the difference here?

> class WellTyped a
> instance WellTyped Nil
> instance WellTyped cs => WellTyped ((a :=: a) :+: cs)
> instance (WellTyped cs1, WellTyped cs2) => WellTyped (cs1 :@: cs2)

Could one not write:

instance WellTyped (a :=: a)

and do away with (:+:)?

Taral <taralx at gmail.com>
"Computer science is no more about computers than astronomy is about
    -- Edsger Dijkstra

More information about the Haskell mailing list