u/phadejin r/haskell • Recommends
The Influence of Dependent Types - Stephanie Weirich
0:00 / 0:00
#dependenttypes#haskell#typesystems
The Influence of Dependent Types -- Stephanie Weirich
POPL PARIS 2017
106 subscribers • 2 videos on Hallway
- Recommended by 1 person: 1 in engineering communities.
- Presented by Stephanie Weirich
Advanced. Deep dive for people who know the field.
2.4K views9 years ago1 recommendation
Programming languagesComputer scienceLanguage design and type systemsComputation and complexity
Stephanie Weirich discusses the history, design, and growing influence of dependent type systems in programming languages.
The Influence of Dependent Types -- Stephanie WeirichWhy it's here
1 person recommends thisWhat people say. Recommended as an excellent overview of dependent types and their impact on language design.
Moments people linked to
u/Faucelmein r/haskell • Mentions
On “The Influence of Dependent Types - Stephanie Weirich”
Starting from 27:16, Weirich makes a distinction between compile-time proofs in GHC that have no runtime costs, and run-time proofs that do.
How does that distiction map to languages like Idris, Agda or Coq? My understanding was that in these languages proofs can always be "elided" at runtime because the languages are total. But what would correspond in these languages to GHC's "compile-time" style of proof?
Interesting that he she thinks GHC should move towards automated theored proving a la Liquid Haskell.
u/Iceland_jackin r/haskell • Mentions
On “[ANN] typelits-printf now uses -XRequiredTypeArguments: `printf "hello %d"` type-safe”
This could be used for other type-indexed systems encoded as strings, like regular expressions that statically knows its match groups:
link to this video
https://www.cis.upenn.edu/~sweirich/talks/popl17.pdf