Brandon,

...

h :: (x ~ y, Eval (y -> Int)) => (x -> Int) -> (y -> Int) -> Int

But actually if you push the constraint inward, into the type so to say, you actually get quite close to Janis' and David's solution.

Sorry, I was thinking out loud there. I meant the Eval constraint, not the equality constraint. But, right now, I guess my comment only makes sense to me, so let's pretend I kept quiet. ;-) Cheers, S.

Brandon,

...

Sorry, I was thinking out loud there. I meant the Eval constraint, not the equality constraint. But, right now, I guess my comment only makes sense to me, so let's pretend I kept quiet. ;-)

The point of this discussion is that the Eval constraint needs to be on one of the functions. So I tried to specify that (x -> Int) and (y -> Int) are different types despite x and y being the same type, because one of them has an Eval constraint. This may be a shortcoming of Haskell (or System Fc?) types, although it may be doable with a newtype.

That was kind of what my thinking out loud was getting at. If you want x -> Int and y -> Int to be different types even if x and y actually are the same type, then apparently you want x -> Int and y -> Int to be built from different function-space constructors, say -> and ->*, yielding x -> Int and y ->* Int. Replacing equals for equals again, you get x -> Int and x ->* Int. So, basically, we are annotating function types, what is IIRC exactly what Janis and David are doing. (I hope Janis corrects me if I'm wrong here). Cheers, Stefan

Nicolas,

OK, I better understand now where we disagree. You want to see in the type whether or not the free theorem apply, I want them to always apply when no call to unsafe function is made.

Implementing your suggestion would make me feel uncomfortable. Turning seq into an unsafe operations effectively places it outside the language, like unsafePerformIO isn't really part of the language (in my view, at least). But experience has made it clear that there are plenty of occasions in which we cannot really do without seq (even though its presence in the language is prominent subject of debate). Cheers, Stefan

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 On 8/3/10 10:24 , Stefan Holdermans wrote:

Implementing your suggestion would make me feel uncomfortable. Turning seq into an unsafe operations effectively places it outside the language, like unsafePerformIO isn't really part of the language (in my view, at least). But experience has made it clear that there are plenty of occasions in which we cannot really do without seq (even though its presence in the language is prominent subject of debate).

...which sounds a lot like unsafePerformIO (which *is* inside the language; it's part of the FFI addendum). The parallels are exactly why I suggested it become unsafeSeq. - -- brandon s. allbery [linux,solaris,freebsd,perl] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH -----BEGIN PGP SIGNATURE----- Version: GnuPG v2.0.10 (Darwin) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iEYEARECAAYFAkxYR/gACgkQIn7hlCsL25WE8QCgtAs+gq93pZeRsBwsis9HLSWm xeEAn2xuKLYSB4IsFlxlssL5Hf3Pxo1x =oA8A -----END PGP SIGNATURE-----

On Tue, 03 Aug 2010 16:36:33 +0200, Janis Voigtländer wrote:

Nicolas Pouillard schrieb:

...

...

- If there is no class instance for function types, then those problems go away, of course. But it is doubtful whether that would be a viable solution. Quite a few programs would be rejected as a consequence. (Say, you want to use the strict version of foldl. That will lead to a type class constraint on one of the type variables. Now suppose you actually want to fold in a higher-order fashion, like when expressing efficient reverse via foldr. That would not anymore be possible for the strict version of foldl, as it would require the type-class-constrained variable to be instantiated with a function type.)

I think it would be a step forward. The old seq would still exists as unsafeSeq and such applications could continue to use it. In the mean time parametricity results would better apply to programs without unsafe functions. And this without adding extra complexity into the type system.

Yes, I agree. Of course, you (and Lennart, and others advocating putting seq into a type class) could work toward that solution right away, could have done so for quite some time: write a package with an Eval type class and method safeSeq (and *no* class instance for function types), upload it on Hackage, encourage people to use it. Modulo the naming difference seq/safeSeq vs. unsafeSeq/seq, that's exactly the solution you want. I wonder why it is not happening. :-)

Yes it would be a starting point.

...

Actually I think we can keep the old generic seq, but cutting its full polymorphism:

seq :: Typeable a => a -> b -> b

I guess I don't know enough about Typeable to appreciate that.

Basically the Typeable constraints tells that we dynamically know the identity of the type being passed in. So this may be a bit challenging to cleanly explain how this safely disable the parametricity but in the mean time this is the net result the type is dynamically known at run time. The same trick is known to work for references as well when effects are everywhere: newRef :: Typeable a => a -> Ref a readRef :: Ref a -> a writeRef :: Ref a -> a -> () In the same vein it would make unsafePerformIO less dangerous to add such a constraint. However I would like to here more comments about this seq variant, anyone?

...

OK, I better understand now where we disagree. You want to see in the type whether or not the free theorem apply,

Oh, YES. That's the point of a free theorem, isn't it: that I only need to look at the type of the function to derive some property about it.

...

I want them to always apply when no call to unsafe function is made.

Well, the question is what you mean by "no call to unsafe function is made". Where? In the function under consideration, from whose type the free theorem is derived? Are you sure that this is enough? Maybe that function f does not contain a call to unsafeSeq, but it has an argument which is itself a function. Maybe in some function application, unsafeSeq is passed to f in that argument position, directly or indirectly. Maybe f does internally apply that function argument to something. Can you be sure that this will not lead to a failure of the free theorem you derived from f's type (counting on the fact that f does not call an unsafe function)?

Of course, preventing the *whole program* from calling unsafeSeq is enough to guarantee validity of the free theorems thus derived. But that's equivalent to excluding seq from Haskell altogether.

It depends on the unsafe function that is used. Using unsafeCoerce or unsafePerformIO (from which we can derive unsafeCoerce) badely anywhere suffice to break anything. So while seq is less invasive I find it too much invasive in its raw form. -- Nicolas Pouillard http://nicolaspouillard.fr

On Wed, 04 Aug 2010 15:41:54 +0200, Janis Voigtländer wrote:

Nicolas Pouillard schrieb:

...

...

...

Actually I think we can keep the old generic seq, but cutting its full polymorphism:

seq :: Typeable a => a -> b -> b I guess I don't know enough about Typeable to appreciate that.

Basically the Typeable constraints tells that we dynamically know the identity of the type being passed in. So this may be a bit challenging to cleanly explain how this safely disable the parametricity but in the mean time this is the net result the type is dynamically known at run time.

...

However I would like to here more comments about this seq variant, anyone?

On reflection, isn't Typeable actually much too strong a constraint?

It is indeed "too strong", or "not precise enough" we could say. However at least this simple change make it "correct" (i.e. restore the parametricity results). I would call this function genericSeq :: Typeable a => a -> b -> b

Given that it provides runtime type inspection, probably one cannot derive any parametricity results at all for a type variable constrained by Typeable.

Exactly. We could say that we no longer car derive wrong parametricity results about it.

In contrast, for a type variable constrained via a hypothetical (and tailored to seq) Eval-constraint, one still gets something which looks like a standard free theorem, just with some side conditions relating to _|_ (strictness, totality, ...).

Indeed, that's why I want both! In particular for the instance on functions which could be defined using genericSeq.

...

...

...

OK, I better understand now where we disagree. You want to see in the type whether or not the free theorem apply, Oh, YES. That's the point of a free theorem, isn't it: that I only need to look at the type of the function to derive some property about it.

...

I want them to always apply when no call to unsafe function is made. Well, the question is what you mean by "no call to unsafe function is made". Where? In the function under consideration, from whose type the free theorem is derived? Are you sure that this is enough? Maybe that function f does not contain a call to unsafeSeq, but it has an argument which is itself a function. Maybe in some function application, unsafeSeq is passed to f in that argument position, directly or indirectly. Maybe f does internally apply that function argument to something. Can you be sure that this will not lead to a failure of the free theorem you derived from f's type (counting on the fact that f does not call an unsafe function)?

Of course, preventing the *whole program* from calling unsafeSeq is enough to guarantee validity of the free theorems thus derived. But that's equivalent to excluding seq from Haskell altogether.

It depends on the unsafe function that is used. Using unsafeCoerce or unsafePerformIO (from which we can derive unsafeCoerce) badely anywhere suffice to break anything. So while seq is less invasive I find it too much invasive in its raw form.

Hmm, from this answer I still do not see what you meant when you said you want free theorems to always apply when no call to seq is made. You say that seq is less invasive, so do you indeed assume that as soon as you are sure a function f does not itself (syntactically) contain a call to seq you are safe to use the standard free theorem derived from f's type unconstrained? Do you have any justification for that? Otherwise, we are back to banning seq completely from the whole program/language, in which case it is trivial that no seq-related side conditions will be relevant.

Actually given genericSeq, I no longer advocate the need for a polymorphic seq function. So both genericSeq and the seq from the type class would both safe. However the rule is still the same when using an unsafe function you are on your own. Clearer? Best regards, -- Nicolas Pouillard http://nicolaspouillard.fr

On Wed, 04 Aug 2010 17:27:01 +0200, Janis Voigtländer wrote:

Nicolas Pouillard schrieb:

...

However the rule is still the same when using an unsafe function you are on your own.

Clearer?

Almost. What I am missing is whether or not you would then consider your genericSeq (which is applicable to functions) one of those "unsafe functions" or not.

I would consider it as a safe function. -- Nicolas Pouillard http://nicolaspouillard.fr

On Wed, 04 Aug 2010 17:47:12 +0200, Janis Voigtländer wrote:

Nicolas Pouillard schrieb:

...

On Wed, 04 Aug 2010 17:27:01 +0200, Janis Voigtländer wrote:

...

Nicolas Pouillard schrieb:

...

However the rule is still the same when using an unsafe function you are on your own.

Clearer? Almost. What I am missing is whether or not you would then consider your genericSeq (which is applicable to functions) one of those "unsafe functions" or not.

I would consider it as a safe function.

Well, then I fear you have come full-circle back to a non-solution. It is not safe:

I feared a bit... but no

Consider the example foldl''' from our paper, and replace seq therein by your genericSeq. Then the function will have the same type as the original foldl, but the standard free theorem for foldl does not hold for foldl''' (as also shown in the paper).

So foldl''' now has some Typeable constraints. I agree that the free theorem for foldl does not hold for foldl'''. However can we derive the free theorem by looking at the type? No because of the Typeable constraint. So it is safe to derive free theorems without looking at the usage of seq, just the type of the function. Taking care of not considering parametric a type constrained by Typeable. Finally the difference between your solution and this one is that fewer (valid) free theorems can be derived (because of the Typable constraints introduced by seq on functions). Still it is a solution since we no longer have to fear the usage of seq when deriving a free theorem. Best regards, -- Nicolas Pouillard http://nicolaspouillard.fr

On Wed, 04 Aug 2010 18:04:13 +0200, Janis Voigtländer wrote:

Nicolas Pouillard schrieb:

...

On Wed, 04 Aug 2010 17:47:12 +0200, Janis Voigtländer wrote:

...

Nicolas Pouillard schrieb:

...

On Wed, 04 Aug 2010 17:27:01 +0200, Janis Voigtländer wrote:

...

Nicolas Pouillard schrieb:

...

However the rule is still the same when using an unsafe function you are on your own.

Clearer? Almost. What I am missing is whether or not you would then consider your genericSeq (which is applicable to functions) one of those "unsafe functions" or not. I would consider it as a safe function. Well, then I fear you have come full-circle back to a non-solution. It is not safe:

I feared a bit... but no

...

Consider the example foldl''' from our paper, and replace seq therein by your genericSeq. Then the function will have the same type as the original foldl, but the standard free theorem for foldl does not hold for foldl''' (as also shown in the paper).

So foldl''' now has some Typeable constraints.

No, I don't see how it has that. Or maybe you should make explicit under what conditions a type (a -> b) is in Typeable. What exactly will the type of foldl''' be, and why?

Right let's make it more explicit, I actually just wrote a Control.Seq module and a test file: module Control.Seq where genericSeq :: Typeable a => a -> b -> b genericSeq = Prelude.seq class Seq a where seq :: a -> b -> b instance (Typeable a, Typeable b) => Seq (a -> b) where seq = genericSeq ... Other seq instances ... $ cat test.hs import Prelude hiding (seq) import Data.Function (fix) import Control.Seq (Seq(seq)) import Data.Typeable foldl :: (a -> b -> a) -> a -> [b] -> a foldl c = fix (\h n ys -> case ys of [] -> n x : xs -> let n' = c n x in h n' xs) foldl' :: Seq a => (a -> b -> a) -> a -> [b] -> a foldl' c = fix (\h n ys -> case ys of [] -> n x : xs -> let n' = c n x in seq n' (h n' xs)) foldl'' :: (Typeable a, Typeable b, Seq b) => (a -> b -> a) -> a -> [b] -> a foldl'' c = fix (\h n ys -> seq (c n) (case ys of [] -> n x : xs -> seq xs (seq x (let n' = c n x in h n' xs)))) foldl''' :: (Typeable a, Typeable b) => (a -> b -> a) -> a -> [b] -> a -- GHC infer this one -- foldl''' :: Seq (a -> b -> a) => (a -> b -> a) -> a -> [b] -> a -- however this one require FlexibleContext, and the first one is accepted. foldl''' c = seq c (fix (\h n ys -> case ys of [] -> n x : xs -> let n' = c n x in h n' xs)) Best regards, -- Nicolas Pouillard http://nicolaspouillard.fr

Hi again, Maybe I should add that, maybe disappointingly, I do not even have a strong opinion about whether seq should be in Haskell or not, and in what form. Let me quote the last paragraph of an extended version of our paper referred to earlier:

Finally, a natural question is whether or not selective strictness should be put under control via the type system in a future version of Haskell (or even removed completely). We have deliberately not taken a stand on this here. What was important to us is that both the costs and benefits of either way should be well understood when making such a decision. Maybe the realization that, contrary to popular opinion, a relatively simple approach like the one that was present in Haskell version 1.3 does not suffice to keep selective strictness in check, and that instead something slightly less wieldy, like our type system presented here or a similar one, would be needed, will quell the recurring calls for "putting seq in a type class" once and for all. Even then, while it would mean that our type system does not get adopted in practice, we would consider our effort well invested. At least, the community would then have made an informed decision, and part of the justification would be on record.

That's under the assumption that the requirements we have on a solution are: 1. All Haskell programs that could be written before should still be implementable, though potentially with a different type. 2. Parametricity results derived from the (new) types should hold, even if seq is involved. The Haskell 1.3 approach achieves 1. but not 2. The approach of an Eval class without a function type instance achieves 2. but not 1. Lennart suggested that the programs one loses that (latter) way might be few in practice. I have no idea whether that is true, but it might well be. But it is actually new to me that proponents of putting seq in a type class admit that they can only do so and achieve 2. by accepting to give up 1. In the past, also in the "Being lazy with class" paper, the impression was given that the controversial issue about the Haskell 1.3 solution were just its practicality in terms of how cumbersome or not the additional typing artifacts become. While it was simply supposed that at least that solution achieves both 1. and 2. It does not. Best, Janis. -- Jun.-Prof. Dr. Janis Voigtländer http://www.iai.uni-bonn.de/~jv/ mailto:jv@iai.uni-bonn.de