Re: [Haskell-cafe] Class constraints with "free" type variables and fundeps

CCing the list back. At Fri, 28 Sep 2012 13:30:52 -0700, Alexander Solla wrote:
What is the problem, exactly? It looks to me like UndecidableInstances and ScopedTypeVariables (on foo, or its arguments) would be enough.
I'm not sure what you mean. I don't see the need for UndecidableInstances, and there is no way I can see to bring the `b' into scope in the type sig for foo, ScopedTypeVariables or not - unless I'm missing something.
Also note that as stated, foo's type "is a bottom" (more specifically, is a function onto bottom, since c is free in the class, and so foo must be parametrically polymorphic in its return type, and so is devoid of "real" Haskell values). Hopefully that is just an artefact of the translation to Foo's and Bar's.
Yeah the type for `foo' is irrelevant, I just needed to put something there. -- Francesco * Often in error, never in doubt

On Fri, Sep 28, 2012 at 5:04 PM, Francesco Mazzoli
CCing the list back.
At Fri, 28 Sep 2012 13:30:52 -0700, Alexander Solla wrote:
What is the problem, exactly? It looks to me like UndecidableInstances and ScopedTypeVariables (on foo, or its arguments) would be enough.
I'm not sure what you mean. I don't see the need for UndecidableInstances, and there is no way I can see to bring the `b' into scope in the type sig for foo, ScopedTypeVariables or not - unless I'm missing something.
Well, then what exactly is the problem? Are you getting an error? You don't need to bring 'b' into scope. You will already have real types in scope. instance Foo A B instance Bar A where foo A B = C tryIt = (foo :: A -> B -> C) A B

At Fri, 28 Sep 2012 17:19:36 -0700, Alexander Solla wrote:
Well, then what exactly is the problem? Are you getting an error?
...well yes. The error I get with the posted class declarations is Not in scope: type variable `b' at the line with class Foo a b => Bar a where Which I get because all the type vars in the LHS must be referenced on the RHS (or so it seems). Now, in my case the problem does not stop there, because I also want to reference the tyvar on the LHS in a type signature of a method, since in that case there is a fundep on b (`a -> b'), which makes `b' decidable if you have `a' and `Foo a b'.
You don't need to bring 'b' into scope. You will already have real types in scope.
instance Foo A B instance Bar A where foo A B = C
Again, I'm not sure what you mean here. -- Francesco * Often in error, never in doubt

On Fri, Sep 28, 2012 at 5:36 PM, Francesco Mazzoli
At Fri, 28 Sep 2012 17:19:36 -0700, Alexander Solla wrote:
Well, then what exactly is the problem? Are you getting an error?
...well yes. The error I get with the posted class declarations is
Not in scope: type variable `b'
at the line with
class Foo a b => Bar a where
Which I get because all the type vars in the LHS must be referenced on the RHS (or so it seems).
Yes, indeed.
Now, in my case the problem does not stop there, because I also want to reference the tyvar on the LHS in a type signature of a method, since in that case there is a fundep on b (`a -> b'), which makes `b' decidable if you have `a' and `Foo a b'.
Only with respect to type inference.
You don't need to bring 'b' into scope. You will already have real types in scope.
instance Foo A B instance Bar A where foo A B = C
Again, I'm not sure what you mean here.
I wouldn't have replied with that line of thought if you had just told us what the problem was in the first place. I /was/ saying that you can use explicit type annotations to disambiguate instances. Most of us haven't memorized the Haskell 2010 report. We let the compiler tell us what's wrong and either learn why, or how to fix it. So post your errors. By the way, it is rather rude to publicly post a private email... Now, on to your real problem. Use TypeFamilies instead: class Foo a where type BarThing a :: * class Foo a => Bar a where foo :: a -> BarThing a -> b This is pretty pointless, since you can just refactor into the nearly equivalent: class Foo a class Foo a => Bar a where type BarThing a :: * foo :: a -> BarThing a -> c It may or may not matter to which family the type synonym belongs. What is the problem you are actually trying to solve?

At Fri, 28 Sep 2012 18:33:23 -0700, Alexander Solla wrote:
Only with respect to type inference.
I don't understand this comment.
I wouldn't have replied with that line of thought if you had just told us what the problem was in the first place. I /was/ saying that you can use explicit type annotations to disambiguate instances.
Most of us haven't memorized the Haskell 2010 report. We let the compiler tell us what's wrong and either learn why, or how to fix it. So post your errors.
Sorry, I posted in a hurry. Besides, feeding those lines to a compiler before replying takes 10 seconds.
By the way, it is rather rude to publicly post a private email...
I thought that you had forgot to reply all, as often happens. I also want the discussion to stay on the list, so that people can read in the future. I'm sorry if that email was meant to be private, I saw nothing private about it.
Now, on to your real problem.
Use TypeFamilies instead:
class Foo a where type BarThing a :: *
class Foo a => Bar a where foo :: a -> BarThing a -> b
As I mentioned in the original post, `Foo' is outside my control.
This is pretty pointless, since you can just refactor into the nearly equivalent:
class Foo a
class Foo a => Bar a where type BarThing a :: * foo :: a -> BarThing a -> c
It may or may not matter to which family the type synonym belongs.
Mine was a contrived example to show the issue. The whole point is to reduce the number of arguments of a class by referring to another class and its fundeps.
What is the problem you are actually trying to solve?
What I actually (would like to) have is something like this:
class (EditDistance algo sym, ListLike full sym) =>
Search container full algo | container -> full, container -> algo where

At Sat, 29 Sep 2012 10:30:07 +0200, Francesco Mazzoli wrote:
Then I'd also like to have
newtype TST sym algo = <...>
instance (Ord sym, ListLike full sym) => Search (TST sym algo) full algo
This one is a different problem - it requires UndecidableInstances and I don't understand why. It seems to me that the coverage condition (http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extension..., point 7.6.3.2) is too strict in these cases. But this is not that important.
This doesn't make sense with the code posted (which would require sensibly UndecidableInstances), I meant something like this (I don't have "actual" code to show the problem): data Foo a class Bar a b | a -> b class Quux a b | a -> b instance Bar a b => Quux (Foo a) b -- Francesco * Often in error, never in doubt

At Sat, 29 Sep 2012 10:56:29 +0200, Francesco Mazzoli wrote:
At Sat, 29 Sep 2012 10:30:07 +0200, Francesco Mazzoli wrote:
Then I'd also like to have
newtype TST sym algo = <...>
instance (Ord sym, ListLike full sym) => Search (TST sym algo) full algo
This one is a different problem - it requires UndecidableInstances and I don't understand why. It seems to me that the coverage condition (http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extension..., point 7.6.3.2) is too strict in these cases. But this is not that important.
This doesn't make sense with the code posted (which would require sensibly UndecidableInstances), I meant something like this (I don't have "actual" code to show the problem):
data Foo a
class Bar a b | a -> b
class Quux a b | a -> b
instance Bar a b => Quux (Foo a) b
Actually I know why this is the case - instances are picked without looking at the constraints, and there is no backtracking. I guess my brain just can't resist from seeing Prolog in type classes... -- Francesco * Often in error, never in doubt
participants (2)
-
Alexander Solla
-
Francesco Mazzoli