The first one is syntactic sugar for when you construct a thing.
Strict a b ~ a `seq` b `seq` Lazy a b
The second one is a magic tag in STG applied on pattern matching.
foo (Lazy a _) = a -> case a_0001 of
bar (Strict a _) = a -> case a_0002<TagProper> ofAh, perhaps I understand. To me I think of it as “because the first has happened then we are also allowed to apply the second (which is an optimization)”. Does that match your understanding?
Yes, making invalid laziness unrepresentable[1] is essential for avoiding space leaks whilst keeping your sanity, in my opinion. Anything that you have to remember to do (for example bang patterns on function arguments, strict let bindings, applying functions with $!) for correct program behaviour imposes a large mental cost. I want to minimize the amount of stuff I have to remember. That’s why I use Haskell after all!
[1] I even wrote an article about it: make-invalid-laziness-unrepresentable
Not “the first thing has happened”, but instead “the first thing is guaranteed to have happened based on the datatype definition”. I haven’t checked any further, but I expect GHC to apply this tag every time it can prove prior evaluation, and if true for those cases it would directly be “the first thing has happened”.
Alternatively, we could use an implementation that has no (heap) space to leak e.g. figure 9 on page 24 of On Inter-deriving Small-step and Big-step Semantics: A Case Study for Storeless Call-by-need Evaluation (2011). Now if that could be implemented in GHC (or some other Haskell implementation), I believe it would greatly reduce the need for strictness annotations…and the need for “semi-duplicate” types with varying levels of strictness.
That we have “semi-duplicate” definitions for varying levels of imperativity (e.g. map and mapM) already provides more than enough annoyance!
Erratum: I got the year wrong. 2011 was when the preprint was submitted - the paper was actually published in 2012 >_<
That article starts strong:
A famous functional programmer once was asked to give an overview talk. He began with “This talk is about lazy functional programming and call by need.” and paused. Then, quizzically looking at the audience, he quipped: “Are there any questions?” There were some, and so he continued: “Now listen very carefully, I shall say this only once.”
Definitely have to check that one out 
So far we have considered types like
data Maybe a
= Nothing
| Just a
and
data Maybe2 a
= Nothing2
| Just2 !a
But what about types like
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE UnliftedDatatypes #-}
import Data.Kind
import GHC.Exts
type Brut = TYPE (BoxedRep Unlifted)
type Maybe3 :: Type -> Brut
data Maybe3 a
= Nothing3
| Just3 a
and
type Maybe4 :: Type -> Brut
data Maybe4 a
= Nothing4
| Just4 !a
?
That’s an interesting reference! Although I doubt that a storeless approach will actually need less space than a … storeful machine with a garbage collector. Furthermore, by storing all heap bindings on the stack, it’s quite complicated to reclaim dead bindings. Well, you could copy collect the whole stack or relink stack frames… But the fundamental problem with space leaks is that some thunk retains a huge working set – nothing about moving the heap into the stack will change that.
…for actual node data, I would tend to agree - it’s (most of the) metadata usually associated with GC that could probably be elided, thereby reducing the overall size of those thunk and their working sets in memory.
But the fundamental problem with space leaks is that some thunk retains a huge working set […]
What would be interesting is to try extending the approach with parallelism (i.e. multiple stacks) to observe what happens (or can be done) which such thunks:
would those thunks and associated working sets be confined to a few stacks?
if so, the tasks with those overly-sized stacks could be given a temporary increase in priority in an attempt to complete them, thereby freeing their stack space.
But this is all conjecture, and there’s been no shortage of that for heapless (or GC-less) approaches to lazy evaluation in the past. That we (in Haskell :-) are all still using GC-managed heaps would appear to suggest that suitable approaches (assuming they exist at all) have yet to be found for production implementations (like GHC).
Huh, so this is UnliftedDatatypes (GHC 9.2+) and unlike strictness flags, which force an evaluation of a field, this allows direct creation of datatypes with no potential bottom.
As with strictness flags, this is great for library performance, but I don’t think it’s making it into base any time soon (and caring about something this tiny in your day-to-day is an overkill).
Unfortunately you can’t even do the most basic things with Bruts, such as put them in a list. By contrast strict-wrapper works with everything in the existing ecosystem with minimal ceremony.
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE UnliftedDatatypes #-}
import Data.Kind
import GHC.Exts
type Brut = TYPE (BoxedRep Unlifted)
type Maybe3 :: Type -> Brut
data Maybe3 a
= Nothing3
| Just3 a
-- test18.hs:13:7: error: [GHC-83865]
-- • Expected a lifted type, but ‘Maybe3 ()’ is a boxed unlifted type
-- • In the type signature: a :: [Maybe3 ()]
-- |
-- 13 | a :: [Maybe3 ()]
-- | ^^^^^^^^^
a :: [Maybe3 ()]
a = []
In all fairness you define strict variations of datatypes in your package and use unsafeCoerce, so the “minimal ceremony” argument only doesn’t apply to unlifted datatypes because noone made a library for it yet.
In all fairness …
I disagree that’s a fair assessment.
noone made a library for it yet
@sgraf has made a library for it, data-elevator.
the “minimal ceremony” argument only doesn’t apply to unlifted datatypes …
I didn’t mean “minimal ceremony” in defining them, I meant in using them. You simply can’t use unlifted data types with the rest of the ecosystem as it currently is. You need to wrap and unwrap them at every use site because the ecosystem expects lifted data types everywhere. But that wrapping and unwrapping completely defeats the point of using unliftedness, because it introduces liftedness!
Until there’s "unlifted base" and indeed a whole unlifted ecosystem (or levity-polymorphic base and levity-polymorphic ecosystem) using unlifted types to avoid space leaks wins you nothing over strict-wrapper.
EDIT: By the way, I’m not wedded to “my package”. I am wedded to the idea of eliminating space leaks from Haskell, because they are one of the top reasons that Haskell might fail as an industrial language (behind difficulty onboarding and ecosystem instability). If there’s a better way to “make invalid laziness unrepresentable” I’ll promote that instead. But it turns out that strict-wrapper is the best way I know of so far.
Btw., I would not recommend usage of data-elevator in productive code bases.
Due to the bidirectional nature of how coercions work today (unsafe or not), it is too easy for the optimiser to push coercions around. Technically, the implementation of unsafeCoerce prohibits floating out these coercions (so there’s no way to accidentally make code stricter), but they might still be pushed inwards.
Arguably, such careless floating will most likely lead to a Core Lint error due to the kind changing nature of such heterogeneous coercions (we are going from Lifted to Unlifted or vice versa, after all), but I wouldn’t be surprised to see misoptimisation.
That said, I have not been able to come up with unsound examples so far.
The plan is to use a blessed version of unsafeCoerce as soon as one becomes available, for example https://github.com/ghc-proposals/ghc-proposals/pull/530. The main point about data-elevator is its API.
Do you mean “bidirectional” in that Coercible a b is equivalent to Coercible b a, or something else?
space leaks … are one of the top reasons that Haskell might fail as an industrial language
I don’t believe this is a language problem, but instead a failure to reason about code correctly on programmer’s part. You can’t “fix” laziness in Haskell, you can only create a library that defines a new set of arcane rules, fighting an uphill battle both against the syntax (if it’s so important, why isn’t it a part of the language?) and the programmer (who isn’t learning about laziness, they’re learning your library).
The problem I see is paranoia, people getting the wrong impression that the language was designed wrong and that they have to use one of the libraries to shield themselves from the harmful influence of thunks. In my experience I’ve only run into a large space leak once in like four years, stemming directly from the fact that I didn’t know what I was doing and it was solved with just a few bang patterns.
Yes, exactly. The symmetry rule associated with GHC’s coercion system doesn’t really work well when coercions appear to change evaluation order. In practice, that evaluation order is actually encoded in Core via Case binding rather than Let binding, right after desugaring, which makes this issue hard to exploit.
@BurningWitness, I completely disagree! Point by point
I don’t believe this is a language problem, but instead a failure to reason about code correctly on programmer’s part
I don’t think it’s a language “problem” either. However, I want programmers to not to have to reason about code when that reasoning can be done automatically by the machine! That’s why I use Haskell in the first place and why I value “making invalid states unrepresentable”.
You can’t “fix” laziness in Haskell
I don’t want to “fix” laziness. I want to make it easier to avoid programming mistakes that are easy to make due to laziness being the default.
you can only create a library that defines a new set of arcane rules
I’m not sure what “arcane rules” you are referring to. By “a library” are you referring to strict-wrapper? If so I would deny that it defines “arcane rules”! Quite the opposite. It is extremely simple and only requires familiarity with pre-existing, basic, Haskell concepts.
fighting an uphill battle both against the syntax (if it’s so important, why isn’t it a part of the language?)
One of the things that is wonderful to me about Haskell is that so many things can be libraries rather than having to be baked in to the language. In fact, that’s one of the benefits we get from laziness by default!
and the programmer (who isn’t learning about laziness, they’re learning your library).
I don’t really follow why that’s part of an uphill battle … In any case, I love it when libraries prevent the need to learn hard concepts! (For example, that’s why STM is so wonderful.) But I don’t think strict-wrapper stops a programmer from needing to learn about laziness. But it does mean that she doesn’t have to remember to apply that knowledge in each relevant situation. She is instead prompted to apply it by the type system. That’s exactly what I love about Haskell.
The problem I see is paranoia, people getting the wrong impression that the language was designed wrong and that they have to use one of the libraries to shield themselves from the harmful influence of thunks.
I’m sorry if you got the impression that I’m paranoid about laziness or that I think the language was designed wrong. That’s not what I think at all.
In my experience I’ve only run into a large space leak once in like four years, stemming directly from the fact that I didn’t know what I was doing and it was solved with just a few bang patterns.
You’re very lucky! In my professional use of Haskell I have come across many space leaks written by well-known Haskellers who you have likely heard of, some of which caused gigabytes of extra memory residency. For example, megaparsec is one of the most widely-used parser libraries. It had a space leak that almost every user will have hit (until I fixed it).
It’s an unfortunate rule for other reasons too, for example it rules out Coercible ValidatedEmailAddress String and other similar "newtype with smart constructor" approaches to type safety.
I have google’d references to the KAOS system and I cannot find anything relating to an OS like that. Do you have a link at hand?
These are by John Cupitt:
The design and implementation of an operating system in a functional language (1989)
A Brief Walk Through KAOS (1989)
There’s also an article by David Turner (published in 1990?), but I don’t recall the title - it may have been in one of those “conference compendiums” of that time.
…actually, David Turner wrote at least two articles:
Functional programming and communicating processes (some design considerations for a functional operating system) (1987)
An approach to functional operating systems (1990)