Re: Newtype over (~#)
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 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::~:#) _N) _N _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 @~ _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::~:# _N _N _N of
>co -> $WRefl# @ k @ b `cast` ((:~:#) _N (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::~:# _N _N _N of
>co -> v `cast` (Sym (N::~: _N)) _N _N
>; ((:~:#) _N _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::~:# _N) _N _N
>
> And we can verify that the issue is localized here: applying
> simpleOptExpr to:
>
> (\ (v :: a ~# a) -> v `cast` _R)
>@~ _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
Newtype over (~#)
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::~:#) _N) _N _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 @~ _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::~:# _N _N _N of
co -> $WRefl# @ k @ b `cast` ((:~:#) _N (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::~:# _N _N _N of
co -> v `cast` (Sym (N::~: _N)) _N _N
; ((:~:#) _N _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::~:# _N) _N _N
And we can verify that the issue is localized here: applying
simpleOptExpr to:
(\ (v :: a ~# a) -> v `cast` _R)
@~ _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
Re: Plan for GHC 9.2
Hi, Am Donnerstag, den 04.02.2021, 13:56 -0500 schrieb Ben Gamari: > If you see something that you would like to see in 9.2.1 please do > holler. it’s hopefully not big deal technically, but support for GHC2021 would be desirable. There is a MR https://gitlab.haskell.org/ghc/ghc/-/merge_requests/4853 that “just” needs chaising test suite failures when rebasing on latest master (and I’d be grateful if someone more fluent with today’s GHC development than me would take the MR over at this point) Cheers, Joachim -- Joachim Breitner m...@joachim-breitner.de http://www.joachim-breitner.de/ signature.asc Description: This is a digitally signed message part ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Plan for GHC 9.2
Hi Ben, Since part of the changes of https://gitlab.haskell.org/ghc/ghc/-/issues/14422 are already merged into master (e.g. we ignore the "type signature" part of a COMPLETE sig now, because there is nothing to disambiguate), it would be good if we merged the solution outlined in https://gitlab.haskell.org/ghc/ghc/-/issues/14422#note_321645, as that would allow users to switch to a new, better mechanism instead of discovering that COMPLETE signatures seemingly have been ripped of a feature. The problem with that is that it needs a GHC proposal, I think, and that's not written yet. Also I hope to merge some efforts in the CPR area before the fork. But that's quite optional. Cheers, Sebastian Am Do., 4. Feb. 2021 um 19:56 Uhr schrieb Ben Gamari : > > tl;dr. Provisional release schedule for 9.2 enclosed. Please discuss, >especially if you have something you would like merged for 9.2.1. > > Hello all, > > With GHC 9.0.1 at long-last out the door, it is time that we start > turning attention to GHC 9.2. I would like to avoid making the mistake > made in the 9.0 series in starting the fork in a state that required a > significant amount of backporting to be releaseable. Consequently, I > want to make sure that we have a fork schedule that is realistic given > the things that need to be merged for 9.2. These include: > > * Update haddock submodule in `master` (Ben) > * Bumping bytestring to 0.11 (#19091, Ben) > * Finishing the rework of sized integer primops (#19026, John Ericson) > * Merge of ghc-exactprint into GHC? (Alan Zimmerman, Henry) > * Merge BoxedRep (#17526, Ben) > * ARM NCG backend and further stabilize Apple ARM support? (Moritz) > * Some form of coercion zapping (Ben, Simon, Richard) > * Tag inference analysis and tag check elision (Andreas) > > If you see something that you would like to see in 9.2.1 please do > holler. Otherwise, if you see your name in this list it would be great > if you could let me know when you think your project may be in a > mergeable state. > > Ideally we would strive for a schedule like the following: > > 4 February 2021: We are here >~4 weeks pass > 3 March 2021: Release branch forked >1 week passes > 10 March 2021: Alpha 1 released >3 weeks pass > 31 March 2021: Alpha 2 released >2 weeks pass > 14 April 2021: Alpha 3 released >2 weeks pass > 28 April 2021: Alpha 4 released >1 week passes > 5 May 2021:Beta 1 released >1 week passes > 12 May 2021: Release candidate 1 released >2 weeks pass > 26 May 2021: Final release > > This provides ample time for stabilization while avoiding deviation from > the usual May release timeframe. However, this would require that we > move aggressively to start getting the tree into shape since the fork > would be less than four weeks away. I would appreciate contributors' > thoughts on the viability of this timeline. > > Cheers, > > - Ben > ___ > 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
Plan for GHC 9.2
tl;dr. Provisional release schedule for 9.2 enclosed. Please discuss, especially if you have something you would like merged for 9.2.1. Hello all, With GHC 9.0.1 at long-last out the door, it is time that we start turning attention to GHC 9.2. I would like to avoid making the mistake made in the 9.0 series in starting the fork in a state that required a significant amount of backporting to be releaseable. Consequently, I want to make sure that we have a fork schedule that is realistic given the things that need to be merged for 9.2. These include: * Update haddock submodule in `master` (Ben) * Bumping bytestring to 0.11 (#19091, Ben) * Finishing the rework of sized integer primops (#19026, John Ericson) * Merge of ghc-exactprint into GHC? (Alan Zimmerman, Henry) * Merge BoxedRep (#17526, Ben) * ARM NCG backend and further stabilize Apple ARM support? (Moritz) * Some form of coercion zapping (Ben, Simon, Richard) * Tag inference analysis and tag check elision (Andreas) If you see something that you would like to see in 9.2.1 please do holler. Otherwise, if you see your name in this list it would be great if you could let me know when you think your project may be in a mergeable state. Ideally we would strive for a schedule like the following: 4 February 2021: We are here ~4 weeks pass 3 March 2021: Release branch forked 1 week passes 10 March 2021: Alpha 1 released 3 weeks pass 31 March 2021: Alpha 2 released 2 weeks pass 14 April 2021: Alpha 3 released 2 weeks pass 28 April 2021: Alpha 4 released 1 week passes 5 May 2021:Beta 1 released 1 week passes 12 May 2021: Release candidate 1 released 2 weeks pass 26 May 2021: Final release This provides ample time for stabilization while avoiding deviation from the usual May release timeframe. However, this would require that we move aggressively to start getting the tree into shape since the fork would be less than four weeks away. I would appreciate contributors' thoughts on the viability of this timeline. Cheers, - Ben signature.asc Description: PGP signature ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
[ANNOUNCE] GHC 9.0.1 released
The GHC team is very pleased to announce the availability of GHC 9.0.1. Source and binary distributions are available at the usual place: https://downloads.haskell.org/ghc/9.0.1/ In addition to numerous bug fixes, GHC 9.0.1 will bring a number of new features: * A first cut of the new LinearTypes language extension [2], allowing use of linear function syntax and linear record fields. * A new bignum library, ghc-bignum, improving portability and allowing GHC to be more easily used with integer libraries other than GMP. * Improvements in code generation, resulting in considerable runtime performance improvements in some programs. * Improvements in pattern-match checking, allowing more precise detection of redundant cases and reduced compilation time. * Implementation of the "simplified subsumption" proposal [3] simplifying the type system and paving the way for QuickLook impredicativity in GHC 9.2. * Implementation of the QualifiedDo extension [4], allowing more convenient overloading of `do` syntax. * An experimental new IO manager implementation for Windows platforms, both improving performance and fixing many of the quirks with the old manager built on POSIX-emulation. * Improvements in compilation time. And many more. See the release notes [5] for a full accounting of the changes in this release. As always, feel free to report any issues you encounter via gitlab.haskell.org. Cheers, - Ben [1]: https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.0#ghc-prim-07 [2]: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0111-linear-types.rst [3]: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0287-simplify-subsumption.rst [4]: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0216-qualified-do.rst [5]: https://downloads.haskell.org/ghc/9.0.1/docs/html/users_guide/9.0.1-notes.html signature.asc Description: PGP signature ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
initIface* usage in plugins
Hi, I'm trying to use initIfaceLoad and initIfaceLcl to lookup core `Name`s within a plugin. My understanding is that functions such as `lookupIfaceTop` are used for this, but I'm running into an issue that I suspect is caused by some `Name`s being inappropriate for this function, so they fail with the error `Iface id out of scope: ...`. Is there a robust way to select which `Name` lookup function to use based on a core binding/expression? Thanks, Josh ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
