[Haskell-cafe] Re: Laziness question

[Nicolas Pouillard]

On Mon, 02 Aug 2010 17:41:02 +0200, Janis Voigtländer <jv at informatik.uni-bonn.de> 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