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

[Nicholls, Mark]

> > 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:

ok

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

My compiler doesn't like this...." A newtype constructor cannot have an
existential context," 

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

Not so sure I understand the difference here..... 

> 
> 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 :-).

Makes little sense to me...."Numeric" looks reasonable...I think...
"Numeric'"...seems weird....and I'm not sure I understood the
explanation.

> 
> > 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.

Ooo blimey....that sort of makes sense.


> 
> > 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