Janis Voigtlaender wrote:
Janis Voigtlaender wrote:
Lennart Augustsson wrote:
There is a good reason seq cannot be defined for functions in the pure lambda calculus... It doesn't belong there. :)
How about the same argument for general recursion? As in: There is a good reason (typability) that fixpoint combinators cannot be defined in the pure lambda calculus... They don't belong there.
Maybe by "pure lambda calculus" you meant the untyped one. Then my comparative argument does not work anymore, because fixpoints are definable in the untyped setting, whereas seq isn't. Still, it remains questionable whether this provides an argument for removing seq but retaining fixpoints in Haskell. Why is the untyped setting the point of reference?
In any case, the argument via losing parametricity does not hold. It is not necessary to sacrifice seq to get parametricity back. Not any more than it was necessary to sacrifice seq to get parametricity back.
Replace "seq" by "fix" in the last sentence ;-) -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de