Explicit Dictionary Applications - From Theory to Practice?
At Haskell Symposium 2018, Thomas Winant and I proposed a language extension for allowing explicit dictionary applications in GHC Haskell. Contrary to previous proposals, we were able to preserve coherence and global uniqueness of instances by allowing dictionary applications only when two criteria were satisfied. One of those criteria (the “coherence criterion”) was hard to implement and our prototype implementation in GHC 8.0 actually only checked the other one. The other criterion (the “role criterion”) was less problematic, building on existing GHC infrastructure, specifically roles.
In this talk, I will present a more practical variant of the proposal that is implementable in practice. It features an alternative coherence criterion that is slightly more restrictive but still sufficiently broad for practical examples. Additionally, I will discuss some nice applications, benchmark results and limitations. My goal is to gather feedback and look for collaborators for making this proposal a reality. The same proposal is being worked out in a GHC proposal.
Conference DayFri 23 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
15:20 - 16:30
|HoleFitPlugins and the future of interactive development in GHC|
Matthías Páll GissurarsonChalmers University of Technology, Sweden
|Explicit Dictionary Applications - From Theory to Practice?|
Dominique DevrieseVrije Universiteit BrusselFile Attached
|Visible dependent quantification|
Ryan ScottIndiana University at Bloomington, USAFile Attached