Skip to content
Hallway
0:00 / 0:00

#haskell#dependenttypes#ghc

"Dependent Types in Haskell" by Stephanie Weirich

Strange Loop Conference

88K subscribers • 114 videos on Hallway • Conference channel

YouTube
  • Recommended by 5 people: 4 in engineering communities and 1 curated list.
  • Presented by Stephanie Weirich, Professor of Computer and Information Science at the University of Pennsylvania

Advanced. Deep dive for people who know the field.

25K views9 years ago5 recommendations

Programming languagesHaskellLanguage design and type systems

Stephanie Weirich discusses the influence of dependent type theory on GHC and demonstrates how to program with dependent types in Haskell.

What has dependent type theory done for Haskell? Over the past ten years, the Glasgow Haskell compiler (GHC) has adopted many type system features inspired by dependent type theory. In this talk, I will discuss the influence of dependent types on the design of GHC and on the practice of Haskell programmers. In particular, I will walk through an extended example and use it to analyze what it means to program with with dependent types in Haskell. Throughout, I will will discuss what we have learned from this experiment in language design: what works now, what doesn't work yet, and what surprised us along the way. Stephanie Weirich UNIVERSITY OF PENNSYLVANIA Stephanie Weirich is a Professor of Computer and Information Science at the University of Pennsylvania, having received tenure in 2008 and the rank of full professor in 2015. She received her B.A. in Computer Science from Rice University and her Ph.D. from Cornell University. She has published broadly in the areas of functional programming, type systems, machine-assisted theorem proving and dependent types. During the past ten years, she and her students have made significant contributions to the design of the Glasgow Haskell Compiler and its type system. Dr. Weirich has served as the program chair of the The 15th ACM SIGPLAN International Conference on Functional Programming, ICFP 2010 and the 2009 Haskell Symposium and is also an editor of the Journal of Functional Programming. She has given invited talks at many venues, including ICFP, FLOPS, RDP, LFMTP, OPLSS, and PLMW. Her recent awards include a 2016 Microsoft Outstanding Collaborator award, and the 2016 Most Influential ICFP Paper award (for 2006) for the paper "Simple unification-based type inference for GADTs" with her co-authors Simon Peyton Jones, Dimitrios Vytiniotis and Geoffrey Washburn, and the 2016 ACM SIGPLAN Robin Milner Young Researcher Award.

Why it's here

5 people recommend this

What people say. Highly recommended as an excellent explanation of dependent types, singletons, and type-level programming in Haskell.

Moments people linked to

u/madjarin r/haskell • Recommends

On “Optics + Regex: Greater than the sum of their parts”

This sounds like what Stephanie Weirich presented in her talk "Dependent Types in Haskell". You can find a recording at link to this video The code is here: https://github.com/sweirich/dth/tree/master/regexp.
5View on Reddit

programming-talkscurated list on GitHubRecommends

Under “Haskell”

Dependent Types in Haskell 00:38:41 by **Stephanie Weirich** (2017)
View the list

u/healthcare-rightsin r/haskell • Recommends

On “Minimal language extensions for dependently typed Haskell”

This repo by Stephanie Weirich is particularly helpful for finding examples: https://github.com/sweirich/dth One of her talks (link to this video ) addresses 4 reasons to do dependent types. Each reason is given a list of extensions. Apparently for some it’s clear which ones are “the way”, but for others it’s less clear.
4View on Reddit

u/theindigamerin r/haskell • Recommends

On “[PDF] Stephen Diehl - Reasoning about Program Behavior Algebraically”

While mbw_rdt has written a lot of good explanations for the different points, if you're looking for a complementary explanation, there's a Strange Loop 2017 talk by Stephanie Weirich on dependent types in Haskell which includes singletons, among other things. I've seen the Refl bit in an Idris talk (YouTube - Idris: practical dependent types)
3View on Reddit

u/gelisamin r/haskell • Recommends

On “N00b post: Understanding the functor []”

> Why don't give Haskell a stronger type checker so it can automatically check whether a functor satisfies the axioms? It is a theoretical barrier? Yes and no. There currently exists type systems called "dependent types" which does make it possible to guarantee this kind of properties. But there are a few obstacles: Idris, for example, is very similar to Haskell except it supports dependent types. But there are a few obstacles in bringing those into Haskell: 1. Adding those features to an existing language which wasn't designed with dependent types in mind requires careful design considerations in order to add the feature in a way which fits with the rest of the language and doesn't break…
3View on Reddit

u/infinity0xin r/haskell • Mentions

On “Questions on actually doing dependently-typed programming in practise”

Great, thanks for the pointers! I'll have a look. Regarding encoding proofs as terms, I've seen mentions of this idea dotted around but couldn't find specific examples that covered my use-context - for Haskell singletons that is. `ConstrainList cc` is of kind `Constraint` not `Type` so your last example wouldn't work as-is. I could maybe instead use a singleton of it, and perhaps the rest of the function could decompose the type of the input `Sing` to generate the tail `Sing`, but then I'd be at a loss on how to *make use* of it back in client code, to recover the constraint. That is, there are two things in play here, (1) the encoding of the proof as a constraint, but also (2) the `c` par…
2View on Reddit