Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Fri 23 Aug 2019 16:06 - 16:30 at Elk - GHC Chair(s): Brent Yorgey

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.

Slides (vdq-hiw.pdf)906KiB

Fri 23 Aug

15:20 - 16:30: HIW 2019 - GHC at Elk
Chair(s): Brent YorgeyHendrix College
hiw-2019-papers15:20 - 15:43
Matthías Páll GissurarsonChalmers University of Technology, Sweden
hiw-2019-papers15:43 - 16:06
Dominique DevrieseVrije Universiteit Brussel
File Attached
hiw-2019-papers16:06 - 16:30
Ryan ScottIndiana University at Bloomington, USA
File Attached