st0244-2023-1-fp

where
  fp :: String
  fp = "Final Project"

Field	Value
Full name	Luis M. Torres V.
Operating system	Ubuntu 22.04.01 LTS
Programming language	Haskell2010
Compiler version	GHC 9.4.5

General description of program

An implementation of John Alan Robinson's 1971 unification algorithm for first-order terms that attempts to find the most general unifier given a set of constraints or type equations.

The grammar for the input can be seen as the production rules generated by Happy in this file.

The program reads the constraint set from a file using a parser generated by Happy and a lexer generated by Alex.

You can see the algorithm this is based on as a snipping from Pierce's book.

How to run the program

No install

cabal run unify [FILENAME]

The filename must be either:

1. the absolute path or

2. the relative path to the root directory.

Simple(r?)

cabal install

And now it should be in your PATH.

So you can do unify [FILEPATH].

How to run the test suite

cabal test --test-show-details=always

Log example when running cabal test

Robinson's 1971 unification algorithm
  cs1.txt
    should unify with empty substitution [✔]
  cs2.txt
    should unify with two mappings [✔]
  cs3.txt
    should unify with two mappings [✔]
  cs4.txt
    should unify with four mappings [✔]
  cs5.txt
    should not unify [✔]
  cs6.txt
    should unify with one mapping [✔]

Finished in 0.0017 seconds
6 examples, 0 failures

Useful bibliography

1. Benjamin C. Pierce. Types and Programming Languages. 2002. MIT Press.

   Specifically chapter 22, subsections 1 through 4.

2. The CS 3110 Textbook, "OCaml Programming: Correct + Efficient + Beautiful" for the course of the same name at Cornell University.

   • Relevant section: 9.6.3. Solving constraints

   • GitHub repository: cs3110/textbook

   • PDF version: ocaml_programming.pdf

Useful tool for generating the lexer and parser

The BNF Converter from the Chalmers University of Technology and University of Gothenburg.

It is "a compiler construction tool generating a compiler front-end from a Labelled BNF grammar."

Given a Labelled BNF grammar the tool produces:

• an abstract syntax implementation in the target language,
• a case skeleton for the abstract syntax in the target language,
• a pretty-printer in the target language,
• an Alex […] lexer generator file ,
• a Happy […] parser generator file, and
• a LaTeX file containing a readable specification of the language.

Other projects I took a look at

1. Nela Brockington's implementation of Robinson's unification algorithm for types. In Haskell. Project written in April 2016.

2. Eli Bendersky's implementation based on the 1965 paper by Robinson. In Python. Blog post published in November 2018.

3. Daniel Gratzer's explanation of higher-order (not first-order) unification in Haskell. Markdown file published in August 2017.