Rowan explained to me the difference between dependent types and refinement types

Written by Jakub Zalewski
Published: 2016-10-31 (last updated: 2016-10-31)

I am a PhD student at EPSRC Centre for Doctoral Training in Pervasive Parallelism at the University of Edinburgh under supervision of Philip Wadler, Garrett Morris, and Hugh Leather. I am currently working on wide applications of gradual typing in refinement types. Last month (September 2016) I attended the International Conference on Functional Programming (ICFP 2016) in Nara, Japan, as a student volunteer. I also took part in the student research competition that was held at the conference.

The conference was an amazing event, as the attendees were able to enjoy both the wonderful cultural and historical site in Nara and the recent advances in functional programming languages.

Aside from visiting local temples, I received a lot of insighful and constructive feedback for my current research during the student research competition. Furthermore, I was able to meet the researchers that are actively advancing the my research area.

One of such highlights was the opportunity to chat with Rowan Davies, who was one of Frank Pfenning's students that worked on the initial work on refinement types. Rowan explained to me that the difference between dependent types and refinement types is similar to the difference between intrinsic typing, also referred to typing a la Church, and extrinsic typing, also referred to typing a la Curry. He also pointed me towards Frank Pfenning's work on that problem.

I greatly enjoyed the opportunity to attent ICFP'16 as a student volunteer, I learned a lot from the talks and attendees, and I plan to attend the conference next year.