Thanks!

Implement the Strict data type only. Doing so provides the same semantics at the cost of more syntactic overhead.

More syntactic overhead, but also more composable! I don’t need Bool and StrictBool and Maybe and StrictMaybe, I can use Strict Bool and Strict Maybe.

At first glance, this makes me lean much more towards the Strict proposal.

Ah, but this allows you to implement Strict, so we can have our cake and eat it too. Compelling!

Yes, the only real drawback compared to implementing Strict only would have been that this is a superset of the functionality #257 provides, so ideally should be implemented in a separate proposal. But having done a little prototyping, I think that we would have to make Force an actual DataCon anyway, so that it is properly handled by the simplifier and other passes. At this point adding the tiny bit of surface syntax is just a stone throw away, hence @simonpj argued in favor of this proposal instead.

I assume that we want to UNPACK those strict fields, but I think this cross-kind UNPACK is slightly novel and should be explicitly spelled out in the proposal (and the other proposal too).

A bit off topic:

I hope someday every data type can have an associate unboxed version connected by a type family (let's call it Unbox), and then UNPACK can have a type directed desugaring. Even better if we can do

• LiftedBoxedFoo ~R LiftedHsPtr (Unbox LiftedBoxedFoo)
• UnliftedBoxedBar ~R UnliftedHsPtr (Unbox UnliftedBoxedBar)

Then Strict essentially gives us UnliftedHsPtr (Unbox LiftedBoxedFoo).

cross-kind UNPACK is slightly novel and should be explicitly spelled out in the proposal

What do you mean by cross-kind? It's just unpacking the regular constructor fields like before, that's entirely orthogonal to the semantic concern of there being no bottom as an inhabitant of that constructor's type.

Unless you mean the implicit unpacking of constructors like Force, that's an entirely different matter but with no consequences for perceived semantics, it's just an optimisation affecting operational semantics. Note that this doesn't UNPACK Forces argument, rather we want to coerce Strict a to a in Core like we do for newtypes, except that one way (a to Strict a) isn't actually zero-cost, but erase to a seq. See Simon's earlier comment and my remarks in https://gitlab.haskell.org/ghc/ghc/wikis/unlifted-data-types#proposal-b4-levity-polymorphic-functions.

I hope someday every data type can have an associate unboxed version connected by a type family (let's call it Unbox)

There are plans for having levity polymorphic (unlike the current meaning of levity polymorphism, which is more like representational/shape polymorphism) data types. See https://gitlab.haskell.org/ghc/ghc/wikis/unlifted-data-types#proposal-b3-levity-polymorphic-data-types for a design I would aim at.

Generally I like the idea here, and I don't think it'd be all that hard to implement. We already have unlifted data types like Array#; this just makes them user-definable.

On syntax, a postfix kind signature is rather a quiet signal for such an important change. I'd suggest using a prefix keyword:

data unlifted SPair = SP Int INt

(This "keyword" would have significance only after data so it wouldn't prevent you using "unlifted" as, say, a variable name.

@sgraf812

Note that this doesn't UNPACK Forces argument, rather we want to coerce Strict a to a in Core like we do for newtypes, except that one way (a to Strict a) isn't actually zero-cost, but erase to a seq.

Well I'd want

data Strict :: Type -> TYPE 'UnliftedRep where
  Strict :: {-# UNPACK #-} !a -> Strict a

data UPairStrict :: Type -> Type -> TYPE 'UnliftedRep where
  UPairStrict :: {-# UNPACK #-} !a -> {-# UNPACK #-} !b -> SPair a b

to work somewhat similarly. The second cannot be conceived of as a one-way coercion.

@simonpj But see how https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0098-unlifted-newtypes.rst#id4 points the way to levity-polymorphic newtypes. I think the kind signature is more in tune with that.

@Ericson2314 If I understand correctly, then I don't think what you want to have is possible. You can't unpack polymorphic fields, at least not without specialisation of the data type, at that's certainly out of scope for this proposal. To exemplify, what is the static offset of the b field in UPairStrict? If we'd unpack the a field, then it depends on the size of the representation of a, which means you can't use UPairStrict in code polymorphic over a.

UNPACK concerns the fields of a constructor (Force's, in particular). After unpacking, the heap object still has its own header. I was rather aiming at making the constructor Force have no representation at runtime at all, because its only field is conveniently of the exact same representation as the constructor itself (i.e. a pointer to the heap).

This is probably most similar in spirit to turning a lifted data type with a single strict boxed field (So as Strict above, but with regular 'LiftedRep) into a newtype, except that that would be broken semantics because a pattern match on the constructor actually evaluates the field (as opposed to newtypes).

The proposal mentions that we could have an unlifted Ptr type. But that wouldn't be a drop-in replacement for the current Ptr type, because it has an unlifted kind and therefore can't be passed to polymorphic functions or stored in polymorphic data structures, right? e.g. you can't have a [Ptr a] when Ptr is unlifted. That should probably be mentioned as a drawback.

(aside from this I'm strongly in favour of the proposal)

@simonmar Yes, currently we have no means of encoding the necessary levity polymorphism. See https://gitlab.haskell.org/ghc/ghc/wikis/unlifted-data-types#proposal-b3-levity-polymorphic-data-types in that regard. I think levity polymorphism (i.e. lifted vs. unlifted, but still boxed pointer to GC'd heap, as opposed to the current interpretation, which is more like representation/shape polymorphism) should be discussed in a subsequent proposal.

Or maybe it should be part of this proposal, I've no idea what the guidelines are wrt. incrementality of GHC proposals. But I'd rather implement it in separate steps.

@sgraf812 Right, I completely forgot about in normal cases need a concrete constructor to unpack, so no polymorphism there.

But perhaps we do anything special with data AlmostNewtype a = AlmostNewtype !a today? By code gen, whether matching on AlmostNewtype forces anything should be irrelevant, and the same unboxing opportunities should be available. Perhaps we should, so the Strict unpacking is less of a one-off optimization.

Back to my original, question I assume plain:

data Strict :: TYPE 'UnliftedRep where
  Strict :: {-# UNPACK #-} !Concrete -> Strict a

data UPairStrict :: TYPE 'UnliftedRep where
  UPairStrict :: {-# UNPACK #-} !Concrete0 -> {-# UNPACK #-} !Concrete1 -> SPair a b

works fine?

I do really really want "template" / "monomorphized" polymorphism, but I think should be separate proposal. There is much to decide about that alone.

Not knowing about this proposal I just added #268. I noticed that we already have support for unlifted types with just one constructor via newtype and that it can be extended to more types with possible compiler simplification by implementing case analysis in two ways, one for data and one for newtype instead of mere coercing (I think I read that's what you do).

Coercing between unlifted and lifted rep are not actually essential to the proposal. Levity polymorphic coercions might be interesting to have in Core to support a zero-cost Strict data type, but that's irrelevant to Haskell as a language. It might become relevant later on when we want to have levity polymorphism (in the sense of lifted vs. unlifted, not boxed vs. unboxed) in the surface language.

I don't see how implementing case analysis in two ways leads to compiler simplification. Note that case already works on terms of unlifted rep, so my proposal wouldn't actually imply a change to semantics at all. Everything is already in place! We just offer the needed vocabulary to the programmer to define her own unlifted data types.

By code gen, whether matching on AlmostNewtype forces anything should be irrelevant, and the same unboxing opportunities should be available. Perhaps we should, so the Strict unpacking is less of a one-off optimization.

Hmm. I felt a strong urge to disagree but couldn't come up with an example. So perhaps eliminating indirections for types like AlmostNewtype (and Strict of course) is indeed a sound transformation, if a little surprising for debugging purposes.

Back to my original, question I assume plain:

data Strict :: TYPE 'UnliftedRep where
  Strict :: {-# UNPACK #-} !Concrete -> Strict a

data UPairStrict :: TYPE 'UnliftedRep where
  UPairStrict :: {-# UNPACK #-} !Concrete0 -> {-# UNPACK #-} !Concrete1 -> SPair a b

works fine?

Yes, it should just unbox the fields, as today.

I do really really want "template" / "monomorphized" polymorphism, but I think should be separate proposal. There is much to decide about that alone.

The best bet is probably a backpack inspired solution. See unpacked-containers for example.

What are the semantics of Strict?

This is the definition. Its semantics follow straight-forward from the semantics of unlifted expressions (i.e. everything unlifted is evaluated by default, because that's the only way to make sure there is no bottom anywhere).

See also #257.

can I pattern match on x : Strict (GHC.Tuple.Unit a)?

case x of {Force (Unit y) = y}

what is undefined :: Strict (GHC.Tuple.Unit a) ? is it still _|_ - or Force _|_?

How do you force types with two constructors? The attempt to force will be _|_ won't it, meaning the type isn't lifted.

Oh I see you can pattern match as above, the tree example is missing parentheses but I'm still curious about the matter of _|_ and undefined

I updated the Change Specification to be more formal. There's an open TODO discussion concerning syntax, so I expect this thread to be on fire very soon 🔥

Great proposal! I wish it at least sketched the path to the zero-cost Strict data type.

The worker-wrapper example is what motivates me write this. Here's the status quo example from the proposal.

foo :: Int -> SPair Int Int
foo x = case $wfoo x of (# a, b #) -> SPair a b

$wfoo :: Int -> (# Int, Int #)
$wfoo x
  | even x
  = (# (x + 1), x #)
  | otherwise
  = case $wfoo (x-1) of
      (# a, b #) -> (# a+1, b+1 #)

To me it's a bit surprising that the type of $wfoo is not Int# -> (# Int#, Int# #) (maybe I'm overlooking something trivial). I'd like to see worker-wrapper transform that produces the second type signature, and I'm assuming it will happen at some point. And it would be a shame if Strict would get in the way of it because it cannot accept unboxed arguments.

I have just realised that in this accepted, and implemented proposal we have done something entirely new. Consider this (from https://gitlab.haskell.org/ghc/ghc/-/issues/20204)

type IntU ::  Bool -> Wombat

...LOTS OF CODE...

data IntU a b = IntU Int

...MORE CODE...

type Wombat =Type -> TYPE UnliftedRep

The kind signature for IntU completely changes the semantics of the data IntU declaration, and yet can be separate from it. That is new: generally, signatures can restrict the applicability of something, but don't change its semantics. (Yes, with overlapping instances, certainly incoherent instances, you could change semantics, but the general principal holds.)

Even if it is adjacent, the fact that it's unlifted is quite subtle... you have to look to the right of the arrows, and then through the distant (and perhaps imported) type synonym Wombat.

I'm not very happy with a distant kind signature having such a profound effect on the semantics of the data type. Indeed in my comment above I suggested a keyword

data unlifted IntU a b = IntU Int

to signal that it's an unlifted data type. But then I went AWOL and didn't pursue the matter. I don't know why I was so negligent.

So this post is to ask: does anyone else think this is bizarre? I'm inclined to make a proposal to add the keyword, but I thought I'd test the waters first.

See the 5ish comments starting at #265 (comment) for why we decided to omit the keyword.

Thanks. I'd missed them (I think GitHub didn't load them).

But still that seems way short of a "decision". More a few remarks from a handful of people.

I'm very bothered about this, and I feel negligent having let it go by. (I'd be perfectly happy allowing data lifted too.)

Instead of adding a keyword, this could be another case where modifiers could come in handy? As in,

-- Existing type already exposed via GHC.Exts:
-- | Whether a boxed type is lifted or unlifted.
data Levity = Lifted | Unlifted

%Unlifted
data SMaybe a = SJust !a | SNothing

Edit: Below the above-mentioned 5ish comments, Simon mentioned taking into account levity polymorphism (#265 (comment)). It's not clear to me at the moment how one might make this work with either the keyword or modifier approach, but incorporating this into the modifier approach somehow does seem like it would be easier.

Also, if we use keywords or modifiers for unlifted datatypes, presumably the same would have to be allowed for unlifted newtypes.

The kind signature for IntU completely changes the semantics of the data IntU declaration, and yet can be separate from it.

Don't we already have similar behavior with normal functions and type classes:

x :: Double
-- x :: Int

-- lots of code

x = 1

main = print x

Will print 1 or 1.0 depending on the distant type signature. In this case the semantic change is very small, but more complicated functions and classes can change the semantics entirely.

I don't think this is very strange.

FWIW I'm very surprised to learn that type signatures can be separated from definitions like this!

I'm sympathetic to Simon's concern here, but I'm not as bothered: I don't feel the need to include a new keyword.

On the other hand, I'd be happy with a modifier (thanks for the idea @JakobBruenker), along with a -Wall warning that bleated whenever the modifier is absent for a non-lifted type. (Non-lifted = not necessarily lifted; unlifted = unlifted. That is, non-lifted includes levity-polymorphic.)

I might also add that as tooling gets better, the textual data type definition becomes less and less relevant while understanding code. Heck, even if I hover over a type like CoreExpr in my editor today, I get the tooltip

> CoreExpr :: * 

 *Defined in ‘GHC.Core’*

Note the *. For IntU, I'd get Bool -> Wombat, as expected. It's no longer the job of the programmer to find and put signatures and definitions together, you can just let the tool do it.

I'm not against a keyword or modifier if people find the current behavior confusing, but I still want to point out that keywords won't help to define a levity-polymorphic data type. You are still stuck with a kind signature (standalone or not) in that case. And then you have the same problem as before. Worse, actually, because now a type parameter determines levity of the data type. So you might find that one use site behaves as unlifted while the other as lifted.

Point being: There's no way out of confusion other than having reliable tooling, which we already have.

I agree with @sgraf812's observation. More generally: as our language gets more intricate, our tools need to keep apace. This is why e.g. Agda and Idris are out ahead of Haskell with tooling. Those languages are more intricate, and so the tooling must be up to the task. For a long time, Haskell has limped along with sub-par tooling, because, well, I don't know why. As the tooling catches up, though, we can new flexibility in design -- for example, by making things less obvious in the code text if they can be clarified by tools.

@simonpj: you prodded this conversation to start. How do you feel about this all now?

Ugh. When I started this conversation had forgotten about

type T :: forall (l :: Levity) -> TYPE (BoxedRep l)
data T l = MkT Int

Now (T Lifted) is lifted, while (T Unlifted) is unlifted; so clearly we can't put a fixed keyword on the data type declaration.

That does leave me a bit stuck. A keyword isn't going to work.

The only viable alterantive is to insist that if the return kind isn't Type then you must declare it in the declaration, thus

data T l :: TYPE (BoxedRep l) where
  MkS :: Int -> T l

I forget -- was that possibility discussed? (I don't think we have a way to declare a return kind in H98 syntax, do we?)

I'm still clinging to the idea that we should be able to infer a kind from a declaration; a signature should make it less polymorphic, but not more. (And yes I know that polymorphic recursion breaks this, but not badly.)

Any other views?

I don't think we have a way to declare a return kind in H98 syntax, do we?

That is exactly the problem. I find H98 quite nice for declaring simple data types such as SMaybe or IntSet, but YMMV. @RyanGlScott and I discussed it very briefly in https://gitlab.haskell.org/ghc/ghc/-/merge_requests/2218#note_335773, but the proposal already included SAKS at the time, probably from a decision I made here.

Another gripe I'd have with it is that -XUnliftedNewtypes works with SAKS, so why wouldn't -XUnliftedDatatypes?

Again, I'm not strongly against disallowing SAKS, but it seems awfully surprising not to allow them from a design perspective. Especially given that they work for all lifted data types. Also to me separating the SAKS from the data type declaration is a code smell to begin with (wasn't syntactic distance the reason you gave in #265 (comment)?). Arguably, the mix up in https://gitlab.haskell.org/ghc/ghc/-/issues/20204 could have happened just as well for a CUSK. I think our eyes merely aren't trained to give SAKS the attention they deserve yet.

I am absolutely not suggesting that we disallow a standalone kind signature! I'm only suggesting that you can infer the kind from the declaration. It may be narrowed by the SAKS.

With unlifted newtypes you can infer the signature, right?

newtype N = MkN Int#

I can see that is unlifted without looking at its signature.

With unlifted newtypes you can infer the signature, right?

You can write this:

type T :: TYPE (BoxedRep r) -> TYPE (BoxedRep r)
newtype T a = T a

Ah yes. So in my straw-man idea, that would be illegal because looking at the newtype decl alone we'd default to lifted. If you want something more general you'd have to decorate the newtype decl itself.

But maybe I am a lone voice.

But maybe I am a lone voice.

Perhaps. But you've been at this for some time and have had a modicum of success, so it's a voice we should listen to.

What about my modifier story?

type N :: TYPE (BoxedRep l) -> TYPE (BoxedRep l)
%HasUnusualKind
newtype N a = MkN a

The %HasUnusualKind modifier is optional, but we could create a warning that would bleat if you leave it out. It's a marker to the reader to look for the SAKS. (Ditto it all for datatypes.) %HasUnusualKind requires the presence of a SAKS.

My own preference is not to have %HasUnusualKind and just to say that the type signature is part of the declaration, but I think the modifier approach could be a way forward toward compromise.

But why would you invent new modifiers rather than use what we already have: kind signatures?

So you would be fine with a warning, rather than an error? -Wgeneralising-standalone-kind-signature perhaps, suggesting to use a CUSK instead? That indeed sounds plausible to me. Although it sounds much more like something a Linter would suggest.

Feels weird to introduce something that goes against the general trend of moving away from CUSKs and towards SAKs, no?

I'm not arguing for a complete user supplied kind (CUSK). The CUSK story was principally to suport polymorphic recursion (user manual entry). That's not at all waht I am talking about here.

I'm only talking about defaulting of the return kind of a data type: to be other than Type, you need an explicit kind signature.

I'm not arguing for a complete user supplied kind (CUSK). The CUSK story was principally to suport polymorphic recursion (user manual entry). That's not at all waht I am talking about here.

I'm only talking about defaulting of the return kind of a data type: to be other than Type, you need an explicit kind signature.

Do we agree, though, that it's already what the proposal says?

Do we agree, though, that it's already what the proposal says?

No, I don't think so. See my original post above, in which we find that

• Looking at the data type declaration on its own, it looks lifted
• But a possibly-distant kind signature makes it unlifted

In fact the proposal says "Specifying a kind signature is the only way to declare an unlifted or levity-polymorphic data type." Is that really true? If I say

data S a :: TYPE UnliftedRep where ...

surely I get an unlifted type?

My suggestion is the opposite of the one in the quote above. I'm suggesting that

• The only way to declare an unlifted or levity-polymorphic data type is using a kind signature in the declaration itself.

so that type inference on the declaration will yield the right kind. (A standalone kind signature might specialise that kind, just as for term level declarations.)

In fact the proposal says "Specifying a kind signature is the only way to declare an unlifted or levity-polymorphic data type." Is that really true? If I say

data S a :: TYPE UnliftedRep where ...

surely I get an unlifted type?

This has a kind signature. So I think it doesn't make the statement from the proposal incorrect.

My suggestion is the opposite of the one in the quote above. I'm suggesting that

• The only way to declare an unlifted or levity-polymorphic data type is using a kind signature in the declaration itself.

so that type inference on the declaration will yield the right kind. (A standalone kind signature might specialise that kind, just as for term level declarations.)

I, for one, find this requirement rather weird. It would be the only place in the language where we make this sort of requirement. Despite the fact that specifying a toplevel type signature does change a whole lot of things for other kind of declarations. For one thing, it changes the typechecking algorithm from inferring mode to checking mode. Or, closer to my heart (and to what's happening in this proposal), it lets one define a linear function rather than an unrestricted function.

This effect at a distance has never been a problem (in great part because people are fairly careful not to put the signature far away from the declaration; in fact, I'm pretty sure many Haskellers are not even aware that it's a possibility). I don't believe that it will be in this case either. I'm personally in favour of leaving the proposal in this state.

@tomjaguarpaw FWIW I'm very surprised to learn that type signatures can be separated from definitions like this

@gridaphobe [on the Steering Committee discussion last month] I think the distance between the type IntU and data IntU is the crux of the issue. If we were forced to keep the signature and declaration together, ...
I've never been particularly fond of Haskell's tolerance for separating signatures and definitions.

I agree, and it afflicts -XScopedTypeVariables too: the significance of the explicit forall is not something you'd pay attention to if the decl is a long way from the binding.

We need a syntactic way to group [**] a type(-of-type) decl with its binding (and other stuff). Some ideas that don't clash with current syntax:

let type IntU ::  Bool -> Wombat                          -- top-level `let`
    type Wombat =Type -> TYPE UnliftedRep
 in data IntU a b = IntU Int

   type IntU ::  Bool -> Wombat                           -- these must be indented deeper than the `in`
   type Wombat =Type -> TYPE UnliftedRep
in data IntU a b = IntU Int

{ type IntU ::  Bool -> Wombat
  type Wombat =Type -> TYPE UnliftedRep
  data IntU a b = IntU Int
}

type IntU ::  Bool -> Wombat
;; type Wombat =Type -> TYPE UnliftedRep
;; data IntU a b = IntU Int

(The last is stolen from BCPL's 'very binding semicolon'. It actually seems to be currently valid Haskell syntax, with apparently the same meaning as a single semicolon in the same position/allowing the following decl to be indented as far as you like; or same as no semicolon at all without indenting. Hmm I like that/might start using it anyway.)

The semantics is to be as currently/proposed here if these were each stand-alone decls. (So Wombat gets top-level scope.) Except that if we supported something like this for -XScopedTypeVariables, the explicit forall would be optional.

For this proposal, if the three decls were given separately stand-alone: infer the usual type (usual liftedness) for IntU from the data decl alone (possibly with an embedded/inline signature); later discover the type IntU ...; type Wombat ...; check IntU's inferred type against the decl'd signature; reject if not consistent -- that is, if the signature is not merely less polymorphic than inferred.

[**] another place we could use grouping is for pattern sigs with their binding -- that would avoid the need to repeat the pattern keyword, and help signal that pattern sigs are bizarre, as compared with function sigs.

I believe this should have an Implemented label.

(Should there be an explicit policy that random passers-by may ping someone to add missing labels?

Thanks! You guessed the policy correctly; where should it be made explicit so that you would have seen it? Feel free to propose a PR

@sgraf812 I just found out that the motivation in this proposal is not that strong, because you can get the same speedup by simply making the recursive fields of IntSet strict too:

data IntSet
  = Branch !IntSet !Int !IntSet
  | Leaf

Perhaps the motivation should focus more on avoiding the need to put bang patterns everywhere and that we now have bona fide algebraic data types.

@sgraf812 I just found out that the motivation in this proposal is not that strong, because you can get the same speedup by simply making the recursive fields of IntSet strict too:

data IntSet
  = Branch !IntSet !Int !IntSet
  | Leaf

Perhaps the motivation should focus more on avoiding the need to put bang patterns everywhere and that we now have bona fide algebraic data types.

I believe this is mostly a result of tag inference, something that hadn't been merged yet when this proposal was written.

There are also some edge cases where tag inference doesn't help (things involving boot files, functions not being W/Wed and others) so I think the spirit of the motivation still holds. Even if the exact example isn't as striking anymore.