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