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 <mn...@typeable.io> 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 > ghc-devs@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs