Implementing Strict Core

Tue May 7 21:29:06 CEST 2013

On Tue, May 7, 2013 at 4:02 PM, Sturdy, Ian <sturdyi12 at 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 at haskell.org [ghc-devs-bounces at haskell.org] on
> behalf of Gábor Lehel [illissius at gmail.com]
> *Sent:* Monday, May 06, 2013 7:14 PM
> *To:* Johan Tibell
> *Cc:* Max Bolingbroke; ghc-devs at haskell.org
> *Subject:* Re: Implementing Strict Core
>
>
>
> On Thu, May 2, 2013 at 6:30 PM, Johan Tibell <johan.tibell at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs
>
>

-- 
Your ship was destroyed in a monadic eruption.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130507/f375ffa1/attachment-0001.htm>