[Haskell-cafe] Quantification in Instance Contexts

[Andras Slemmer]

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.
>>
>>
>>
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140626/f80bec89/attachment.html>