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

[Oleg Grenrus]

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.