[Haskell-cafe] Question on Coerce

[David Feuer]

Coincidentally, I've been thinking about (a small part of) this issue for a
day or two. I think it would probably be pretty easy to add a language
feature that basically brought what the compiler does up to the Haskell
level. Imagine a sort of *generalized* as-pattern:

f x@@(Right y) = ...

`x` here is not bound to the actual argument; instead, it is bound to
`Right y`. The type of `x` will either be inferred or given explicitly:

f (x :: ...)@@(Right y) = ...

How can this translate to Core? Roughly speaking, it would look like

f _x = case _x of
  Left p -> ...
  Right y ->
    let x = unsafeCoerce _x
    in ...

But `x` would be given the unfolding `Right y`.

For existentials and GADTs, the type checking and Core translation needs
some extras. In particular, the dictionary arguments need to be included to
ensure the coercion is valid. Just make sure they match. The special ~ and
Coercible constraints don't need to be included in that check, but it must
be possible to produce coercions with the appropriate types.

On Wed, Dec 2, 2020, 11:32 AM Brent Walker <brenthwalker at gmail.com> wrote:

> My question was on how to use coerce -- not whether this is worth doing or
> not.  If we were discussing that, then I would say it's not 'just a leaf'
> -- it's ALL the leaves of the tree -- and for a tree of depth n, there are
> 2^n of them so depending on what 'n' is, it could potentially be something
> to worry about.
>
>
>
> On Wed, Dec 2, 2020 at 6:00 PM Henning Thielemann <
> lemming at henning-thielemann.de> wrote:
>
>>
>> On Wed, 2 Dec 2020, Brent Walker wrote:
>>
>> > In the following code, function fmap does not compile because variable
>> > 'y' on line marked <***> has type (Expr a) where an (Expr b) is
>> > expected.  The code can be fixed simply by returning (Val x) on the rhs
>> > of the function but then we are allocating a new object for something
>> we
>> > could potentially reuse since (Val n) has the same runtime
>> > representation in (Expr a) and (Expr b) (it has no dependence on the
>> > type variable).
>>
>> Is it worth the trouble? It is only a leaf of the tree.
>
> _______________________________________________
> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20201202/0e1463db/attachment-0001.html>