[Haskell-cafe] Unboxed, zero-width :~:/Refl?

12 Jan 2023

      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.