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.
- 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.
- 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.
________________________________
From: ghc-devs-boun...@haskell.org [ghc-devs-boun...@haskell.org] on behalf of
Gábor Lehel [illiss...@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.tib...@gmail.com<mailto:johan.tib...@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
