Does an unboxed unit get pushed to the stack?

Tom Ellis

12 Jan 2023 12 Jan '23

1:12 p.m.

If I define bar and baz as below then, as I understand it, calling baz requires pushing an argument onto the machine stack. Is the same true for baz, or is "calling" baz the same as "calling" foo, i.e. no argument needs to be pushed? Thanks, Tom {-# LANGUAGE MagicHash #-} {-# LANGUAGE UnboxedTuples #-} module Bar where import GHC.Prim foo :: Int foo = 1 bar :: (# #) -> Int bar (# #) = 1 baz :: () -> Int baz () = 0

Show replies by date

Bertram Felgenhauer

12 Jan 12 Jan

3:01 p.m.

Tom Ellis wrote:

...

If I define bar and baz as below then, as I understand it, calling baz requires pushing an argument onto the machine stack. Is the same true for baz, or is "calling" baz the same as "calling" foo, i.e. no argument needs to be pushed?

{-# LANGUAGE MagicHash #-} {-# LANGUAGE UnboxedTuples #-}

module Bar where

import GHC.Prim

foo :: Int foo = 1

bar :: (# #) -> Int bar (# #) = 1

baz :: () -> Int baz () = 0

There is more to the story than just arguments. Assuming that nothing gets inlined, - "calling" foo simply uses the existing `foo` closure (at the top level it becomes a static indirection) - calling baz pushes an update frame recording where the result goes onto the stack and the argument as well, and calls the entry point for `baz`. Well, conceptually. Actually, the argument is passed in a register on x86_64. - calling bar pushes an update frame, but does not push or pass an argument to the entry point of `bar`. This is specific to `(# #)` being the final argument of the function. For intermediate arguments, the argument is just skipped. So if you had foo :: Int -> Int foo x = x + 42 bar :: (# #) -> Int -> Int bar (# #) x = x + 42 then `foo 1` and `bar (# #) 1` produce identical same code. If the arity of the function is unknown, as in xyzzy :: ((# #) -> a) -> a xyzzy f = f (# #) xyzzy :: (() -> a) -> a xyzzy f = f () then the distinction is delegated to a helper function in the RTS (`stg_ap_v_fast` vs. `stg_ap_p_fast`; `v` stands for "void", while `p` stands for "pointer") that inspects the info table of the `f` closure to determine whether the argument is the final one that needs special treatment, or whether the argument can simply be skipped. Cheers, Bertram

Tom Ellis

3:05 p.m.

On Thu, Jan 12, 2023 at 04:01:48PM +0100, Bertram Felgenhauer via Haskell-Cafe wrote:

...

Tom Ellis wrote:

...
If I define bar and baz as below then, as I understand it, calling baz requires pushing an argument onto the machine stack. Is the same true for baz, or is "calling" baz the same as "calling" foo, i.e. no argument needs to be pushed?

{-# LANGUAGE MagicHash #-} {-# LANGUAGE UnboxedTuples #-}

module Bar where

import GHC.Prim

foo :: Int foo = 1

bar :: (# #) -> Int bar (# #) = 1

baz :: () -> Int baz () = 0

There is more to the story than just arguments. Assuming that nothing gets inlined

Very helpful, thank you!

Tom Ellis

3:12 p.m.

New subject: Unboxed, zero-width :~:/Refl?

Subsequent to Bertram's helpful answer about the unboxed unit tuple as an argument type, I have a follow-up question. Data.Typeable allows me to write a nice API like refl/unRefl below: {-# LANGUAGE GHC2021 #-} {-# LANGUAGE LambdaCase #-} module Example where import Data.Typeable refl :: a :~: a refl = Refl unRefl :: a :~: b -> (a ~ b => r) -> r unRefl = \case Refl -> \r -> r But why I am paying the cost for a boxed argument to unRefl? Is there an alternative API using an unboxed, zero-width equality witness that means I pay minimal cost for its existence? That is, an API like the following where `a :~:# b` is zero-width unboxed? unboxedRefl :: a :~:# a unUnboxedRefl :: a :~:# b -> (a ~ b => r) -> r I guess I can do it the following unpleasant way, if I keep the constructor hidden. But is there a better way? newtype a :~:# a = Refl (# #) unboxedRefl :: a :~:# a unboxedRefl = Refl (# #) unUnboxedRefl :: a :~:# b -> (a ~ b => r) -> r unUnboxedRefl (Refl (# #)) = unsafeCoerce Tom On Thu, Jan 12, 2023 at 04:01:48PM +0100, Bertram Felgenhauer via Haskell-Cafe wrote:

...

Tom Ellis wrote:

...
If I define bar and baz as below then, as I understand it, calling baz requires pushing an argument onto the machine stack. Is the same true for baz, or is "calling" baz the same as "calling" foo, i.e. no argument needs to be pushed?

{-# LANGUAGE MagicHash #-} {-# LANGUAGE UnboxedTuples #-}

module Bar where

import GHC.Prim

foo :: Int foo = 1

bar :: (# #) -> Int bar (# #) = 1

baz :: () -> Int baz () = 0

There is more to the story than just arguments. Assuming that nothing gets inlined,

- "calling" foo simply uses the existing `foo` closure (at the top level it becomes a static indirection)

- calling baz pushes an update frame recording where the result goes onto the stack and the argument as well, and calls the entry point for `baz`. Well, conceptually. Actually, the argument is passed in a register on x86_64.

- calling bar pushes an update frame, but does not push or pass an argument to the entry point of `bar`.

This is specific to `(# #)` being the final argument of the function. For intermediate arguments, the argument is just skipped. So if you had

foo :: Int -> Int foo x = x + 42

bar :: (# #) -> Int -> Int bar (# #) x = x + 42

then `foo 1` and `bar (# #) 1` produce identical same code.

If the arity of the function is unknown, as in

xyzzy :: ((# #) -> a) -> a xyzzy f = f (# #)

xyzzy :: (() -> a) -> a xyzzy f = f ()

then the distinction is delegated to a helper function in the RTS (`stg_ap_v_fast` vs. `stg_ap_p_fast`; `v` stands for "void", while `p` stands for "pointer") that inspects the info table of the `f` closure to determine whether the argument is the final one that needs special treatment, or whether the argument can simply be skipped.

Oleg Grenrus

3:51 p.m.

New subject: Unboxed, zero-width :~:/Refl?

Because you have to actually compute `Refl` for it to be valid. Consirer a lie :: a :~: b lie = lie When you match on `lie` to get a proof of `a ~ b`, it will loop, so you won't make unsafeCoerce out of a thin air. Your a :~:# b doesn't work. you cannot define unboxedRefl: Top-level bindings for unlifted types aren't allowed: unboxedRefl = Refl (##) Also a ~ b is *boxed* constraint, so you need to create it e.g. unUnboxedRefl :: forall a b r. a :~:# b -> (a ~ b => r) -> r unUnboxedRefl (URefl (# #)) r = case unsafeCoerce (Refl :: a :~: a) :: a :~: b of Refl -> r Then you could (try to) have a local lie: myUnsafeCoerce :: forall a b. a -> b myUnsafeCoerce a = let lie :: a :~:# b lie = lie in unUnboxedRefl lie a GHC won't accept it (Recursive bindings for unlifted types aren't allowed: lie = lie). In summary, GHC tries hard to not let you define unsafeCoerce. On 12.1.2023 17.12, Tom Ellis wrote:

...

Subsequent to Bertram's helpful answer about the unboxed unit tuple as an argument type, I have a follow-up question.

Data.Typeable allows me to write a nice API like refl/unRefl below:

{-# LANGUAGE GHC2021 #-} {-# LANGUAGE LambdaCase #-}

module Example where

import Data.Typeable

refl :: a :~: a refl = Refl

unRefl :: a :~: b -> (a ~ b => r) -> r unRefl = \case Refl -> \r -> r

But why I am paying the cost for a boxed argument to unRefl? Is there an alternative API using an unboxed, zero-width equality witness that means I pay minimal cost for its existence? That is, an API like the following where `a :~:# b` is zero-width unboxed?

unboxedRefl :: a :~:# a

unUnboxedRefl :: a :~:# b -> (a ~ b => r) -> r

I guess I can do it the following unpleasant way, if I keep the constructor hidden. But is there a better way?

newtype a :~:# a = Refl (# #)

unboxedRefl :: a :~:# a unboxedRefl = Refl (# #)

unUnboxedRefl :: a :~:# b -> (a ~ b => r) -> r unUnboxedRefl (Refl (# #)) = unsafeCoerce

Tom

On Thu, Jan 12, 2023 at 04:01:48PM +0100, Bertram Felgenhauer via Haskell-Cafe wrote:

...
Tom Ellis wrote:

...
If I define bar and baz as below then, as I understand it, calling baz requires pushing an argument onto the machine stack. Is the same true for baz, or is "calling" baz the same as "calling" foo, i.e. no argument needs to be pushed?

{-# LANGUAGE MagicHash #-} {-# LANGUAGE UnboxedTuples #-}

module Bar where

import GHC.Prim

foo :: Int foo = 1

bar :: (# #) -> Int bar (# #) = 1

baz :: () -> Int baz () = 0 There is more to the story than just arguments. Assuming that nothing gets inlined,

- "calling" foo simply uses the existing `foo` closure (at the top level it becomes a static indirection)

- calling baz pushes an update frame recording where the result goes onto the stack and the argument as well, and calls the entry point for `baz`. Well, conceptually. Actually, the argument is passed in a register on x86_64.

- calling bar pushes an update frame, but does not push or pass an argument to the entry point of `bar`.

This is specific to `(# #)` being the final argument of the function. For intermediate arguments, the argument is just skipped. So if you had

foo :: Int -> Int foo x = x + 42

bar :: (# #) -> Int -> Int bar (# #) x = x + 42

then `foo 1` and `bar (# #) 1` produce identical same code.

If the arity of the function is unknown, as in

xyzzy :: ((# #) -> a) -> a xyzzy f = f (# #)

xyzzy :: (() -> a) -> a xyzzy f = f ()

then the distinction is delegated to a helper function in the RTS (`stg_ap_v_fast` vs. `stg_ap_p_fast`; `v` stands for "void", while `p` stands for "pointer") that inspects the info table of the `f` closure to determine whether the argument is the final one that needs special treatment, or whether the argument can simply be skipped.

Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Tom Ellis

4:24 p.m.

New subject: Unboxed, zero-width :~:/Refl?

On Thu, Jan 12, 2023 at 05:51:58PM +0200, Oleg Grenrus wrote:

...

Because you have to actually compute `Refl` for it to be valid.

Sure, but an unboxed constraint would be unlifted, wouldn't it?

...

Your a :~:# b doesn't work. you cannot define unboxedRefl:

Top-level bindings for unlifted types aren't allowed: unboxedRefl = Refl (##)

Ah, that's interesting. Why is that? I can't immediately see a theoretical blocker. There's a practical one, of course: strict bindings are not allowed at the top level either, I guess to prevent infinite loops. Seems strange though. Does OCaml not allow defining constants at the top level?

...

Also a ~ b is *boxed* constraint, so you need to create it e.g.

That seems enough to make my scheme impossible. By why is it boxed? It doesn't seem like it actually needs any evidence to make it work. Tom

David Feuer

5:58 p.m.

New subject: Unboxed, zero-width :~:/Refl?

On Thu, Jan 12, 2023, 11:24 AM Tom Ellis < tom-lists-haskell-cafe-2017@jaguarpaw.co.uk> wrote:

...

Ah, that's interesting. Why is that? I can't immediately see a theoretical blocker. There's a practical one, of course: strict bindings are not allowed at the top level either, I guess to prevent infinite loops. Seems strange though. Does OCaml not allow defining constants at the top level?

OCaml has a notion of module loading time, at which top level definitions are all run. Haskell has nothing like that.

...

Tom Ellis

21 Jan 21 Jan

4:05 p.m.

New subject: Why can't I bind unlifted values at the top level?

I can't bind unlifted values at the top level: foo = (##) Top-level bindings for unlifted types aren't allowed: foo = (##) I can understand why I shouldn't be able to bind unlifted *expressions* at the top level foo = complicatedExpression Perhaps complicatedExpression doesn't terminate! But why can't I bind _values_, i.e. things that are already evaluated? Given that (##) and proxy# already exist at the top-level it seems reasonable that I should be allowed to define my own! Tom

Ben Gamari

7 p.m.

New subject: Why can't I bind unlifted values at the top level?

Tom Ellis writes:

...

I can't bind unlifted values at the top level:

foo = (##)

Top-level bindings for unlifted types aren't allowed: foo = (##)

I can understand why I shouldn't be able to bind unlifted *expressions* at the top level

foo = complicatedExpression

Perhaps complicatedExpression doesn't terminate! But why can't I bind _values_, i.e. things that are already evaluated? Given that (##) and proxy# already exist at the top-level it seems reasonable that I should be allowed to define my own!

There are a few things going on here. The case you give here is not just unlifted but also unboxed (namely, being an unboxed tuple). It's hard to see how top-level binding of unboxed values would work operationally (e.g. how is the garbage collector to know how to trace this object, given that unboxed objects have no object header?). However, I suspect you do have a point when it comes to unlifted data constructors. I think it would be fine to allow an application of a data constructor of an unlifted type on the top-level: type UMaybe :: Type -> UnliftedType data UMaybe a = UNothing | UJust a x :: UMaybe Int x = UJust 42 Perhaps you could open a ticket for this? Cheers, - Ben

David Feuer

7:10 p.m.

New subject: Why can't I bind unlifted values at the top level?

Unboxed things that don't contain pointers probably don't need to be garbage collected, right? On Sat, Jan 21, 2023, 2:01 PM Ben Gamari wrote:

...

Tom Ellis writes:

...
I can't bind unlifted values at the top level:

foo = (##)

Top-level bindings for unlifted types aren't allowed: foo = (##)

I can understand why I shouldn't be able to bind unlifted *expressions* at the top level

foo = complicatedExpression

Perhaps complicatedExpression doesn't terminate! But why can't I bind _values_, i.e. things that are already evaluated? Given that (##) and proxy# already exist at the top-level it seems reasonable that I should be allowed to define my own!

There are a few things going on here. The case you give here is not just unlifted but also unboxed (namely, being an unboxed tuple). It's hard to see how top-level binding of unboxed values would work operationally (e.g. how is the garbage collector to know how to trace this object, given that unboxed objects have no object header?).

However, I suspect you do have a point when it comes to unlifted data constructors. I think it would be fine to allow an application of a data constructor of an unlifted type on the top-level:

type UMaybe :: Type -> UnliftedType data UMaybe a = UNothing | UJust a

x :: UMaybe Int x = UJust 42

Perhaps you could open a ticket for this?

Cheers,

- Ben _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Jaro Reinders

9:52 p.m.

New subject: Why can't I bind unlifted values at the top level?

On 21-01-2023 20:00, Ben Gamari wrote:

...

However, I suspect you do have a point when it comes to unlifted data constructors. I think it would be fine to allow an application of a data constructor of an unlifted type on the top-level:

type UMaybe :: Type -> UnliftedType data UMaybe a = UNothing | UJust a

x :: UMaybe Int x = UJust 42

Perhaps you could open a ticket for this?

This ticket seems related: #17521 Consider top-level unlifted bindings [1]. Or do you think it needs a separate ticket? Cheers, Jaro [1] https://gitlab.haskell.org/ghc/ghc/-/issues/17521

Tom Ellis

10:06 p.m.

New subject: Why can't I bind unlifted values at the top level?

On Sat, Jan 21, 2023 at 10:52:33PM +0100, Jaro Reinders wrote:

...

On 21-01-2023 20:00, Ben Gamari wrote:

...
However, I suspect you do have a point when it comes to unlifted data constructors. I think it would be fine to allow an application of a data constructor of an unlifted type on the top-level:

type UMaybe :: Type -> UnliftedType data UMaybe a = UNothing | UJust a

x :: UMaybe Int x = UJust 42

Perhaps you could open a ticket for this?

This ticket seems related: #17521 Consider top-level unlifted bindings [1].

Or do you think it needs a separate ticket?

Thanks Jaro. That ticket contains the observation "there are other cases where unlifted types are desireable at the top-level (e.g. saturated data constructor applications). In principle it would be fairly straightforward to incorporate a validity check that admits top-level constructor applications which rejecting function applications if we wanted." So I think that ticket subsumes my question, and filing another one would be redundant. Tom

Ben Gamari

22 Jan 22 Jan

6:10 a.m.

New subject: Why can't I bind unlifted values at the top level?

Indeed that is the ticket. There is one wrinkle that I should have mentioned earlier: not even all data constructor applications are admissible at the top level. In particular, constructors with strict fields may require computation to construct. The validity check would need to account for this, either by rejecting such constructors altogether or by having some of syntactic WHNF check. Cheers, - Ben On January 21, 2023 5:06:13 PM EST, Tom Ellis wrote:

...

On Sat, Jan 21, 2023 at 10:52:33PM +0100, Jaro Reinders wrote:

...
On 21-01-2023 20:00, Ben Gamari wrote:

...
However, I suspect you do have a point when it comes to unlifted data constructors. I think it would be fine to allow an application of a data constructor of an unlifted type on the top-level:

type UMaybe :: Type -> UnliftedType data UMaybe a = UNothing | UJust a

x :: UMaybe Int x = UJust 42

Perhaps you could open a ticket for this?

This ticket seems related: #17521 Consider top-level unlifted bindings [1].

Or do you think it needs a separate ticket?

Thanks Jaro. That ticket contains the observation

"there are other cases where unlifted types are desireable at the top-level (e.g. saturated data constructor applications). In principle it would be fairly straightforward to incorporate a validity check that admits top-level constructor applications which rejecting function applications if we wanted."

So I think that ticket subsumes my question, and filing another one would be redundant.

Tom _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

David Feuer

6:12 a.m.

New subject: Why can't I bind unlifted values at the top level?

That's what ML calls the "value restriction", right? On Sun, Jan 22, 2023, 1:11 AM Ben Gamari wrote:

...

Indeed that is the ticket.

There is one wrinkle that I should have mentioned earlier: not even all data constructor applications are admissible at the top level. In particular, constructors with strict fields may require computation to construct. The validity check would need to account for this, either by rejecting such constructors altogether or by having some of syntactic WHNF check.

Cheers,

- Ben

On January 21, 2023 5:06:13 PM EST, Tom Ellis < tom-lists-haskell-cafe-2017@jaguarpaw.co.uk> wrote:

...
On Sat, Jan 21, 2023 at 10:52:33PM +0100, Jaro Reinders wrote:

...
On 21-01-2023 20:00, Ben Gamari wrote:

...
However, I suspect you do have a point when it comes to unlifted data constructors. I think it would be fine to allow an application of a data constructor of an unlifted type on the top-level:

type UMaybe :: Type -> UnliftedType data UMaybe a = UNothing | UJust a

x :: UMaybe Int x = UJust 42

Perhaps you could open a ticket for this?

This ticket seems related: #17521 Consider top-level unlifted bindings [1].

Or do you think it needs a separate ticket?

Thanks Jaro. That ticket contains the observation

"there are other cases where unlifted types are desireable at the top-level (e.g. saturated data constructor applications). In principle it would be fairly straightforward to incorporate a validity check that admits top-level constructor applications which rejecting function applications if we wanted."

So I think that ticket subsumes my question, and filing another one would be redundant.

Tom ------------------------------ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________

Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Tom Ellis

8:55 a.m.

New subject: Why can't I bind unlifted values at the top level?

I think so, and that's also why I said "value" (versus "expression") in my original message. On Sun, Jan 22, 2023 at 01:12:36AM -0500, David Feuer wrote:

...

That's what ML calls the "value restriction", right?

On Sun, Jan 22, 2023, 1:11 AM Ben Gamari wrote:

...
Indeed that is the ticket.

There is one wrinkle that I should have mentioned earlier: not even all data constructor applications are admissible at the top level. In particular, constructors with strict fields may require computation to construct. The validity check would need to account for this, either by rejecting such constructors altogether or by having some of syntactic WHNF check.

On January 21, 2023 5:06:13 PM EST, Tom Ellis wrote:

...
On Sat, Jan 21, 2023 at 10:52:33PM +0100, Jaro Reinders wrote:

...
On 21-01-2023 20:00, Ben Gamari wrote:

...
However, I suspect you do have a point when it comes to unlifted data constructors. I think it would be fine to allow an application of a data constructor of an unlifted type on the top-level:

type UMaybe :: Type -> UnliftedType data UMaybe a = UNothing | UJust a

x :: UMaybe Int x = UJust 42

Perhaps you could open a ticket for this?

This ticket seems related: #17521 Consider top-level unlifted bindings [1].

Or do you think it needs a separate ticket?

Thanks Jaro. That ticket contains the observation

"there are other cases where unlifted types are desireable at the top-level (e.g. saturated data constructor applications). In principle it would be fairly straightforward to incorporate a validity check that admits top-level constructor applications which rejecting function applications if we wanted."

So I think that ticket subsumes my question, and filing another one would be redundant.

Richard Eisenberg

26 Jan 26 Jan

2:07 a.m.

New subject: Why can't I bind unlifted values at the top level?

...

On Jan 22, 2023, at 1:12 AM, David Feuer wrote:

That's what ML calls the "value restriction", right?

No, ML's value restriction is unrelated to this conversation. ML's value restriction says that all polymorphic variables (top-level or otherwise) must syntactically be values -- not, say, function calls. The "value-ness" check might end up similar, but the motivations are distinct. Richard

David Feuer

2:46 a.m.

New subject: Why can't I bind unlifted values at the top level?

I meant the valueness check. I know their motivation has to do with type safety (IIRC, it's to avoid what we know in Haskell as unsafeCoerce-via-unsafePerformIO). On Wed, Jan 25, 2023, 9:07 PM Richard Eisenberg wrote:

...

On Jan 22, 2023, at 1:12 AM, David Feuer wrote:

That's what ML calls the "value restriction", right?

No, ML's value restriction is unrelated to this conversation. ML's value restriction says that all polymorphic variables (top-level or otherwise) must syntactically be values -- not, say, function calls. The "value-ness" check might end up similar, but the motivations are distinct.

Richard

893

Age (days ago)

907

Last active (days ago)

List overview

Download

16 comments

7 participants

participants (7)

Ben Gamari
Bertram Felgenhauer
David Feuer
Jaro Reinders
Oleg Grenrus
Richard Eisenberg
Tom Ellis