Quantification in Instance Contexts

newer
ANN: psqueues

older
direct-fastcgi and logging

Julian K. Arni

25 Jun 2014 25 Jun '14

3:16 p.m.

Hi Cafe, I'm playing around with simple logic-programming at the type level. For instance, encoding trees:

...

...
{-# LANGUAGE MultiParamTypeClasses , FunctionalDependencies , FlexibleInstances , UndecidableInstances , FlexibleContexts , OverlappingInstances #-} {-# OPTIONS_GHC -fcontext-stack=100 #-}

-- *A -- / \ -- B* *C -- | -- D*

data A data B data C data D class Child a b bool | a b -> bool instance Child A B TrueT instance Child B D TrueT instance Child B C TrueT class Path a b bool | a b -> bool

Now the following obviously doesn't work (never mind for now that 'Path' needs a recursive definition, and that this is really just 'Grandchild'):

...

...
instance (Child a b TrueT, Child b c TrueT) => Path a c TrueT

Because 'b' is ambiguous. Fair enough. But I can't directly use a fundep, because 'b' *is* in fact ambiguous. What I want to tell the compiler is that it's really okay, since the RHS side (and any possible 'where' expressions) doesn't depend on what is instantiated for 'b'. I know I could switch to a class 'Children a bs bool' and encode all children of as a type-level list, and then have a fundep between 'a' and 'bs'. That's not a *bad* solution: it does give a good sense of the intention. But it's not very extensible; really I'd rather be using something like 'forall' - something, I would guess, along the lines of:

...

...
instance forall a c. (forall b. (Child a b TrueT, Child b c TrueT)) => Path a c TrueT

That, however, fails with: Malformed instance head: (forall b. (Child a b TrueT, Child b c TrueT)) -> Path a c TrueT In the instance declaration for ‘Path a c TrueT’ So: is there a way (presumably with 'forall') of telling the compiler that the ambiguous type 'b' actually won't "leak through" to the RHS, so stop bugging me about ambiguity? Thanks, Julian

Show replies by date

adam vogt

25 Jun 25 Jun

6:36 p.m.

Hi Julian, Does each child have only one parent? In other words, is a larger "tree" still accepted if you use: class Child1 a b bool | a b -> bool, b -> a instead of your Child. Regards, Adam On Wed, Jun 25, 2014 at 5:46 AM, Julian K. Arni wrote:

...

Hi Cafe,

I'm playing around with simple logic-programming at the type level. For instance, encoding trees:

...
...
{-# LANGUAGE MultiParamTypeClasses , FunctionalDependencies , FlexibleInstances , UndecidableInstances , FlexibleContexts , OverlappingInstances #-} {-# OPTIONS_GHC -fcontext-stack=100 #-}

-- *A -- / \ -- B* *C -- | -- D*

data A data B data C data D class Child a b bool | a b -> bool instance Child A B TrueT instance Child B D TrueT instance Child B C TrueT class Path a b bool | a b -> bool

Now the following obviously doesn't work (never mind for now that 'Path' needs a recursive definition, and that this is really just 'Grandchild'):

...
...
instance (Child a b TrueT, Child b c TrueT) => Path a c TrueT

Because 'b' is ambiguous. Fair enough. But I can't directly use a fundep, because 'b' *is* in fact ambiguous. What I want to tell the compiler is that it's really okay, since the RHS side (and any possible 'where' expressions) doesn't depend on what is instantiated for 'b'.

I know I could switch to a class 'Children a bs bool' and encode all children of as a type-level list, and then have a fundep between 'a' and 'bs'. That's not a *bad* solution: it does give a good sense of the intention. But it's not very extensible; really I'd rather be using something like 'forall' - something, I would guess, along the lines of:

...
...
instance forall a c. (forall b. (Child a b TrueT, Child b c TrueT)) => Path a c TrueT

That, however, fails with:

Malformed instance head: (forall b. (Child a b TrueT, Child b c TrueT)) -> Path a c TrueT In the instance declaration for ‘Path a c TrueT’

So: is there a way (presumably with 'forall') of telling the compiler that the ambiguous type 'b' actually won't "leak through" to the RHS, so stop bugging me about ambiguity?

Thanks, Julian _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Julian Arni

7:30 p.m.

Alas, no. I tried to simplify the use case, but in fact the structure is a DAG, and each node may have multiple parents. So neither "a -> b" nor "b -> a" hold. On Wed, Jun 25, 2014 at 3:06 PM, adam vogt wrote:

...

Hi Julian,

Does each child have only one parent? In other words, is a larger "tree" still accepted if you use:

class Child1 a b bool | a b -> bool, b -> a

instead of your Child.

Regards, Adam

...
Hi Cafe,

I'm playing around with simple logic-programming at the type level. For instance, encoding trees:

...
...
{-# LANGUAGE MultiParamTypeClasses , FunctionalDependencies , FlexibleInstances , UndecidableInstances , FlexibleContexts , OverlappingInstances #-} {-# OPTIONS_GHC -fcontext-stack=100 #-}

-- *A -- / \ -- B* *C -- | -- D*

data A data B data C data D class Child a b bool | a b -> bool instance Child A B TrueT instance Child B D TrueT instance Child B C TrueT class Path a b bool | a b -> bool

Now the following obviously doesn't work (never mind for now that 'Path' needs a recursive definition, and that this is really just 'Grandchild'):

...
...
instance (Child a b TrueT, Child b c TrueT) => Path a c TrueT

Because 'b' is ambiguous. Fair enough. But I can't directly use a fundep, because 'b' *is* in fact ambiguous. What I want to tell the compiler is

...
it's really okay, since the RHS side (and any possible 'where' expressions) doesn't depend on what is instantiated for 'b'.

I know I could switch to a class 'Children a bs bool' and encode all children of as a type-level list, and then have a fundep between 'a' and 'bs'. That's not a *bad* solution: it does give a good sense of the intention. But it's not very extensible; really I'd rather be using something like 'forall' - something, I would guess, along the lines of:

...
...
instance forall a c. (forall b. (Child a b TrueT, Child b c TrueT)) => Path a c TrueT

That, however, fails with:

Malformed instance head: (forall b. (Child a b TrueT, Child b c TrueT)) -> Path a c TrueT In the instance declaration for ‘Path a c TrueT’

So: is there a way (presumably with 'forall') of telling the compiler

On Wed, Jun 25, 2014 at 5:46 AM, Julian K. Arni wrote: that that the

...
ambiguous type 'b' actually won't "leak through" to the RHS, so stop bugging me about ambiguity?

Thanks, Julian _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Andras Slemmer

26 Jun 26 Jun

5:28 a.m.

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. On 25 June 2014 07:00, Julian Arni wrote:

...

Alas, no. I tried to simplify the use case, but in fact the structure is a DAG, and each node may have multiple parents. So neither "a -> b" nor "b -> a" hold.

On Wed, Jun 25, 2014 at 3:06 PM, adam vogt wrote:

...
Hi Julian,

Does each child have only one parent? In other words, is a larger "tree" still accepted if you use:

class Child1 a b bool | a b -> bool, b -> a

instead of your Child.

Regards, Adam

...
Hi Cafe,

I'm playing around with simple logic-programming at the type level. For instance, encoding trees:

...
...
{-# LANGUAGE MultiParamTypeClasses , FunctionalDependencies , FlexibleInstances , UndecidableInstances , FlexibleContexts , OverlappingInstances #-} {-# OPTIONS_GHC -fcontext-stack=100 #-}

-- *A -- / \ -- B* *C -- | -- D*

data A data B data C data D class Child a b bool | a b -> bool instance Child A B TrueT instance Child B D TrueT instance Child B C TrueT class Path a b bool | a b -> bool

Now the following obviously doesn't work (never mind for now that 'Path' needs a recursive definition, and that this is really just 'Grandchild'):

...
...
instance (Child a b TrueT, Child b c TrueT) => Path a c TrueT

Because 'b' is ambiguous. Fair enough. But I can't directly use a fundep, because 'b' *is* in fact ambiguous. What I want to tell the compiler is

...
it's really okay, since the RHS side (and any possible 'where' expressions) doesn't depend on what is instantiated for 'b'.

I know I could switch to a class 'Children a bs bool' and encode all children of as a type-level list, and then have a fundep between 'a' and 'bs'. That's not a *bad* solution: it does give a good sense of the intention. But it's not very extensible; really I'd rather be using something like 'forall' - something, I would guess, along the lines of:

...
...
instance forall a c. (forall b. (Child a b TrueT, Child b c TrueT)) => Path a c TrueT

That, however, fails with:

Malformed instance head: (forall b. (Child a b TrueT, Child b c TrueT)) -> Path a c TrueT In the instance declaration for ‘Path a c TrueT’

So: is there a way (presumably with 'forall') of telling the compiler

On Wed, Jun 25, 2014 at 5:46 AM, Julian K. Arni wrote: that that the

...
ambiguous type 'b' actually won't "leak through" to the RHS, so stop bugging me about ambiguity?

Thanks, Julian _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Julian Arni

11:36 a.m.

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

Andras Slemmer

2:38 p.m.

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

Julian K. Arni

7:29 p.m.

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.

That's exactly what I want! Well, modulo actually caring that the witness be provided (of course *that* would raise the 'which one' question). Sorry if that wasn't clear.

...

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?

I understand the general problem of ambiguous types, but my point was that sometimes which instance is picked doesn't matter, and my question was whether there was a way of expressing that - e.g., with a quantifier whose scope doesn't extend to the RHS, so the RHS wouldn't even have access to it. As to the "Should this compile" question, I guess I still don't see how the situation is different from:

...

...
v = (undefined::A) t = show v

Which should only compile if there is an instance for Show A. In both cases you need to check whether an instance exists; but in one it's *any* instance, and with the other it's an instance with the right instance head. I concede the former is probably tricky, but I've seen people achieve really tricky things with Haskell types, and have decided to ask even when something looks impossible.

...

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

What I meant was that IsNotFirst A, for some concrete A, will hold depending on whether there is an instance declaration - for example, IsNotFirst A. But you're right: without OverlappingInstances, this is a stretch of the imagination, whereas with it, you can have type-level boolean witnesses to this 'change'.

Julian K. Arni

7:58 p.m.

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

4214

Age (days ago)

4215

Last active (days ago)

List overview

Download

7 comments

4 participants

participants (4)

adam vogt
Andras Slemmer
Julian Arni
Julian K. Arni

Quantification in Instance Contexts

tags

participants (4)