Re: [Haskell-cafe] Haskell's type system

On 6/18/08, Edsko de Vries 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