Re: [Haskell-cafe] Re: Laziness question

2010-08-04 Thread Nicolas Pouillard 
On Tue, 03 Aug 2010 16:36:33 +0200, Janis Voigtländer 
j...@informatik.uni-bonn.de 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

2010-08-04 Thread Janis Voigtländer 

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

2010-08-04 Thread Nicolas Pouillard 
On Wed, 04 Aug 2010 15:41:54 +0200, Janis Voigtländer 
j...@informatik.uni-bonn.de 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

2010-08-04 Thread Janis Voigtländer 

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

2010-08-04 Thread Nicolas Pouillard 
On Wed, 04 Aug 2010 17:27:01 +0200, Janis Voigtländer 
j...@informatik.uni-bonn.de 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

2010-08-04 Thread Janis Voigtländer 

Nicolas Pouillard schrieb:

On Wed, 04 Aug 2010 17:27:01 +0200, Janis Voigtländer 
j...@informatik.uni-bonn.de 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

2010-08-04 Thread Nicolas Pouillard 
On Wed, 04 Aug 2010 17:47:12 +0200, Janis Voigtländer 
j...@informatik.uni-bonn.de wrote:
 Nicolas Pouillard schrieb:
  On Wed, 04 Aug 2010 17:27:01 +0200, Janis Voigtländer 
  j...@informatik.uni-bonn.de 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

2010-08-04 Thread Janis Voigtländer 

Nicolas Pouillard schrieb:

On Wed, 04 Aug 2010 17:47:12 +0200, Janis Voigtländer 
j...@informatik.uni-bonn.de wrote:

Nicolas Pouillard schrieb:

On Wed, 04 Aug 2010 17:27:01 +0200, Janis Voigtländer 
j...@informatik.uni-bonn.de 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

2010-08-04 Thread Nicolas Pouillard 
On Wed, 04 Aug 2010 18:04:13 +0200, Janis Voigtländer 
j...@informatik.uni-bonn.de wrote:
 Nicolas Pouillard schrieb:
  On Wed, 04 Aug 2010 17:47:12 +0200, Janis Voigtländer 
  j...@informatik.uni-bonn.de wrote:
  Nicolas Pouillard schrieb:
  On Wed, 04 Aug 2010 17:27:01 +0200, Janis Voigtländer 
  j...@informatik.uni-bonn.de 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

2010-08-04 Thread Janis Voigtländer 

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

2010-08-03 Thread Nicolas Pouillard 
On Mon, 02 Aug 2010 17:41:02 +0200, Janis Voigtländer 
j...@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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org

Re: [Haskell-cafe] Re: Laziness question

2010-08-03 Thread Stefan Holdermans 
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

2010-08-03 Thread Janis Voigtländer 

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

2010-08-03 Thread Janis Voigtländer 

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

2010-08-03 Thread Nicolas Pouillard 
On Tue, 3 Aug 2010 16:24:54 +0200, Stefan Holdermans ste...@vectorfabrics.com 
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

2010-08-03 Thread Brandon S Allbery KF8NH 
-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

[Haskell-cafe] Re: Laziness question

2010-08-02 Thread 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.

- 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

Re: [Haskell-cafe] Re: Laziness question

2010-08-02 Thread Brandon S Allbery KF8NH 
-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

Re: [Haskell-cafe] Re: Laziness question

2010-08-02 Thread Stefan Holdermans 
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

2010-08-02 Thread Stefan Holdermans 
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

2010-08-02 Thread Brandon S Allbery KF8NH 
-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

2010-08-02 Thread Stefan Holdermans 
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