Can we throw some whole program partial evaluation with a termination decision oracle into the mix? On Tuesday, April 1, 2014, John Lato wrote:

I think this is a great idea and should become a top priority. I would probably start by switching to a type-class-based seq, after which perhaps the next step forward would become more clear.

John L. On Apr 1, 2014 2:54 AM, "Dan Doel" javascript:_e(%7B%7D,'cvml','dan.doel@gmail.com');> wrote:

...

In the past year or two, there have been multiple performance problems in various areas related to the fact that lambda abstraction is not free, though we tend to think of it as so. A major example of this was deriving of Functor. If we were to derive Functor for lists, we would end up with something like:

instance Functor [] where fmap _ [] = [] fmap f (x:xs) = f x : fmap (\y -> f y) xs

This definition is O(n^2) when fully evaluated,, because it causes O(n) eta expansions of f, so we spend time following indirections proportional to the depth of the element in the list. This has been fixed in 7.8, but there are other examples. I believe lens, [1] for instance, has some stuff in it that works very hard to avoid this sort of cost; and it's not always as easy to avoid as the above example. Composing with a newtype wrapper, for instance, causes an eta expansion that can only be seen as such at the core level.

The obvious solution is: do eta reduction. However, this is not operationally sound currently. The problem is that seq is capable of telling the difference between the following two expressions:

undefined \x -> undefined x

The former causes seq to throw an exception, while the latter is considered defined enough to not do so. So, if we eta reduce, we can cause terminating programs to diverge if they make use of this feature.

Luckily, there is a solution.

Semantically one would usually identify the above two expressions. While I do believe one could construct a semantics that does distinguish them, it is not the usual practice. This suggests that there is a way to not distinguish them, perhaps even including seq. After all, the specification of seq is monotone and continuous regardless of whether we unify ⊥ with \x -> ⊥ x or insert an extra element for the latter.

The currently problematic case is function spaces, so I'll focus on it. How should:

seq : (a -> b) -> c -> c

act? Well, other than an obvious bottom, we need to emit bottom whenever our given function is itself bottom at every input. This may first seem like a problem, but it is actually quite simple. Without loss of generality, let us assume that we can enumerate the type a. Then, we can feed these values to the function, and check their results for bottom. Conal Elliot has prior art for this sort of thing with his unamb [2] package. For each value x :: a, simply compute 'f x `seq` ()' in parallel, and look for any successes. If we ever find one, we know the function is non-bottom, and we can return our value of c. If we never finish searching, then the function must be bottom, and seq should not terminate, so we have satisfied the specification.

Now, some may complain about the enumeration above. But this, too, is a simple matter. It is well known that Haskell programs are denumerable. So it is quite easy to enumerate all Haskell programs that produce a value, check whether that value has the type we're interested in, and compute said value. All of this can be done in Haskell. Thus, every Haskell type is programatically enumerable in Haskell, and we can use said enumeration in our implementation of seq for function types. I have discussed this with Russell O'Connor [3], and he assures me that this argument should be sufficient even if we consider semantic models of Haskell that contain values not denoted by any Haskell program, so we should be safe there.

The one possible caveat is that this implementation of seq is not operationally uniform across all types, so the current fully polymorphic type of seq may not make sense. But moving back to a type class based approach isn't so bad, and this time we will have a semantically sound backing, instead of just having a class with the equivalent of the current magic function in it.

Once this machinery is in place, we can eta reduce to our hearts' content, and not have to worry about breaking semantics. We'd no longer put the burden on programmers to use potentially unsafe hacks to avoid eta expansions. I apologize for not sketching an implementation of the above algorithm, but I'm sure it should be elementary enough to make it into GHC in the next couple versions. Everyone learns about this type of thing in university computer science programs, no?

Thoughts? Comments? Questions?

Cheers, -- Dan

[1] http://hackage.haskell.org/package/lens [2] http://hackage.haskell.org/package/unamb [3] http://r6.ca/

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.orgjavascript:_e(%7B%7D,'cvml','Glasgow-haskell-users@haskell.org'); http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Hi Edward, Yes, I'm aware of that. However, I thought Dan's proposal especially droll given that changing seq to a class-based function would be sufficient to make eta-reduction sound, given appropriate instances (or lack thereof). Meaning we could leave the rest of the proposal unevaluated (lazily!). And if somebody were to suggest that on a different day, +1 from me. John On Apr 1, 2014 10:32 AM, "Edward Kmett" wrote:

John,

Check the date and consider the process necessary to "enumerate all Haskell programs and check their types".

-Edward

On Tue, Apr 1, 2014 at 9:17 AM, John Lato wrote:

...

I think this is a great idea and should become a top priority. I would probably start by switching to a type-class-based seq, after which perhaps the next step forward would become more clear.

John L. On Apr 1, 2014 2:54 AM, "Dan Doel" wrote:

...

In the past year or two, there have been multiple performance problems in various areas related to the fact that lambda abstraction is not free, though we tend to think of it as so. A major example of this was deriving of Functor. If we were to derive Functor for lists, we would end up with something like:

instance Functor [] where fmap _ [] = [] fmap f (x:xs) = f x : fmap (\y -> f y) xs

This definition is O(n^2) when fully evaluated,, because it causes O(n) eta expansions of f, so we spend time following indirections proportional to the depth of the element in the list. This has been fixed in 7.8, but there are other examples. I believe lens, [1] for instance, has some stuff in it that works very hard to avoid this sort of cost; and it's not always as easy to avoid as the above example. Composing with a newtype wrapper, for instance, causes an eta expansion that can only be seen as such at the core level.

The obvious solution is: do eta reduction. However, this is not operationally sound currently. The problem is that seq is capable of telling the difference between the following two expressions:

undefined \x -> undefined x

The former causes seq to throw an exception, while the latter is considered defined enough to not do so. So, if we eta reduce, we can cause terminating programs to diverge if they make use of this feature.

Luckily, there is a solution.

Semantically one would usually identify the above two expressions. While I do believe one could construct a semantics that does distinguish them, it is not the usual practice. This suggests that there is a way to not distinguish them, perhaps even including seq. After all, the specification of seq is monotone and continuous regardless of whether we unify ⊥ with \x -> ⊥ x or insert an extra element for the latter.

The currently problematic case is function spaces, so I'll focus on it. How should:

seq : (a -> b) -> c -> c

act? Well, other than an obvious bottom, we need to emit bottom whenever our given function is itself bottom at every input. This may first seem like a problem, but it is actually quite simple. Without loss of generality, let us assume that we can enumerate the type a. Then, we can feed these values to the function, and check their results for bottom. Conal Elliot has prior art for this sort of thing with his unamb [2] package. For each value x :: a, simply compute 'f x `seq` ()' in parallel, and look for any successes. If we ever find one, we know the function is non-bottom, and we can return our value of c. If we never finish searching, then the function must be bottom, and seq should not terminate, so we have satisfied the specification.

Now, some may complain about the enumeration above. But this, too, is a simple matter. It is well known that Haskell programs are denumerable. So it is quite easy to enumerate all Haskell programs that produce a value, check whether that value has the type we're interested in, and compute said value. All of this can be done in Haskell. Thus, every Haskell type is programatically enumerable in Haskell, and we can use said enumeration in our implementation of seq for function types. I have discussed this with Russell O'Connor [3], and he assures me that this argument should be sufficient even if we consider semantic models of Haskell that contain values not denoted by any Haskell program, so we should be safe there.

The one possible caveat is that this implementation of seq is not operationally uniform across all types, so the current fully polymorphic type of seq may not make sense. But moving back to a type class based approach isn't so bad, and this time we will have a semantically sound backing, instead of just having a class with the equivalent of the current magic function in it.

Once this machinery is in place, we can eta reduce to our hearts' content, and not have to worry about breaking semantics. We'd no longer put the burden on programmers to use potentially unsafe hacks to avoid eta expansions. I apologize for not sketching an implementation of the above algorithm, but I'm sure it should be elementary enough to make it into GHC in the next couple versions. Everyone learns about this type of thing in university computer science programs, no?

Thoughts? Comments? Questions?

Cheers, -- Dan

[1] http://hackage.haskell.org/package/lens [2] http://hackage.haskell.org/package/unamb [3] http://r6.ca/

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

I'm already uneasy using bang patterns on polymorphic data because I don't know exactly what it will accomplish. Maybe it adds too much strictness? Not enough? Simply duplicates work? Perhaps it's acceptable to remove that feature entirely (although that may require adding extra strictness in a lot of other places). Alternatively, maybe it's enough to simply find a use for that good-for-nothing syntax we already have? On Apr 1, 2014 5:32 PM, "Edward Kmett" wrote:

Unfortunately the old class based solution also carries other baggage,

like the old data type contexts being needed in the language for bang patterns. :(

-Edward

On Apr 1, 2014, at 5:26 PM, John Lato wrote:

...

Hi Edward,

Yes, I'm aware of that. However, I thought Dan's proposal especially

...

And if somebody were to suggest that on a different day, +1 from me.

John

On Apr 1, 2014 10:32 AM, "Edward Kmett" wrote:

...

John,

Check the date and consider the process necessary to "enumerate all

Haskell programs and check their types".

...

...

-Edward

On Tue, Apr 1, 2014 at 9:17 AM, John Lato wrote:

...

I think this is a great idea and should become a top priority. I would

...

...

...

John L.

On Apr 1, 2014 2:54 AM, "Dan Doel" wrote:

...

In the past year or two, there have been multiple performance

...

...

...

...

various areas related to the fact that lambda abstraction is not free, though we tend to think of it as so. A major example of this was deriving of Functor. If we were to derive Functor for lists, we would end up with something like:

instance Functor [] where fmap _ [] = [] fmap f (x:xs) = f x : fmap (\y -> f y) xs

This definition is O(n^2) when fully evaluated,, because it causes O(n) eta expansions of f, so we spend time following indirections proportional to the depth of the element in the list. This has been fixed in 7.8, but

...

...

...

...

other examples. I believe lens, [1] for instance, has some stuff in it that works very hard to avoid this sort of cost; and it's not always as easy to avoid as the above example. Composing with a newtype wrapper, for instance, causes an eta expansion that can only be seen as such at the core level.

The obvious solution is: do eta reduction. However, this is not operationally sound currently. The problem is that seq is capable of telling the difference between the following two expressions:

undefined \x -> undefined x

The former causes seq to throw an exception, while the latter is considered defined enough to not do so. So, if we eta reduce, we can cause terminating programs to diverge if they make use of this feature.

Luckily, there is a solution.

Semantically one would usually identify the above two expressions. While I do believe one could construct a semantics that does distinguish them, it is not the usual practice. This suggests that there is a way to not distinguish them, perhaps even including seq. After all, the specification of seq is monotone and continuous regardless of whether we unify ⊥ with \x -> ⊥ x or insert an extra element for the latter.

The currently problematic case is function spaces, so I'll focus on it. How should:

seq : (a -> b) -> c -> c

act? Well, other than an obvious bottom, we need to emit bottom whenever our given function is itself bottom at every input. This may first seem

droll given that changing seq to a class-based function would be sufficient to make eta-reduction sound, given appropriate instances (or lack thereof). Meaning we could leave the rest of the proposal unevaluated (lazily!). probably start by switching to a type-class-based seq, after which perhaps the next step forward would become more clear. problems in there are like a

...

...

...

...

problem, but it is actually quite simple. Without loss of generality, let us assume that we can enumerate the type a. Then, we can feed these values to the function, and check their results for bottom. Conal Elliot has prior art for this sort of thing with his unamb [2] package. For each value x :: a, simply compute 'f x `seq` ()' in parallel, and look for any successes. If we ever find one, we know the function is non-bottom, and we can return our value of c. If we never finish searching, then the function must be bottom, and seq should not terminate, so we have satisfied the specification.

Now, some may complain about the enumeration above. But this, too, is a simple matter. It is well known that Haskell programs are denumerable. So it is quite easy to enumerate all Haskell programs that produce a value, check whether that value has the type we're interested in, and compute said value. All of this can be done in Haskell. Thus, every Haskell type is programatically enumerable in Haskell, and we can use said enumeration in our implementation of seq for function types. I have discussed this with Russell O'Connor [3], and he assures me that this argument should be sufficient even if we consider semantic models of Haskell that contain values not denoted by any Haskell program, so we should be safe there.

The one possible caveat is that this implementation of seq is not operationally uniform across all types, so the current fully polymorphic type of seq may not make sense. But moving back to a type class based approach isn't so bad, and this time we will have a semantically sound backing, instead of just having a class with the equivalent of the current magic function in it.

Once this machinery is in place, we can eta reduce to our hearts' content, and not have to worry about breaking semantics. We'd no longer put the burden on programmers to use potentially unsafe hacks to avoid eta expansions. I apologize for not sketching an implementation of the above algorithm, but I'm sure it should be elementary enough to make it into GHC in the next couple versions. Everyone learns about this type of thing in university computer science programs, no?

Thoughts? Comments? Questions?

Cheers, -- Dan

[1] http://hackage.haskell.org/package/lens [2] http://hackage.haskell.org/package/unamb [3] http://r6.ca/

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Consider something like data Foo a = Foo !Int !a The data constructor Foo needs to be strict in its arguments, so it'd need Seq Int and Seq a. Seq Int would be resolved by the environment, but Seq a would need to come from somewhere. data Seq a => Foo a = Foo !Int !a gives you Foo :: Seq a => Int -> a -> Foo a so it is available when evaluating the constructor. We're not storing the instance as a slot in the constructor, so this isn't. data Foo a where Foo :: Seq a => Int -> a -> Foo a or equivalently data Foo a = Seq a => Foo !Int !a This is where the data type contexts came from. They were originally motivated by the needs of the no-longer existent Seq class, and then subverted to make Complex less useful than it otherwise could be. ;) -Edward On Wed, Apr 2, 2014 at 3:08 AM, Tom Ellis < tom-lists-haskell-cafe-2013@jaguarpaw.co.uk> wrote:

On Tue, Apr 01, 2014 at 05:32:45PM -0400, Edward Kmett wrote:

...

Unfortunately the old class based solution also carries other baggage, like the old data type contexts being needed in the language for bang patterns. :(

Can you explain why that is so? I don't understand.

Tom

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Wed, Apr 02, 2014 at 09:51:46AM -0400, Edward Kmett wrote:

Consider something like

data Foo a = Foo !Int !a

The data constructor Foo needs to be strict in its arguments, so it'd need Seq Int and Seq a. Seq Int would be resolved by the environment, but Seq a would need to come from somewhere.

data Seq a => Foo a = Foo !Int !a

Oh right, I didn't realise that's what you meant by "patterns". I assumed you were talking about let or function definitions.

On Wed, Apr 2, 2014 at 3:08 AM, Tom Ellis < tom-lists-haskell-cafe-2013@jaguarpaw.co.uk> wrote:

...

On Tue, Apr 01, 2014 at 05:32:45PM -0400, Edward Kmett wrote:

...

Unfortunately the old class based solution also carries other baggage, like the old data type contexts being needed in the language for bang patterns. :(

Can you explain why that is so? I don't understand.

I stand corrected. So they were there all along and then finally briefly had a reason to exist later on. ;) -Edward On Wed, Apr 2, 2014 at 11:56 AM, Dan Doel wrote:

On Wed, Apr 2, 2014 at 9:51 AM, Edward Kmett wrote:

...

This is where the data type contexts came from. They were originally motivated by the needs of the no-longer existent Seq class, and then subverted to make Complex less useful than it otherwise could be. ;)

This is wrong. Data type contexts existed in the Haskell 1.0 report, and Ratio and Complex used them there. Strict fields didn't exist until 1.3.

-- Dan

On Apr 2, 2014 4:32 PM, "Niklas Haas" wrote:

On Wed, 2 Apr 2014 09:51:46 -0400, Edward Kmett wrote:

...

We're not storing the instance as a slot in the constructor, so this

isn't.

...

data Foo a where Foo :: Seq a => Int -> a -> Foo a

or equivalently

data Foo a = Seq a => Foo !Int !a

Why not? Say we define Seq to something like

...

type family Seq (a :: *) :: Constraint where Seq (a -> b) = 1 ~ 0 Seq t = ()

What would be the drawback in this scenario?

I think that would be acceptable if we posit the existence of a valid Seq a dictionary. I think that would be possible for all builtin types and anything defined via data. But what about e.g. newtype F = F (forall x. Show x => x-> String)

On Wed, Apr 2, 2014 at 8:40 PM, Niklas Haas wrote:

Oh, fair point; this particular F apparently doesn't break it but if you remove the Show x constraint, it does.

Actually, is that a bug in GHC?

...

λ newtype F = F (forall x. Show x => x -> String) λ F undefined `seq` () () λ undefined `seq` () *** Exception: Prelude.undefined

I'm not sure how to interpret this output.

This is pretty weird, but here's what I think is going on: F requires an argument of type forall x. Show x => x -> String. This requires abstracting over a dictionary for Show x. So at the core level, this gets expanded to something like: \showd -> undefined which is non-bottom. Even if you annotate undefined with the above type, You'll probably end up with: (\showd -> undefined) defaultd `seq` () after GHC reinstantiates the polymorphic type and then defaults, which will be undefined. So you can only observe this by wrapping the polymorphic expression in a newtype, to keep it abstracted. I don't know that this qualifies as a bug, but it's definitely pretty subtle behavior. -- Dan