[Haskell-cafe] Quantification in Instance Contexts

[Julian K. Arni]

Ah, but yes, now I see what you mean by CWA. I was thinking in terms of 
instance declarations, but you mean 'types'. That makes sense.

Pity, it would have been fun!

On Thu, Jun 26, 2014 at 02:08:24AM -0700, Andras Slemmer wrote:
> Your second example shouldn't (and doesn't) compile, as the IsNotFirst
> instance has an ambiguous variable 'b'. What you want is this 'b' to be
> existentially quantified and have the compiler provide a witness for it.
> 
> Again, Haskell doesn't have a closed world of types. Even if the compiler
> doesn't find a 'b' in say the current module it cannot refute an IsNotFirst
> constraint, as an IsAfter instance may be defined in another module.
> 
> module A where
> weirdId :: IsNotFirst a => a -> a
> weirdId = id
> 
> Should this compile if we don't have an IsAfter instance in the current
> module? What if we define one in module B which imports module A? What if
> we have two IsAfter instances? Which instance should it use?
> 
> > adding extra instance declarations can 'change the truth-value' of the
> right-hand side.
> 
> No, they cannot. instance (IsSecond a) => IsNotFirst a translates to
> (\forall a. IsSecond(a) -> IsNotFirst(a)), which will always hold. (Unless
> you switch on overlappinginstances which you shouldnt)
> 
> 
> On 25 June 2014 23:06, Julian Arni <jkarni at gmail.com> wrote:
> 
> > 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.
> >>
> >>
> >>
> >>