Unpacking coercions

[Ryan Scott]

> We could utterly lie and say
>
>               data Coercion a b where
>
>                   Coercion :: Coercion a a
>
>
>
> That would generate the right bits in in the .o file, and we’d totally
ignore the .hi file.  Gruesome but I think it would work.

This was precisely what I had in mind. We already perform this trick for
several things defined in ghc-prim (e.g., the (~) and (~~) classes), so
this would just be another example of that.

> But rather than all this circumlocution, why don’t we just make it
possible to write ~# and ~R# directly.  Even if we dodge the need right
now, it’ll surely come back.

Hah, the reason David is suggesting his idea in the first place is to avoid
having to do this! My understanding is that making it possible to write
(~#) and (~R#) directly would involve quite a number of complications, as
Richard's wiki entry on the subject [1] demonstrates.

That's not to say that I wouldn't like to see that happen some day. But a
mere mortal like myself couldn't possibly implement this, whereas David's
idea is actually within reach.

Ryan S.
-----
[1]
https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Internal#Liftedvs.Unliftedequality

On Wed, Sep 5, 2018 at 10:45 AM, Simon Peyton Jones <simonpj at microsoft.com>
wrote:

> I think the intention is to have that proposal (which proposes a language
> change) be superseded by this idea (which does not change the language).
>
> Oh, I did not know that.   I’ll ignore the proposal for now, in that case.
>
>
>
> All that would take is putting Coercion in TysWiredIn, and moving Coercion
> from Data.Type.Coercion to somewhere in ghc-prim.
>
>
>
> I don’t think it’s quite as simple as that.  Yes, we can wire it into the
> compiler; but we still need a module that defines the info table, curried
> data constructor etc for the type.  And we have no way to do that.
>
>
>
> We could utterly lie and say
>
>               data Coercion a b where
>
>                   Coercion :: Coercion a a
>
>
>
> That would generate the right bits in in the .o file, and we’d totally
> ignore the .hi file.  Gruesome but I think it would work.
>
>
>
>
>
> But rather than all this circumlocution, why don’t we just make it
> possible to write ~# and ~R# directly.  Even if we dodge the need right
> now, it’ll surely come back.
>
>
>
> If that is lexically tiresome, we could I suppose provide builtin-aliases
> for them, as if we had
>
>               type NomEq# = (~#)
>
>              type ReprEq# = (~R#)
>
>
>
> Simon
>
>
>
> *From:* Ryan Scott <ryan.gl.scott at gmail.com>
> *Sent:* 05 September 2018 15:26
> *To:* Simon Peyton Jones <simonpj at microsoft.com>
> *Cc:* ghc-devs at haskell.org
> *Subject:* Re: Unpacking coercions
>
>
>
> > Simple is good.  But what is this dead simple idea?
>
>
>
> I'm referring to David's first e-mail on this thread:
> https://mail.haskell.org/pipermail/ghc-devs/2018-September/016191.html
>
>
>
> All that would take is putting Coercion in TysWiredIn, and moving Coercion
> from Data.Type.Coercion to somewhere in ghc-prim.
>
>
>
> > Maybe this thread belongs with the proposal, unless I’m
> misunderstanding.
>
>
>
> I think the intention is to have that proposal (which proposes a language
> change) be superseded by this idea (which does not change the language).
>
>
>
> Ryan S.
>
>
>
>
>
> On Wed, Sep 5, 2018 at 10:20 AM, Simon Peyton Jones <simonpj at microsoft.com>
> wrote:
>
> Simple is good.  But what is this dead simple idea?
>
>
>
> Perhaps: https://github.com/ghc-proposals/ghc-proposals/pull/116
> <https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F116&data=02%7C01%7Csimonpj%40microsoft.com%7Cab6e886b24b548eab26608d6133b91b5%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636717543898919689&sdata=XKBwJiLM%2FcH5FeRLuodH3SKXQUppYT0QYDojH4fO7Tg%3D&reserved=0>
>
> But that proposal lists several possible alternatives.  Which one did you
> mean?
>
>
>
> And all of them are language changes. Making evidence strict would require
> no language changes to solve the original problem.
>
>
>
> Maybe this thread belongs with the proposal, unless I’m misunderstanding.
>
>
>
> Simon
>
>
>
> *From:* ghc-devs <ghc-devs-bounces at haskell.org> *On Behalf Of *Ryan Scott
> *Sent:* 05 September 2018 15:15
> *To:* ghc-devs at haskell.org
> *Subject:* Re: Unpacking coercions
>
>
>
> These aren't mutually exclusive ideas. While I'm sure there's many ways we
> could solve this problem, David's idea has the distinct advantage of being
> dead simple. I'd rather not block his vision on some other large refactor
> that may never materialize. (And if it _does_ materialize, we could revert
> any wiring-in of Coercible quite easily.)
>
>
>
> Ryan S.
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20180905/63b5b443/attachment.html>