Newtype over (~#)

[Edward Kmett]

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 <mniip at 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20210204/3b8d0a6f/attachment.html>