[Haskell-cafe] Unboxed, zero-width :~:/Refl?
Oleg Grenrus
oleg.grenrus at iki.fi
Thu Jan 12 15:51:58 UTC 2023
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.
More information about the Haskell-Cafe
mailing list