<div dir="ltr">A similar unlifted constraint style newtype that would be very valuable to me would be to be able to talk about unlifted implicit parameters.<div><br></div><div><font face="monospace">type GivenFoo = (?foo :: Int#)</font></div><div><br>(hopefully properly inhabiting <font face="monospace">TYPE 'IntRep</font>)<br><br></div><div>This would go a long way towards removing the last bit of overhead when using implicit parameters to automatically dispatch <i>just</i> 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.</div><div><br></div><div>-Edward</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Feb 4, 2021 at 4:52 PM Igor Popov <<a href="mailto:mniip@typeable.io">mniip@typeable.io</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">Hello list!<br><br>Recently I've had this idea of letting Haskell source handle unboxed<br>equalities (~#) by the means of an unboxed newtype. The idea is pretty<br>straightforward: in Core Constraint is Type and (=>) is (->), so a<br>datatype like<br><br> data Eq a b = (a ~ b) => Refl<br><br>could become a newtype because it only has a single "field": (a ~ b).<br>Furthermore now that we have unlifted newtypes, we could write it as a<br>newtype over (~#), of kind TYPE (TupleRep []).<br><br>Defining such a datatype is of course impossible in source Haskell, but<br>what I came up with is declaring a plugin that magically injects the<br>necessary bits into the interface file.<br><br>Sounds like it should be straightforward: define a newtype (:~:#) with a<br>constructor whose representation type is:<br><br> forall k (a :: k) (b :: k). (a ~# b) -> a :~:# b<br><br>The worker constructor is implemented by a coercion (can even be<br>eta-reduced):<br><br> axiom N::~:# :: forall {k}. (:~:#) = (~#)<br> Refl# = \ (@ k) (@ (a :: k)) (@ (b :: k)) (v :: a ~# b) -><br> v `cast` (Sym (N::~:#) <k>_N) <a>_N <b>_N<br><br>And the wrapper constructor has a Haskell-ish type:<br><br> $WRefl# :: forall k (b :: k). b :~:# b<br> $WRefl# = \ (@ k) (@ (b :: k)) -><br> Refl# @ k @ a @ b @~ <b>_N<br><br>Caveat: we don't actually get to specify the unwrappings ourselves, and<br>we have to rely on mkDataConRep generating the right wrapper based on<br>the types and the EqSpec (because this will have to be done every time<br>the constructor is loaded from an iface). In this case the machinery is<br>not convinced that a wrapper is required, unless we ensure that<br>dataConUserTyVarsArePermuted by fiddling around with ordering of<br>variables. This is a minor issue (which I think I can work around) but<br>could be addressed on the GHC side.<br><br>I've indeed implemented a plugin that declares these, but we run into a<br>more major issue: the simplifier is not ready for such code! Consider a<br>simple utility function:<br><br> sym# :: a :~:# b -> b :~:# a<br> sym# Refl# = Refl# <br><br>This gets compiled into:<br><br> sym# = \ (@ k) (@ (a :: k)) (@ (b :: k)) (ds :: a :~:# b) -><br> case ds `cast` N::~:# <k>_N <a>_N <b>_N of<br> co -> $WRefl# @ k @ b `cast` ((:~:#) <k>_N <b> (Sym co))_R<br><br>which seems valid but then the simplifier incorrectly inlines the<br>unfolding of $WRefl# and arrives at code that is not even well-scoped<br>(-dcore-lint catches this):<br><br> sym# = \ (@ k) (@ (a :: k)) (@ (b :: k)) (ds :: a :~:# b) -><br> case ds `cast` N::~:# <k>_N <a>_N <b>_N of<br> co -> v `cast` (Sym (N::~: <k>_N)) <b>_N <b>_N<br> ; ((:~:#) <k>_N <b>_N (Sym co))_R<br><br>Actually the problem manifests itself even earlier: when creating an<br>unfolding for the wrapper constructor with mkCompulsoryUnfolding we run<br>the unfolding term through simpleOptExpr once before memorizing the<br>unfolding, and this produces an unfolding for $WRefl# that is broken<br>(ill-scoped) in a similar fashion:<br><br> $WRefl = \ (@ k) (@ (b :: k)) -><br> v `cast` Sym (N::~:# <k>_N) <b>_N <b>_N<br><br>And we can verify that the issue is localized here: applying<br>simpleOptExpr to:<br><br> (\ (v :: a ~# a) -> v `cast` <a ~# a>_R)<br> @~ <a>_N<br><br>results in:<br><br> v<br><br>The former term is closed and the latter is not.<br><br>There is an invariant on mkPrimEqPred (though oddly not on<br>mkReprPrimEqPred) that says that the related types must not be<br>coercions (we're kind of violating this here).<br><br>I have several questions here:<br>- Is there a good reason for the restriction that equalities should not<br> contain other equalities?<br>- Should this use case be supported? Coercions are almost first class<br> citizens in Core (are they?), makes sense to let source Haskell have a<br> bit of that?<br>- Does it make sense to include this and a few similar types (unboxed<br> Coercion and Dict) as a wired in type packaged with GHC in some form?<br><br>-- mniip<br></div>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div>