Re: [Haskell-cafe] Re: Laziness question
Nicolas Pouillard schrieb: 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''' :: (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)) Well, in this example you were lucky that the function type on which you use seq involves some type variables. But consider this example: f :: (Int -> Int) -> a -> a f h x = seq h x I think with your definitions that function will really have that type, without any type class constraints on anything. So let us derive the free theorem for that type. It is: forall t1,t2 in TYPES, g :: t1 -> t2, g strict. forall p :: Int -> Int. forall q :: Int -> Int. (forall x :: Int. p x = q x) ==> (forall y :: t1. g (f p y) = f q (g y)) Now, set p :: Int -> Int p = undefined q :: Int -> Int q _ = undefined Clearly, forall x :: Int. p x = q x holds. So it should be the case that for every strict function g and type-appropriate input y it holds: g (f p y) = f q (g y) But clearly the left-hand side is undefined (due to strictness of g and f p y = f undefined y = seq undefined y), while the right-hand side is not necessarily so (due to f q (g y) = f (\_ -> undefined) (g y) = seq (\_ -> undefined) (g y) = g y). So you have claimed that by using seq via genericSeq in the above definition of f you are guaranteed that any free theorem you derive from its type is correct. But as you see above it is not! I think you have to face it: if you want a solution that both gives meaningful free theorems and still allows to write all programs involving seq that you can currently write in Haskell, then using type classes is not the answer. Ciao, Janis. -- Jun.-Prof. Dr. Janis Voigtländer http://www.iai.uni-bonn.de/~jv/ mailto:j...@iai.uni-bonn.de ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Laziness question
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Laziness question
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? Ciao, Janis. -- Jun.-Prof. Dr. Janis Voigtländer http://www.iai.uni-bonn.de/~jv/ mailto:j...@iai.uni-bonn.de ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Laziness question
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Laziness question
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: 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). Ciao, Janis. -- Jun.-Prof. Dr. Janis Voigtländer http://www.iai.uni-bonn.de/~jv/ mailto:j...@iai.uni-bonn.de ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Laziness question
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Laziness question
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. Ciao, Janis. -- Jun.-Prof. Dr. Janis Voigtländer http://www.iai.uni-bonn.de/~jv/ mailto:j...@iai.uni-bonn.de ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Laziness question
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Laziness question
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? Given that it provides runtime type inspection, probably one cannot derive any parametricity results at all for a type variable constrained by Typeable. 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, ...). In other words, by saying seq :: Typeable a => a -> b -> b, you assume pessimistically that seq can do everything that is possible on members of the Typeable class. But that might be overly pessimistic, since in reality the only thing that seq can do is evaluate an arbitrary expression to weak head normal form. 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. Best, Janis. -- Jun.-Prof. Dr. Janis Voigtländer http://www.iai.uni-bonn.de/~jv/ mailto:j...@iai.uni-bonn.de ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Laziness question
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Laziness question
-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] allb...@kf8nh.com system administrator [openafs,heimdal,too many hats] allb...@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- ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Laziness question
On Tue, 3 Aug 2010 16:24:54 +0200, Stefan Holdermans wrote: > 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). If we ignore the solution using Typeable for now. The actual seq would be considered unsafe but seq would be re-introduced as a method of a type class with instances for many types but not for functions. So in this view only forcing functions would be considered "out of the language". -- Nicolas Pouillard http://nicolaspouillard.fr ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Laziness question
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:j...@iai.uni-bonn.de ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Laziness question
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. :-) 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. 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. Best, Janis. -- Jun.-Prof. Dr. Janis Voigtländer http://www.iai.uni-bonn.de/~jv/ mailto:j...@iai.uni-bonn.de ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Laziness question
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Laziness question
On Mon, 02 Aug 2010 17:41:02 +0200, Janis Voigtländer wrote: > 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 ___ Has
Re: [Haskell-cafe] Re: Laziness question
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Laziness question
-BEGIN PGP SIGNED MESSAGE- Hash: SHA1 On 8/2/10 17:18 , Stefan Holdermans wrote: > 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. ;-) 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. - -- brandon s. allbery [linux,solaris,freebsd,perl] allb...@kf8nh.com system administrator [openafs,heimdal,too many hats] allb...@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/ iEYEARECAAYFAkxXWZUACgkQIn7hlCsL25XhxACdFLFtCUrJqEpqGSsymt1uE3Zc yWgAoKcyJZdjng1zthyAtPkMCIvHce27 =XkFz -END PGP SIGNATURE- ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Laziness question
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Laziness question
Brandon, > Hm. Seems to me that (with TypeFamilies and FlexibleContexts) > >> h :: (x ~ y, Eval (y -> Int)) => (x -> Int) -> (y -> Int) -> Int > > should do that, but ghci is telling me it isn't (substituting Eq for Eval > for the nonce): > > Prelude> let h :: (x ~ y, Eq (y -> Int)) => (x -> Int) -> (y -> Int) -> > Int; h = undefined > Prelude> :t h > h :: (Eq (x -> Int)) => (x -> Int) -> (x -> Int) -> Int > > Bleah. (as if it weren't obvious) I still don't quite grok this stuff Well... x ~ y kind of implies that x could replace y within the scope of the constraint: it's like one of the first thing I would expect to follow from a notion of equality. ;-) 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. Cheers, Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Laziness question
-BEGIN PGP SIGNED MESSAGE- Hash: SHA1 On 8/2/10 11:41 , Janis Voigtländer wrote: > 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 Hm. Seems to me that (with TypeFamilies and FlexibleContexts) > h :: (x ~ y, Eval (y -> Int)) => (x -> Int) -> (y -> Int) -> Int should do that, but ghci is telling me it isn't (substituting Eq for Eval for the nonce): Prelude> let h :: (x ~ y, Eq (y -> Int)) => (x -> Int) -> (y -> Int) -> Int; h = undefined Prelude> :t h h :: (Eq (x -> Int)) => (x -> Int) -> (x -> Int) -> Int Bleah. (as if it weren't obvious) I still don't quite grok this stuff - -- brandon s. allbery [linux,solaris,freebsd,perl] allb...@kf8nh.com system administrator [openafs,heimdal,too many hats] allb...@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/ iEYEARECAAYFAkxW+VwACgkQIn7hlCsL25Us2gCbBaiDCutFcN7URjqBL0RUUMUl fkkAoJ6jV52RUeNQcISeyzTMFtDwic+y =0fBN -END PGP SIGNATURE- ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Laziness question
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. - 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.) 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. Best regards, Janis. -- Jun.-Prof. Dr. Janis Voigtländer http://www.iai.uni-bonn.de/~jv/ mailto:j...@iai.uni-bonn.de ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
