Site Map - skip to main content

Hacker Public Radio

Your ideas, projects, opinions - podcasted.

New episodes Monday through Friday.

hpr3796 :: Dependent Types

A quick taste of programming with dependent types

<< First, < Previous, , Latest >>

Hosted by David Thrane Christiansen on 2023-02-20 is flagged as Clean and is released under a CC-BY-SA license.
types, math, programming languages, functional programming. 1.

Listen in ogg, spx, or mp3 format. Play now:

Duration: 00:08:28


I discuss dependent types, which are types that can contain non-type programs. An example of a dependent type is a list whose type contains its length. Instead of just writing List<String> for a list that contains strings, dependent types include types like List<String, 5> that describe lists of exactly five strings. Dependent types can also be used to represent mathematics, in which case the programs that they describe count as proofs, and tools from programming can be used to write math.

Dependent types used to be something that really required a research background, but there has been a lot of progress on making them more user-friendly and on writing accessible introductions lately.

Languages mentioned:

  • Idris is a self-hosted dependently typed language with type-level resource tracking
  • Agda is a testbed for new ideas in dependently typed programming
  • Lean 4 is a self-hosted dependently typed language that has a more conservative logical core than Idris or Agda, and attempts to appeal more to practicing mathematicians.
  • Coq is a proof assistant based on dependent types that has been used to fully mathematically verify a C compiler

Books mentioned:

  • The Little Typer, by Daniel P. Friedman and David Thrane Christiansen is an intro to the core ideas of dependent types, in dialog form
  • Type Driven Development with Idris by Edwin Brady, the creator of Idris, describes an approach to programming that uses expressive types as a way to make programmers' lives easier
  • Programming Language Foundations in Agda by Phil Wadler, Wen Kokke, and Jeremy Siek describes the use of Agda for both programming and proving
  • Software Foundations is a series of books that use Coq as an introduction to mathematically rigorous software development in a proof assistant. It's how I initially learned these topics!


Subscribe to the comments RSS feed.

Comment #1 posted on 2023-02-22 22:09:16 by mcnalu

Concise and clear

Concise and clear David, but then I expected no less given what you said to me at the HPR stand at FOSDEM. I will be trying out some of these languages and reading the books you mentioned. Thank you for this show!

Leave Comment

Note to Verbose Commenters
If you can't fit everything you want to say in the comment below then you really should record a response show instead.

Note to Spammers
All comments are moderated. All links are checked by humans. We strip out all html. Feel free to record a show about yourself, or your industry, or any other topic we may find interesting. We also check shows for spam :).

Provide feedback
Your Name/Handle:
Anti Spam Question: What does the P in HPR stand for ?