rahulc29/eopl

Solutions to EOPL

I'm Rahul Chhabra (he/they), a student of Information Technology at Indian Institute of Information Technology, Allahabad, graduating in 2025.

My primary interests are best described by "computational trinitarianism" - logic, category theory, dependent type theory (especially cubical ones), and the development and engineering of proof assistants.

Much of my work right now is on my realizability project - a formalisation of categorical realizability from the ground up in Cubical Agda.

eopl's Issues

Implement first-class mutual recursion

Mutual recursion can only be obtained right now through the means of tricks involving the fixpoint combinator. Make it first-class by adding the defmutrec form. Possible concrete syntax :

(defmutrec
     (defproc (odd n)
       (if (= n 0)
           false
           (even (- n 1))))
     (defproc (even n)
       (if (= n 0)
           true
           (odd (- n 1)))))

Implement definitional forms

Implement the following definition forms :

• defval to define values
• defproc to define procedures
• defrec to define recursive procedures
  Doing so we can later extend the language with deftype and the like.

Add corecursion

Currently the language supports recursion as a first-class construct using the fix form.
It might be fun to try to add corecursion as well so that something like the corecursive definition of Fibonacci can be given.

metaFibs x y = x :: metaFibs y (x + y)
fibs = metaFibs 0 1

Possible concrete syntax :

(defcorec (meta-fibs x y) 
   (cons x (meta-fibs y (+ x y))))
(defval fibs (meta-fibs 0 1))

Proper citations in design doc

No citations are made currently and the design doc is more of a shitpost than I would like.
Fix this.

Helpful error messages in parser

Currently if an incorrect string is given to the parser it just blurts an ugly garbage error message that is effectively useless.

Update the parser code to have helpful error messages.

Make design doc on recursion more mathematically formal

The mathematics is essentially given at a very basic level and the amount of rigour is basically none.
More concretely :

• mention the Knaster-Tarski theorem
• show that the convergence point of the approximation sequence is also a solution to the fixpoint equation
• if time permits, actually prove the Knaster-Tarski theorem
• mention the fact our fixpoint discussion is specifically about least fixpoints
• ideally, justify the usage of least fixpoints for recursive definitions and maybe also introduce and justify the usage of greatest fixpoints for corecursive definitions (use BFS as example of corecursion)