On Mon, 02 Aug 2010 17:41:02 +0200, Janis Voigtländer
Hi,
I am late to reply in this thread, but as I see Stefan has already made what (also from my view) are the main points:
- Putting seq in a type class makes type signatures more verbose, which one may consider okay or not. In the past (and, as it seems, again in every iteration of the language development process since then) the majority of the language design decision makers have considered this verbosity non-okay enough, so that they decided to have a fully polymorhpic seq.
- Even if putting seq in a type class, problems with parametricity do not simply vanish. The question is what instances there will be for that class. (For example, if there is not instance at all, then no seq-related problems of *any* nature can exist...)
- The Haskell 1.3 "solution" was to, among others, have a class instance for functions. As we show in the paper Stefan mentioned, that is not a solution. Some statements claimed by parametricity will then still be wrong due to seq.
I agree. Adding an instance with a polymorphic primitive vanish the whole bonus of the type class approach.
- 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. Actually I think we can keep the old generic seq, but cutting its full polymorphism: seq :: Typeable a => a -> b -> b Even if this is acceptable I would still introduce a type class for seq for the following reasons: - It can be useful to have a different implementation on some specific types. - It may apply one types on which we do not want Typeable. - One could safely use the Typeable version for functions.
Two more specific answers to Nicolas' comments:
Actually my point is that if we do not use any polymorphic primitive to implement a family of seq functions then it cannot be flawed. Indeed if you read type classes as a way to implicitly pass and pick > functions then it cannot add troubles.
Completely correct. But the point is that without using any polymorphic primitive you won't be able to implement a member of that family for the case of function types (which you do not consider a big restriction, but others do).
However I absolutely do not buy their argument using as example a function f :: Eval (a -> Int) => (a -> Int) -> (a -> Int) -> Int. They consider as an issue the fact that the type does not tell us on which argument seq is used. I think it is fine we may want a more precise type for it to get more properties out of it but it is not flawed. As much as we don't know where (==) is used given a function of type ∀ a. Eq a => [a] -> [a].
I fear you do not buy our argument since you did not fully understand what our argument is, which in all probability is our fault in not explaining it enough. The point is not that we dislike per se that one doesn't know from the type signature how/where exactly methods from a type class are used. In your example ∀ a. Eq a => [a] -> [a] it's alright that we don't know more about where (==) is used. But for a function of type f :: Eval (a -> Int) => (a -> Int) -> (a -> Int) -> Int, in connection with trying to find out whether uses of seq are harmful or not, it is absolutely *essential* to know on which of the two functions (a -> Int) seq is used. The type class approach cannot tell that. Hence, a type class approach is unsuitable for trying to prevent seq from doing parametricity-damage while still allowing to write all the Haskell programs one could before (including ones that use seq on functions). That is the flaw of the type class approach to controlling seq. It is of course no flaw of using type classes in Haskell for other things, and we certainly did not meant to imply such a thing.
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. Kind regards, -- Nicolas Pouillard http://nicolaspouillard.fr