On Thu, May 2, 2013 at 12:09 PM, Erik de Castro Lopo <mle+hs@mega-nerd.com>wrote:

I've also been asking some questions of my local GHC internals guru Ben Lippmeier. A couple of open questions Ben brought are as follows:

* The paper seems to be based on the System Fw + algebraic data types (including existentials) based core, while core is now System Fc with equality constraints and coercions. How does that affect this project?

I'm afraid I don't know and I hope that someone smarter than me (Simon? :)) could comment on this.

* Does anyone have any feel for whether the Core2Core transforms will be easier or more difficult to write with Strict Core?

I don't know if it'll be more verbose or not, but the result should be better since we have strictly more information available.

All good questions! On Thu, May 2, 2013 at 12:48 PM, Carter Schonwald < carter.schonwald@gmail.com> wrote:

What changes in the semantics of doing fusion optimization?

I think Duncan said that fusion is quite separate from the strictness/laziness in the language.

Hi all, Thanks for the input. Given that it'd probably take me weeks or months to get a production ready implementation, I'm probably going to punt on this and hope MSR gets a intern to do it some day. :) -- Johan

On Tue, May 7, 2013 at 4:02 PM, Sturdy, Ian <sturdyi12@mail.wlu.edu> wrote:

Further largely uneducated thoughts on type-level strictness annotations:

- I would imagine that it would work somewhat like uniqueness types in Clean, where `!a` is not a separate type from (or even a subtype of) `a`, but rather `a` itself with the type modifier `!`. I am not certain that all the UNQ semantics carry over, but that is where I would start.

Interesting. Are strict types and uniqueness types in Clean related to each other (or the same thing)? I had the impression that they were separate. I've also had the thought that perhaps we should look into how Clean does things, but I haven't been able to find much discussion or documentation about it.

- I think that `f !a` would be a lazy spine with strict elements, so that a function with an input of type `[!a]` could be passed a lazy list, but with each element evaluated when the spine is evaluated that far rather than when the value itself becomes needed. Consider the rather pointless function

f :: [a] -> Maybe a f (_:e:_) = Just e f _ = Nothing

`f [undefined,1]` evaluates just fine, because even though the spine is evaluated past the first element, that element is not needed. But if we change the signature to `f :: [!a] -> Maybe a`, when evaluating the spine past that element the compiler would evaluate the element and throw the undefined. I see no reason why this would be a problem to implement, but that could be my ignorance.

That brings up a good point. I had been thinking that if you have a function [!Int] -> Int, and you apply it to an argument that's [Int], then all the Ints in the list should be evaluated before calling the function, to match its expectations. But I see now that that's **clearly** wrong: Haskell is still a call-by-need language, and the list is still spine-lazy. As you say, the individual Ints should be forced when the list node containing them is forced. If I'm thinking right it's as if we had (using present Haskell) foo :: [a] -> [a] foo [] = [] foo (x:xs) = x `seq` x:(foo xs) and the compiler would automatically insert `foo` wherever a translation from [a] to [!a] was needed. But the question I posed still basically applies: How in the world can the compiler know what `foo` should look like for *any* type? Say, `IO !a`? Or `forall a. Typeable !a`? etc.

- While technically speaking a "strict type" does not make sense in the return, an evaluated type does, and it is my feeble understanding that being strict in an argument is equivalent to requiring evaluation of the argument before evaluating the function. So if we redefine `!a` from "strict a" to "evaluated a", it does what we want in argument positions while also making sense in returns, so that we can have `seq' :: a -> !a`. But as I think about it, while that makes sense, it is also pointless: if I have `f :: a -> Int; f = const 0`, `f . seq'` will happily never evaluate its argument, since it will never try to evaluate `seq'`. In a strict functional language, evaluation is only forced when something is passed as a function parameter; I see no need to show evaluation in returns because it will be overridden by laziness in the function application itself.

Yep, that's what I was referring to. Thanks for the example :)

------------------------------ *From:* ghc-devs-bounces@haskell.org [ghc-devs-bounces@haskell.org] on behalf of Gábor Lehel [illissius@gmail.com] *Sent:* Monday, May 06, 2013 7:14 PM *To:* Johan Tibell *Cc:* Max Bolingbroke; ghc-devs@haskell.org *Subject:* Re: Implementing Strict Core

On Thu, May 2, 2013 at 6:30 PM, Johan Tibell <johan.tibell@gmail.com>wrote:

...

- implementing strictness annotations at the type level in Haskell itself*.

* I think this could be one of the most important changes in a long time to help Haskell in the "real world". It gives us a better way to talk about strictness than we have today, reducing time spent on chasing down space leaks. One we have strictness annotations in type, we could experiment with a Strict language pragma to make a whole module call-by-value.

FWIW, have you done any thinking about the "strictness types" part of the whole thing? Has anyone? I'd be quite interested in it if so. I mean "Haskell has problems keeping track of strictness/laziness, Haskell has a great type system => let's put strictness in the type system" seems logical enough, but does it actually work out?

The basic idea -- stick a ! on a type to get a strict version of it -- looks simple, but after trying to think it through further, it doesn't seem as simple as it seems. The main questions/issues I've encountered in my undereducated speculation:

- If `!a` and `a` are completely separate types, you would have to put explicit conversions everywhere, which is unpleasant. If `!a` and `a` are the same type, the compiler can't prevent them from getting mixed up, which is useless. So I think you would want `!a` to be a subtype of `a`: `a` is inhabited by both evaluated and unevaluated values, `!a` only by evaluated ones. Where `a` is expected, `!a` is also accepted. But GHC's type system doesn't have subtyping, for (I'm told) good reasons. Could it, for this specific case?

- As a consequence of the subtype relationship, you would also have to track the co/contra/invariance of type parameters, in order to determine whether `f !a` is a subtype of `f a`, or vice versa.

- If you try to pass an `a` where an `!a` is expected, should it be a type error, or should the compiler automatically insert code to evaluate it? What about `f a` and `f !a`? How could the compiler possibly know how to evaluate the `a`s inside of a structure?

- Strict types in the return type position don't make any sense. This makes taking a value, evaluating it somehow, and then having that fact show up in its type difficult.

- As far as I can tell, "strict types" and "unlifted types" are the same thing. The former is guaranteed to be in WHNF, while the latter is guaranteed not to be bottom. I don't see a difference there. Perhaps the second formulation has seen more research?

Or would it be a different kind of scheme that doesn't rest on `!a` being a subtype of `a`? (Especially the thing with the return types makes me think it might not be the best idea.) But how would it look?

-- Your ship was destroyed in a monadic eruption.

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

-- Your ship was destroyed in a monadic eruption.

On Tue, May 7, 2013 at 6:38 PM, Johan Tibell <johan.tibell@gmail.com> wrote:

Hi,

All very good questions. Here's my current thinking on the matter:

`a` and `!a` are compatible types. The compiler will insert the `seq`s where needed. I don't think this is useless.

First, it serves as good documentation. Documenting strictness properties, e.g. as we do in the container library today, is awkward. Strictness annotations on types would make the documentation precise and succinct.

Second, it's a bit more declarative than having put manually put bang patterns at the right places in the function definition and having to remember (and teach beginners) how to do that correctly..

Third, it might help use generate better code, especially if we also implement Strict Core.

Right. I completely agree. The idea is attractive to me for the same reasons. My questions basically relate to: how would you implement it? Right now GHC's type checker works by solving type equality constraints. Type equality is symmetric, and implies that the two types are substitutable for each other in all contexts: there's no concept of "mixing them up", because there's nothing to get mixed up, they are the same. But `a` and `!a` aren't like that. You very much want to avoid mixing them up, so you can insert `seq`s in the right places. But how would that mesh with the present system? Would you allow strictness annotations on type arguments in arbitrary positions ([!Int] and so forth)? That leads to the issues regarding "how could the compiler know how to strict-ify arbitrary types", and/or co/contra/invariance of type parameters.

I believe this is analogous to what Scala does for their by-value parameters, which types are preceded with a => annotation.

Looks like it's the reverse actually: http://stackoverflow.com/a/6297466

Cheers, Johan

-- Your ship was destroyed in a monadic eruption.

I don't know any way to make a compositional story about nested ! annotations in types. As various of you have pointed out, it looks attractive and then runs out of steam. Putting !'s on data constructor arguments works because it's not really part of the type at all; rather, it just says "give this contstructor a wrapper that makes it strict". I think one could make a similar story for functions in general, so that f :: !a -> a -> ![a] -> Int f a b c = e would mean "add a wrapper to f that makes it strict"; thus f a b c = a `seq` c `seq` e But it's not at all clear that this is worth the fuss. Strict Core is another matter. As the paper says, it's an intermediate language that exposes more about what is evaluated and what is not, and how functions are curried. As I said in an earlier reply, it would certainly be an interesting experiment to make GHC's intermediate language be Strict Core, but it would not be a routine exercise. Fun to be had! Simon From: Johan Tibell [mailto:johan.tibell@gmail.com] Sent: 07 May 2013 21:33 To: Gábor Lehel Cc: Simon Peyton-Jones; Max Bolingbroke; ghc-devs@haskell.org Subject: Re: Implementing Strict Core On Tue, May 7, 2013 at 1:00 PM, Gábor Lehel <illissius@gmail.com<mailto:illissius@gmail.com>> wrote: On Tue, May 7, 2013 at 6:38 PM, Johan Tibell <johan.tibell@gmail.com<mailto:johan.tibell@gmail.com>> wrote: `a` and `!a` are compatible types. The compiler will insert the `seq`s where needed. I don't think this is useless. First, it serves as good documentation. Documenting strictness properties, e.g. as we do in the container library today, is awkward. Strictness annotations on types would make the documentation precise and succinct. Second, it's a bit more declarative than having put manually put bang patterns at the right places in the function definition and having to remember (and teach beginners) how to do that correctly.. Third, it might help use generate better code, especially if we also implement Strict Core. Right. I completely agree. The idea is attractive to me for the same reasons. My questions basically relate to: how would you implement it? A function: f :: !a -> ... would be implemented as f !x = ... i.e. the body of x would start with a `seq` of `x`. I we had Strict Core we could do better and instead demand that the caller does the evaluation, removing cases of duplicate reevaluation and perhaps expose more unboxing. Right now GHC's type checker works by solving type equality constraints. Type equality is symmetric, and implies that the two types are substitutable for each other in all contexts: there's no concept of "mixing them up", because there's nothing to get mixed up, they are the same. But `a` and `!a` aren't like that. You very much want to avoid mixing them up, so you can insert `seq`s in the right places. But how would that mesh with the present system? I honestly don't know. Possibly we could just erase the strictness annotations after we have annotated `f` as being strict in its first argument. Would you allow strictness annotations on type arguments in arbitrary positions ([!Int] and so forth)? That leads to the issues regarding "how could the compiler know how to strict-ify arbitrary types", and/or co/contra/invariance of type parameters. My current thinking is that we would only allow `!` at the "top-level". Even if we defined a meaning for e.g. `f !a`, I don't know if it would be very useful as we wouldn't be able to say things about specific fields. For example, given data T a = C a a should `T !a` mean that both fields are strict? What if we only want one to be strict? What if the type is opaque to the user, how is he/she supposed to know what `T !a` means without referring to implementation details? I believe Scala has the same restriction. The only thing I would regret if `!` is only allowed at the top-level is that we couldn't reuse e.g. Haskell pairs for both lazy and strict pairs, which would be neat. Looks like it's the reverse actually: http://stackoverflow.com/a/6297 using466<http://stackoverflow.com/a/6297466> I might have used the word "analogous" incorrectly. I meant: similar to what Scala does, except that Scala is strict by-default and adds by-name parameters through annotations. -- Johan