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

[Tom Ellis]

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.