[Haskell-cafe] confusion about 'instance'....

[Luke Palmer]

On Jan 10, 2008 1:25 PM, Nicholls, Mark <Nicholls.Mark at mtvne.com> wrote:
> Thanks for your response, I think you helped me on one of my previous
> abberations.
>
> Hmmm....this all slightly does my head in....on one hand we have
> types....then type classes (which appear to be a relation defined on
> types)....then existential types...which now appear not to be treated
> quite in the same way as 'normal' types....and in this instance the
> syntax even seems to change....does
>
> "instance Num a => A a"
>
> Mean the same thing as
>
> "instance A (forall a.Num a=>a)"

Uh... that second one is pretty much nonsensical to me.  I could imagine it
meaning the type (forall a.Num a => a) itself is an instance of A, but not
specializations of it (like Int).  But without an identity in the type system,
the meaning of that would be convoluted.  It's kind of off topic, but just
for the interested, here are two similar, legal constructions:

Existential:
newtype Numeric  = forall a. Num a => Numeric a

Universal:
newtype Numeric' = Numeric' (forall a. Num a => a)

Both of which are easily declared to be instances of Num.  They're not what
you want though, because Haskell doesn't support what you want :-(.  Anyway,
if you have a value of type Numeric, you know it contains some value of a
Num type, but you don't know what type exactly (and you can never find out).
If you have a value of type Numeric', then you can produce a value of any Num
type you please (i.e. the value is built out of only operations in the Num
class, nothing more specific).

But that was a digression; ignore at your leisure (now that you've already
read it :-).

> and secondly in what way can this construct lead to "undecidable
> instances"

Okay, read:

instance A a => B b

(where a and be might be more complex expressions) not as "b is an instance of
B whenever a is an instance of A", but rather as "b is an instance of B, and
using it as such adds a constraint of A a".  Let's look at a slightly more
complex (and contrived) example:

class Foo a where
    foo :: a -> a

instance (Foo [a]) => Foo a where
    foo x = head $ foo [x]

Then when checking the type of the expression foo (0::Int), we'd have to
check if Foo Int, Foo [Int], Foo [[Int]], Foo [[[Int]]], ad infinitum.

> What are the instances, and what about them is undecidable....seems
> pretty decidable to me?
>
> What is the ramifications of turning this option on?

Theoretically, compile time fails to guarantee to ever finish.  Practically,
ghc will give you a very-difficult-to-reason-about message when constraint
checking stack overflows.

Luke