[Haskell-cafe] Quantification in Instance Contexts

[Julian Arni]

Thanks for the reply. I don't quite understand why guessing whether there
is an intermediate type would be so magical, though. Let's simplify:

data A
data B
class IsNotFirst a
class IsAfter b a
instance (IsAfter b a) => IsNotFirst a
instance IsAfter B A


Here we've separated out the ambiguous type issue from the unification.
Note that *already*, if I query with undefined::(IsNotFirst A => a), I get:

  No instance for (IsAfter b A) arising from a use of ‘t’
    The type variable ‘b’ is ambiguous
    Note: there is a potential instance available:
      instance [overlap ok] IsAfter B A

Generally, GHC is doing the work that I wanted it to *in the error
message*. In what sense, then, is this impossible?
  And why is there some inexcusable use of CWA here? Instances already have
(if you squint) a negation-as-failure semantics. "instance (IsAfter b a) =>
IsNotFirst a"  doesn't *in that sense* look that different to me than
"instance (IsSecond a) => IsNotFirst a": adding extra instance declarations
can 'change the truth-value' of the right-hand side.


Thanks again,
   Julian


On Thu, Jun 26, 2014 at 1:58 AM, Andras Slemmer <0slemi0 at gmail.com> wrote:

> Think about what you're asking from the compiler. If it sees a (Path a c)
> constraint it would have to magically guess whether there is an
> intermediate type b for which (Path a b) and (Path b c), which is
> impossible.
>
> Logic programming relies on the closed world assumption, meaning that if a
> statement cannot be proven within the closed world we are working in then
> it is false. Haskell typeclasses don't work like this; there is no closed
> world of types, so the compiler cannot "refute" a constraint.
>
> In prolog you'd have something like this:
> path(A,C) :- path(A,B), path(B,C).
> (havent used prolog for a while so syntax might be off)
>
> If you translate this to first order logic you'd have:
> \forall A,C.(path(A,C) <- \exists B.(path(A,B)^path(B,C)))
>
> It is the existential that is emulated with the cwa and cannot be emulated
> in haskell's typesystem.
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140626/a7ad58da/attachment.html>