Newtype over (~#)

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
7 messages Options
Reply | Threaded
Open this post in threaded view
|

Newtype over (~#)

Igor Popov
Hello list!

Recently I've had this idea of letting Haskell source handle unboxed
equalities (~#) by the means of an unboxed newtype. The idea is pretty
straightforward: in Core Constraint is Type and (=>) is (->), so a
datatype like

data Eq a b = (a ~ b) => Refl

could become a newtype because it only has a single "field": (a ~ b).
Furthermore now that we have unlifted newtypes, we could write it as a
newtype over (~#), of kind TYPE (TupleRep []).

Defining such a datatype is of course impossible in source Haskell, but
what I came up with is declaring a plugin that magically injects the
necessary bits into the interface file.

Sounds like it should be straightforward: define a newtype (:~:#) with a
constructor whose representation type is:

forall k (a :: k) (b :: k). (a ~# b) -> a :~:# b

The worker constructor is implemented by a coercion (can even be
eta-reduced):

axiom N::~:# :: forall {k}. (:~:#) = (~#)
Refl# = \ (@ k) (@ (a :: k)) (@ (b :: k)) (v :: a ~# b) ->
   v `cast` (Sym (N::~:#) <k>_N) <a>_N <b>_N

And the wrapper constructor has a Haskell-ish type:

$WRefl# :: forall k (b :: k). b :~:# b
$WRefl# = \ (@ k) (@ (b :: k)) ->
   Refl# @ k @ a @ b @~ <b>_N

Caveat: we don't actually get to specify the unwrappings ourselves, and
we have to rely on mkDataConRep generating the right wrapper based on
the types and the EqSpec (because this will have to be done every time
the constructor is loaded from an iface). In this case the machinery is
not convinced that a wrapper is required, unless we ensure that
dataConUserTyVarsArePermuted by fiddling around with ordering of
variables. This is a minor issue (which I think I can work around) but
could be addressed on the GHC side.

I've indeed implemented a plugin that declares these, but we run into a
more major issue: the simplifier is not ready for such code! Consider a
simple utility function:

sym# :: a :~:# b -> b :~:# a
sym# Refl# = Refl#

This gets compiled into:

sym# = \ (@ k) (@ (a :: k)) (@ (b :: k)) (ds :: a :~:# b) ->
   case ds `cast` N::~:# <k>_N <a>_N <b>_N of
       co -> $WRefl# @ k @ b `cast` ((:~:#) <k>_N <b> (Sym co))_R

which seems valid but then the simplifier incorrectly inlines the
unfolding of $WRefl# and arrives at code that is not even well-scoped
(-dcore-lint catches this):

sym# = \ (@ k) (@ (a :: k)) (@ (b :: k)) (ds :: a :~:# b) ->
   case ds `cast` N::~:# <k>_N <a>_N <b>_N of
       co -> v `cast` (Sym (N::~: <k>_N)) <b>_N <b>_N
           ; ((:~:#) <k>_N <b>_N (Sym co))_R

Actually the problem manifests itself even earlier: when creating an
unfolding for the wrapper constructor with mkCompulsoryUnfolding we run
the unfolding term through simpleOptExpr once before memorizing the
unfolding, and this produces an unfolding for $WRefl# that is broken
(ill-scoped) in a similar fashion:

$WRefl = \ (@ k) (@ (b :: k)) ->
   v `cast` Sym (N::~:# <k>_N) <b>_N <b>_N

And we can verify that the issue is localized here: applying
simpleOptExpr to:

(\ (v :: a ~# a) -> v `cast` <a ~# a>_R)
   @~ <a>_N

results in:

v

The former term is closed and the latter is not.

There is an invariant on mkPrimEqPred (though oddly not on
mkReprPrimEqPred) that says that the related types must not be
coercions (we're kind of violating this here).

I have several questions here:
- Is there a good reason for the restriction that equalities should not
  contain other equalities?
- Should this use case be supported? Coercions are almost first class
  citizens in Core (are they?), makes sense to let source Haskell have a
  bit of that?
- Does it make sense to include this and a few similar types (unboxed
  Coercion and Dict) as a wired in type packaged with GHC in some form?

-- mniip

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Newtype over (~#)

Edward Kmett-2
A similar unlifted constraint style newtype that would be very valuable to me would be to be able to talk about unlifted implicit parameters.

type GivenFoo = (?foo :: Int#)

(hopefully properly inhabiting TYPE 'IntRep)

This would go a long way towards removing the last bit of overhead when using implicit parameters to automatically dispatch just the portions of the environment/state/etc. that you need to handle effect systems without incurring unnecessary boxes. Right now when I work with a custom Monad I can of course unbox the argument to by reader or state, but when I move it into an implicit parameter to get it automatically thinned down to just what portions of the environment I actually need, I lose that level of expressiveness.

-Edward

On Thu, Feb 4, 2021 at 4:52 PM Igor Popov <[hidden email]> wrote:
Hello list!

Recently I've had this idea of letting Haskell source handle unboxed
equalities (~#) by the means of an unboxed newtype. The idea is pretty
straightforward: in Core Constraint is Type and (=>) is (->), so a
datatype like

data Eq a b = (a ~ b) => Refl

could become a newtype because it only has a single "field": (a ~ b).
Furthermore now that we have unlifted newtypes, we could write it as a
newtype over (~#), of kind TYPE (TupleRep []).

Defining such a datatype is of course impossible in source Haskell, but
what I came up with is declaring a plugin that magically injects the
necessary bits into the interface file.

Sounds like it should be straightforward: define a newtype (:~:#) with a
constructor whose representation type is:

forall k (a :: k) (b :: k). (a ~# b) -> a :~:# b

The worker constructor is implemented by a coercion (can even be
eta-reduced):

axiom N::~:# :: forall {k}. (:~:#) = (~#)
Refl# = \ (@ k) (@ (a :: k)) (@ (b :: k)) (v :: a ~# b) ->
   v `cast` (Sym (N::~:#) <k>_N) <a>_N <b>_N

And the wrapper constructor has a Haskell-ish type:

$WRefl# :: forall k (b :: k). b :~:# b
$WRefl# = \ (@ k) (@ (b :: k)) ->
   Refl# @ k @ a @ b @~ <b>_N

Caveat: we don't actually get to specify the unwrappings ourselves, and
we have to rely on mkDataConRep generating the right wrapper based on
the types and the EqSpec (because this will have to be done every time
the constructor is loaded from an iface). In this case the machinery is
not convinced that a wrapper is required, unless we ensure that
dataConUserTyVarsArePermuted by fiddling around with ordering of
variables. This is a minor issue (which I think I can work around) but
could be addressed on the GHC side.

I've indeed implemented a plugin that declares these, but we run into a
more major issue: the simplifier is not ready for such code! Consider a
simple utility function:

sym# :: a :~:# b -> b :~:# a
sym# Refl# = Refl#

This gets compiled into:

sym# = \ (@ k) (@ (a :: k)) (@ (b :: k)) (ds :: a :~:# b) ->
   case ds `cast` N::~:# <k>_N <a>_N <b>_N of
       co -> $WRefl# @ k @ b `cast` ((:~:#) <k>_N <b> (Sym co))_R

which seems valid but then the simplifier incorrectly inlines the
unfolding of $WRefl# and arrives at code that is not even well-scoped
(-dcore-lint catches this):

sym# = \ (@ k) (@ (a :: k)) (@ (b :: k)) (ds :: a :~:# b) ->
   case ds `cast` N::~:# <k>_N <a>_N <b>_N of
       co -> v `cast` (Sym (N::~: <k>_N)) <b>_N <b>_N
           ; ((:~:#) <k>_N <b>_N (Sym co))_R

Actually the problem manifests itself even earlier: when creating an
unfolding for the wrapper constructor with mkCompulsoryUnfolding we run
the unfolding term through simpleOptExpr once before memorizing the
unfolding, and this produces an unfolding for $WRefl# that is broken
(ill-scoped) in a similar fashion:

$WRefl = \ (@ k) (@ (b :: k)) ->
   v `cast` Sym (N::~:# <k>_N) <b>_N <b>_N

And we can verify that the issue is localized here: applying
simpleOptExpr to:

(\ (v :: a ~# a) -> v `cast` <a ~# a>_R)
   @~ <a>_N

results in:

v

The former term is closed and the latter is not.

There is an invariant on mkPrimEqPred (though oddly not on
mkReprPrimEqPred) that says that the related types must not be
coercions (we're kind of violating this here).

I have several questions here:
- Is there a good reason for the restriction that equalities should not
  contain other equalities?
- Should this use case be supported? Coercions are almost first class
  citizens in Core (are they?), makes sense to let source Haskell have a
  bit of that?
- Does it make sense to include this and a few similar types (unboxed
  Coercion and Dict) as a wired in type packaged with GHC in some form?

-- mniip
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Newtype over (~#)

Richard Eisenberg-5
In reply to this post by Igor Popov
GHC cheats in this area. The problem is that (a ~# b) is a type, because that is terribly, terribly convenient. But it really shouldn't be.

The problem is that coercion variables are different from regular variables. So, if we say (v :: a ~# b), we must always be careful: is v a coercion variable or not? If it isn't, then v is useless. You cannot, for instance, use v in a cast. In a number of places, GHC must produce a variable binder of a certain type. It will sometimes examine that type; if the type is an equality type, then the binder will be a coercion variable; otherwise, it will be a normal Id. This is wrong, but again, very convenient. (Wrong because we should always know in advance whether we want a coercion variable or an Id.)

I think the problems you're running into are all around this confusion. For example,

(\ (v :: a ~# a) -> v `cast` <a ~# a>_R)
   @~ <a>_N

is ill-formed, whether v is an Id or a CoVar. If it's an Id, then this is wrong because you have an Id with a coercion type. (The theory of the core language does not prevent such things, but I'm not surprised that GHC would fall over if you tried it.) If v is a CoVar, then its use as the left-hand side of `cast` is wrong.


All that said, I think your original idea is a fine one: a newtype wrapper around ~#. It's possible there is just some Id/CoVar confusion in your implementation, and that's what's causing the trouble. I don't see a correct implementation as impossible.

Is your implementation available somewhere?

I hope this helps!
Richard

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Newtype over (~#)

Igor Popov
> GHC cheats in this area. The problem is that (a ~# b) is a type, because that is terribly, terribly convenient. But it really shouldn't be.
>
> The problem is that coercion variables are different from regular variables. So, if we say (v :: a ~# b), we must always be careful: is v a coercion variable or not? If it isn't, then v is useless. You cannot, for instance, use v in a cast.

I don't really see a problem here. The fact that only a "coercion
variable" can be used in a cast should be enforced by the typing rule
for cast. That doesn't require having a distinct "syntactic category"
of coercion variables, unless I'm missing something.

-- mniip
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Newtype over (~#)

Richard Eisenberg-5
We do need a separate category, though: otherwise, we could cast by `f x`, where `f` is a non-terminating functions. We erase casts, so the function would never get called. Maybe if we required that casts are always by variables (essentially, A-normalize casts) we could avoid this? But then would we require A-normalization to build coercions from pieces (as opposed to calling functions)? It's unclear.

I think the first versions of this idea didn't require the separate syntactic category, but all work for the past decade has. I think there are other ways, but the way GHC handles this now is somewhat poor, because of #17291.

Richard

> On Feb 5, 2021, at 7:56 PM, Igor Popov <[hidden email]> wrote:
>
>> GHC cheats in this area. The problem is that (a ~# b) is a type, because that is terribly, terribly convenient. But it really shouldn't be.
>>
>> The problem is that coercion variables are different from regular variables. So, if we say (v :: a ~# b), we must always be careful: is v a coercion variable or not? If it isn't, then v is useless. You cannot, for instance, use v in a cast.
>
> I don't really see a problem here. The fact that only a "coercion
> variable" can be used in a cast should be enforced by the typing rule
> for cast. That doesn't require having a distinct "syntactic category"
> of coercion variables, unless I'm missing something.
>
> -- mniip

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Newtype over (~#)

Igor Popov
That's a really interesting quirk. That kind of explains why an
argument to a cast has to be a CoVar, we want all casts to be guarded
by a case-of. But do we still need the restriction that an Id cannot
have a coercion type?

Either case it seems like we need to be extremely careful with how the
wrapper and the matcher works for such a constructor. I was hoping a
sledgehammer approach would work where we kind of just force (a ~# b)
as a field into a newtype, and the existing machinery magically works
with it.

The construction is then chock full of questions:

    axiom N::~:# :: forall k. (:~:#) @k ~R (~#) @k

Is this valid? mkPrimEqPred says it doesn't like equalities on either
side (I'm assuming this applies to eta-contracted equalities as well).
mkReprPrimEqPred doesn't. Who to believe and what are the pitfalls?

    Refl# :: forall k (a b :: k). a ~# b -> a :~:# b
    Refl# = \@k @a @b v -> v `cast` Sym (N::~:# k) <a> <b>

Is this valid? You say that v has to be bound as a CoVar (current
newtype machinery will not do this). Can a CoVar appear in the LHS of
a cast? The result is definitely a type and can be bound to an Id, I
guess.

    $WRefl# :: forall k (a :: k). a :~:# a
    $WRefl# = \@k @a -> Refl# @k @a @a <a>

Relatively tame, but however once we inline the definition of Refl#
(simpleOptExpr will do this when registering an unfolding), we get:

    <a> `cast` Sym (N::~:# k) <a> <a>

Is this valid?

The matcher/boxer (is that the word) has to be carefully constructed
as well: we have to desugar

    case x of Refl# -> e

where (x :: a :~:# b) into:

    case x `cast` N::~:# k <a> <b> of
        co -> e

where co is now a CoVar. Can a cast's result type be a coercion? Can a
coercion be the scrutinee of a case-of? (Judging by the code we
generate for eq_sel the answer is yes).

-- mniip


On Sun, Feb 7, 2021 at 7:41 PM Richard Eisenberg <[hidden email]> wrote:

>
> We do need a separate category, though: otherwise, we could cast by `f x`, where `f` is a non-terminating functions. We erase casts, so the function would never get called. Maybe if we required that casts are always by variables (essentially, A-normalize casts) we could avoid this? But then would we require A-normalization to build coercions from pieces (as opposed to calling functions)? It's unclear.
>
> I think the first versions of this idea didn't require the separate syntactic category, but all work for the past decade has. I think there are other ways, but the way GHC handles this now is somewhat poor, because of #17291.
>
> Richard
>
> > On Feb 5, 2021, at 7:56 PM, Igor Popov <[hidden email]> wrote:
> >
> >> GHC cheats in this area. The problem is that (a ~# b) is a type, because that is terribly, terribly convenient. But it really shouldn't be.
> >>
> >> The problem is that coercion variables are different from regular variables. So, if we say (v :: a ~# b), we must always be careful: is v a coercion variable or not? If it isn't, then v is useless. You cannot, for instance, use v in a cast.
> >
> > I don't really see a problem here. The fact that only a "coercion
> > variable" can be used in a cast should be enforced by the typing rule
> > for cast. That doesn't require having a distinct "syntactic category"
> > of coercion variables, unless I'm missing something.
> >
> > -- mniip
>
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Newtype over (~#)

Richard Eisenberg-5


> On Feb 10, 2021, at 5:43 AM, Igor Popov <[hidden email]> wrote:
>
> That's a really interesting quirk. That kind of explains why an
> argument to a cast has to be a CoVar, we want all casts to be guarded
> by a case-of. But do we still need the restriction that an Id cannot
> have a coercion type?

No, we wouldn't need the restriction if GHC were implemented correctly -- that is, without the mkLocalIdOrCoVar abomination that looks at the type of a binder to determine whether it's a CoVar.

>
> Either case it seems like we need to be extremely careful with how the
> wrapper and the matcher works for such a constructor. I was hoping a
> sledgehammer approach would work where we kind of just force (a ~# b)
> as a field into a newtype, and the existing machinery magically works
> with it.
>
> The construction is then chock full of questions:
>
>    axiom N::~:# :: forall k. (:~:#) @k ~R (~#) @k
>
> Is this valid? mkPrimEqPred says it doesn't like equalities on either
> side (I'm assuming this applies to eta-contracted equalities as well).

I don't see any equalities on either side here. Instead, this is a relationship between equality *types*. That should be just fine; GHC even produces such things already from time to time. I do think you'll need two `@k`s on the right, though. The rule you're worried about forbids constructions like (cv1 ~R cv2), where cv1 and cv2 have been injected into types via CoercionTy.

> mkReprPrimEqPred doesn't. Who to believe and what are the pitfalls?

mkReprPrimEqPred has the same properties here; the comments should be better.

>
>    Refl# :: forall k (a b :: k). a ~# b -> a :~:# b
>    Refl# = \@k @a @b v -> v `cast` Sym (N::~:# k) <a> <b>
>
> Is this valid? You say that v has to be bound as a CoVar (current
> newtype machinery will not do this). Can a CoVar appear in the LHS of
> a cast?

No, it can't. This may be a real blocker. I hadn't thought about this part of the problem.
>
>
>    <a> `cast` Sym (N::~:# k) <a> <a>
>
> Is this valid?

No, for the same reasons.

This is unfortunate, as I thought this was a good idea. Yet I'm not hopeful that there's an easy way out of this particular trap.

Richard
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs