Project Proposal: Dependent Types in OCaml

[alaiasolkobreslin]

What will you do?

My goal for the final project is to implement an OCaml-like language that also supports dependent types. Although Coq already exists, I think it will be a good learning experience to implement a typechecker that deals with dependent types. I want this language to be based on the Calculus of Constructions.

How will you do it?

I already started a project called Hazel (with Cornell student, Chris Lam) with a similar goal in mind in the summer of 2020, but didn't fully think through how dependent types were going to come into play. We have already implemented a lexer and parser and have started a typechecker for our language. The main tasks in this project include extending the lexer and parser to support dependent types and fully implementing the typechecker. The original goal when I started this project was to gain experience with writing compilers for functional programming languages since we did not have that opportunity in 4120. For now, I think a reasonable goal would be to implement an interpreter for this project and finish the compiler when the semester is over. Although Chris isn't a student here anymore, he might continue to contribute to this project.

How will you empirically measure success?

I will measure success based on how many theorems and proofs can be encoded and successfully typechecked in this language. I am thinking of using some exercises in the first chapter of Software Foundations (SF) as I think we will be successful if we can prove some of the most basic theorems from SF.

Team members:

@FlyingRockSquirrel

[sampsyo]

OK, this all sounds cool! To distill the plan, your aim is to implement type checking & interpretation, with compilation (“extraction,” I think, in the dependent types world?) as a stretch goal.

Before you get started, can you please nail down exactly what the evaluation will consist of? Some questions you could answer, for example, include:

• Exactly which SF chapters will you aim to target?
• How will you quantify the breadth of support? Will it be qualitative (here are a list of features we have, and a list of features we don’t) or quantitative (we support this percentage of the exercises in the targeted SF chapters)?
• How will you port the examples? Manually, or with some kind of automatic translation? How can you quickly demonstrate that either approach wil succeed on a nontrivial number of SF exercises, even before you finish the type checker?
• Will you measure anything quantitative about performance, either of type checking or interpretation? If so, what will you be comparing to what?

[alaiasolkobreslin]

• We will target the Logic chapter of SF. We aim to do all of the one star exercises, and maybe some of the two-star exercises such as and_assoc.
• We plan on listing features we have and don't have to show the breadth of support Hazel provides
• We will port the examples manually. We're not really sure how we could ensure that the type checker will succeed on a nontrivial number of SF exercises, but given that Coq's kernel uses the Calculus of Constructions as its foundation, as long as we properly implement the CoC, the conversion should go smoothly.
• The evaluation will consist of SF exercises and their proofs that were successfully typechecked by Hazel. We don't think this is possible, but we think it would also be amusing to compare the time Hazel takes to typecheck a program and the time Coq takes to typecheck an equivalent program (need to see if there is a way to run just the Coq typechecker).

[sampsyo]

OK! This all sounds good, but I want to challenge you to do one extra thing: think of something you can measure quantitatively, not just qualitatively. Is there some kind of percentage you can calculate to quantify support? Find some numerator and denominator that you pick now, before finishing the project, and commit to reporting after finishing it—such that, the bigger the number, the more "successful" you can say you have been. Do you have any thoughts about what that number will be?