Implementing and Optimizing a Simple, Dependently-Typed Language (2010)

9

Implementing and Optimizing a Simple, Dependently-Typed Language (2010) ☶ pdf compilers haskell plt publications.lib.chalmers.se
via nickpsecurity 6 months ago | cached | 5 comments

5

Original version of LambdaPi. A reorganization of that here. Code for this one is here.

3

SeanW 6 months ago | link

Nice simple explanation of Dependent Types, proof-type checking that uses values to determine the types. Though I’m still a little confused. Anybody else have any other good papers that explain Dependent Types?
2

lindig 6 months ago | link

This is very well written and is worth reading for the section about prior work alone. I would have liked a closer look at LambdaPi since I am not familiar with it.
1. 3
  brnhy edited 6 months ago | link
  Henk: A Typed Intermediate Language by Erik Meijer and Simon Peyton Jones contains a tutorial covering the Lambda Cube and can serve as a brief introduction to Pure Type Systems.
  
  Lambda Pi: A Tutorial Implementation of a Dependently Typed Lambda Calculus by Andres Löh, Conor McBride and Wouter Swierstra is a worked introduction to implementing a dependently-typed lambda calculus, and has the resulting implementation available in Haskell which can be useful to follow along.
  
  I’d recommend reading those in order. The Henk paper in particular is great, and despite being from 1997 I haven’t personally found any better introduction to the topic.
  
  (That is, I recommend reading Henk before the actual link regarding LambdaPi or the reorganisation.)
2

brendan 6 months ago | link

Interesting! I’ve been working on my own implementation of LambdaPi in Rust (please don’t repost - it’s still a WIP). Haven’t got up to codegen, so I’ll be interested to have a look at the code and see what they do.
1. 1
  
  nickpsecurity 6 months ago | link
  
  Won’t repost. Good luck on it. Glad this can help. :)