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 |
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:
_______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
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. This is all https://gitlab.haskell.org/ghc/ghc/-/issues/17291. 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 |
> 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 |
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 |
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 |
> 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 |
Free forum by Nabble | Edit this page |