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
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` _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