[Haskell-cafe] Haskell's type system

[Ryan Ingram]

On 6/18/08, Edsko de Vries <devriese at cs.tcd.ie> wrote:
> Regarding type classes, I'm not 100% what the logical equivalent is,
> although one can regard a type such as
>
>  forall a. Eq a => a -> a
>
> as requiring a proof (evidence) that equality on a is decidable. Where
> this sits formally as a logic I'm not sure though.

You can take the minimalist view and treat a typeclass parameter as an
explicitly passed dictionary; that is:
   (Eq a => a -> a)
is isomorphic to
   (a -> a -> Bool, a -> a -> Bool) -> a -> a

In fact, this is basically what GHC does.

You then treat an instance declaration:
   instance Eq Int where
      (==) = eqInt#
      (/=) = neqInt#
as just a constant
   Eq_Int = (eqInt#, neqInt#)

  -- ryan