Visible dependent quantification (VDQ) is a new language feature (discussed in this GHC proposal) that will debut in GHC 8.10. VDQ grants the programmer to write first-class kinds that dependently quantify their arguments, such as
forall k -> k -> Type. The key difference between this kind and
forall k. k -> Type is the presence of an arrow after the
forall, which indicates that the
forall is visible. That is to say, a user must explicitly provide the
k argument when instantiating it, rather than relying on type inference to figure it out implicitly.
In this talk, I will explain in more detail what VDQ is and provide examples to demonstrate situations where VDQ can be useful. Since VDQ is required in order to implement a handful of other GHC proposals, such as top-level kind signatures and constrained type families, I will also briefly discuss the interaction between VDQ and these proposals.
If the word “dependent” in “visible dependent quantification” brings Dependent Haskell to mind, that is no coincidence, as VDQ can be considered a very limited form of dependent types. In this talk, I will clarify the relationship between VDQ and Dependent Haskell, and consider what dependently types programs a user can (and cannot) write with VDQ.
Fri 23 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
15:20 - 16:30
GHCHIW at Elk
Chair(s): Brent Yorgey Hendrix College
|HoleFitPlugins and the future of interactive development in GHC|
Matthías Páll Gissurarson Chalmers University of Technology, Sweden
|Explicit Dictionary Applications - From Theory to Practice?|
Dominique Devriese Vrije Universiteit BrusselFile Attached
|Visible dependent quantification|
Ryan Scott Indiana University at Bloomington, USAFile Attached