Fwd: [Ann] Haskell Ecosystem Proposals
I am forwarding this mail to ghc-devs and cabal-devs in case anyone missed the original which went to haskell-cafe only. Alan -- Forwarded message -- From: Alan & Kim Zimmerman Date: Sun, Dec 11, 2016 at 9:39 PM Subject: [Ann] Haskell Ecosystem Proposals To: haskell Earlier this year Simon Peyton Jones wrote about respect [1], and said "It's worth separating two things 1. Publicly debating an issue where judgements differ 2. Using offensive or adversarial language in that debate" There is now a repository[2] for us as a community to have the first kind of discussion about issues that affect the community as a whole. The intention is that this becomes a neutral place where discussion can take place about coordinating the various services offered to the haskell community. This is partly to expose the thinking and constraints on a particular approach, so proponents of other approaches can have a better understanding of how things can evolve. The idea is that through an honest understanding of the various parts we can achieve consensus on how to improve things. If this all sounds a bit handwavy, the first concrete example of this approach is a pull request [3] discussing the management of implicit or speculative version bounds between cabal-install/hackage and stack/stackage. This has reached a point where there is a clearer understanding of the actual problem, and a viable solution must be agreed. The structure of the repository is shamelessly copied from the one for GHC proposals, so the actual process description is way off. It should probably just state that we discuss until consensus is reached if possible, but that we are always open for further discussion. It is up to all of us to make this work. Regards Alan [1] https://mail.haskell.org/pipermail/haskell/2016-September/024995.html [2] https://github.com/haskell/ecosystem-proposals [3] https://github.com/haskell/ecosystem-proposals/pull/1 ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Join points!
Everyone: please take a look. Luke Very good. · I think it’s fine to work from your repo; no need to use the main repo. · One big patch is fine. The exception is late lambda-lifting which would best be done separately. · Can you identify any bits that you are less happy with? · Before long, can you put up nofib figures? Make a Trac ticket for this too. On Phab, you can have dialogue about “what does this line of code mean”. On Trac you can have longer-term strategic concerns. There isn’t a clear boundary. But Trac persists and Phab really doesn’t. We should talk about your question about floating. Simon From: Luke Maurer [mailto:maur...@cs.uoregon.edu] Sent: 15 December 2016 10:52 To: Simon Peyton Jones Subject: Phab diff up Okay, after some further cleanups, I've put up a Phabricator diff: https://phabricator.haskell.org/D2853 (Has some lint failures, but I figure better to put it up sooner … will fix after I get some sleep) Was going to push to a branch in the official GHC repo, too, but I don't think I have push access? Anyway, should I try and split it up into pieces? Hard to see how that would work, given how many interconnected pieces there are. I suppose if you apply the changes to Core Lint last, it might work … Also, the patch includes the stuff from the late lambda-lifting branch, which is perhaps more than we want to push at once! Certainly that much is splittable, if desired. I'm also just not as happy with that code. - Luke ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Explicit inequality evidence
Hi Oleg,
I'm afraid to say that there is no one current type safety proof. Instead,
there are lots of bits and pieces:
- A system with roles (but no TypeInType or kind polymorphism) is proved in
"Safe Zero-cost Coercions for Haskell" (JFP '16) [1].
- A system with TypeInType but no roles is proved in "System FC with Explicit
Kind Equality (extended version)" (ICFP '13) [2]. This type safety proof is
broken (see [3], section 5.10.5.2), but we have no counterexample to safety.
- Closed type families are proved safe in "Closed Type Families with
Overlapping Equations" (POPL '14) [4]. This system has no roles nor kind
polymorphism. It also assumed that type family reductions terminate, explicitly
leaving the challenge of proving safety with non-terminating type families as
an open problem (see Section 6 of that paper). There may be a solution in work
that has since been completed ("Non-ω-overlapping TRSs are UN" (LIPIcs '16)
[5]), but I'm not aware of work that has adapted that solution to work with
Haskell.
- My thesis (Univ. of Pennsylvania '16) [3] has a proof of a version of Haskell
with dependent types. Closed type families have been converted into type-level
lambdas; the full proof does not consider the possibility of non-linear
patterns in type families. A start toward such an approach is described
(Section 5.13.2) but not fleshed out. Roles are not included.
- A draft paper, never published, ("An overabundance of equality: Implementing
kind equalities into Haskell" (2015) [6]) considers the possibility of
combining roles with TypeInType. The proof is somewhat sparse, and it has not
gotten the level of scrutiny in the other proofs. Furthermore, the way roles
and TypeInType are integrated in GHC is different than what appears in this
draft.
- Forthcoming work, by Stephanie Weirich, Pedro Amorim, Antoine Voizard, and
myself, contains a mechanized proof of safety of a dependently typed
Haskell-like system, but with no roles, closed type families, or even
datatypes. I do not believe there is a public link to this work; we expect to
submit to ICFP.
- There is a formally written, but unproved, description of what is implemented
in GHC [7]. It is useful for understanding the GHC source code in relation to
other published work. There is no proof whatsoever.
This is a sorry state of affairs, I know. It remains my hope that we will have
a formal, mechanized proof of this all Some Day, and progress is indeed slowly
marching toward that goal.
Richard
[1]: http://cs.brynmawr.edu/~rae/papers/2016/coercible-jfp/coercible-jfp.pdf
[2]: http://cs.brynmawr.edu/~rae/papers/2013/fckinds/fckinds-extended.pdf
[3]: http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf
[4]: http://cs.brynmawr.edu/~rae/papers/2014/axioms/axioms-extended.pdf
[5]: http://kar.kent.ac.uk/55349/1/proc-kahrs.pdf
[6]: http://cs.brynmawr.edu/~rae/papers/2015/equalities/equalities.pdf
[7]: https://github.com/ghc/ghc/blob/master/docs/core-spec/core-spec.pdf
> On Dec 15, 2016, at 1:30 AM, Oleg Grenrus wrote:
>
> Out of curiosity: where's the current type safety proof, and is it
> mechanized?
>
> Oleg
>
>
> On 13.12.2016 17:01, Richard Eisenberg wrote:
>> I've thought about inequality on and off for years now, but it's a hard nut
>> to crack. If we want this evidence to affect closed type family reduction,
>> then we would need evidence of inequality in Core, and a brand-spanking-new
>> type safety proof. I don't wish to discourage this inquiry, but I also don't
>> think this battle will be won easily.
>>
>> Richard
>>
>>> On Dec 13, 2016, at 1:02 AM, David Feuer wrote:
>>>
>>> On Tue, Dec 13, 2016 at 12:49 AM, Oleg Grenrus wrote:
First the bike shedding: I’d prefer /~ and :/~:.
>>> Those are indeed better.
>>>
new Typeable [1] would actually provide heterogenous equality:
eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
And this one is tricky, should it be:
eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b ->
Either (Either (k1 :/~: k2) (a :/~: b)) (a :~~: b)
i.e. how kind inequality would work?
>>> I don't know. It sounds like some details of how kinds are expressed
>>> in TypeRep might still be a bit uncertain, but I'm not tuned in. Maybe
>>> we should punt and use heterogeneous inequality? That's over my head.
>>>
I'm not sure about propagation rules, with inequality you have to be
*very* careful!
irreflexivity, x /~ x and symmetry x /~ y <=> y /~ x are clear.
I assume that in your rules, variables are not type families, otherwise
x /~ y => f x /~ f y doesn't hold if `f` isn't injective. (e.g. type
family F x where F x = ())
other direction is true though.
>>> I was definitely imagining them as first-class types; your point that
>>> f x /~ f y => x /~ y even if f is a type family is an excellent o
Compile GHC with -prof to get a stack trace on panic
I think this has been mentioned before but it's probably not widely known:
if you compile GHC profiled (that is, enable GhcProfiled=YES in your mk/
build.mk), then every panic comes with a stack trace. Here's one I just
saw:
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.1.20161206 for x86_64-unknown-linux):
Ix{Int}.index: Index (65536) out of range ((0,28))
CallStack (from -prof):
HscTypes.bin_fixities (compiler/main/HscTypes.hs:1050:51-56)
HscMain.checkOldIface (compiler/main/HscMain.hs:(586,20)-(587,60))
HscMain.hscIncrementalFrontend (compiler/main/HscMain.hs:(556,1)-(618,81))
HscMain.hscIncrementalCompile (compiler/main/HscMain.hs:(644,1)-(699,32))
GHC.withCleanupSession (compiler/main/GHC.hs:(464,1)-(473,27))
GHC.runGhc (compiler/main/GHC.hs:(439,1)-(444,26))
GHC.defaultErrorHandler (compiler/main/GHC.hs:(379,1)-(411,7))
To get more detail in the stack trace you need to add
GhcStage2HcOpts += -fprof-auto-top
Or -fprof-auto, depending on how much detail you want.
Cheers
Simon
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
FYI: base version bump landing soon
Hello fellow Haskellers, Sometime soon (likely today) I'll be landing a commit to `master` which will bump the version of the `base` library to 4.10.0.0 This will involve bumping a number of submodules as well. This will mean that testing against Hackage will typically require that you pass `--allow-newer=base` to cabal. 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
