On Tue, May 7, 2013 at 4:02 PM, Sturdy, Ian <sturdy...@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-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>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.
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
