unification-pfa/README.md

# Project of "Programmation Fonctionelle Avancé"

This file is divided in two parts.
The first part describes the project that you have to
realise to get a partial note for the module
"Programmation Fonctionelle Avancé".

## PART I: Scientific content the project

To realise this project you will implement a type inference
algorithm that works over terms of a programming language
for functional programming.

## Terms = Expressions = Programs

- [Term](./lib/term.mli) This module contains the syntax of
  the minimal programming language to we use in this project.
  Terms (i.e. programs) are values of type `Term.t`.
  This language is "applicative", i.e. fit for functional programming,
  thanks to the constructors for application (`App`) and
  for function definition (`Fun`).

## Aim of the project

The [third lecture]
(https://gaufre.informatique.univ-paris-diderot.fr/Bernardi/pfa-2324/tree/master/week03)
describes two algorithms:
the first one transforms any given program into a system of
equations, and the second one is a unification algorithm that solves
such systems.

To realise this project you will have to implement the following modules:

1. [typeSubstitution](./lib/typeSubstituion.ml)
   You must implement at least:

   - [ ] `type t`, i.e. how to represent syntactic substitutions in memory,
   - [ ] `val apply`, which applies a syntactic substitution to a type
   - [ ] `val compose`, which computes the substitution obtained composing two given substitutions.

1. [unifcation](./lib/unification.ml)
   You must implement at least:

   - [ ] `val unify` which given two type `t1` and `t2`,
         must compute the substitution `s` such that if
         `unify t1 t2 = Some s` then `apply s t1 = apply s t2`.

   You can of course use the Herbrand / Robinson algorithm
   to start designing your implementation.

1. [inference](./lib/inference.ml)
   You must implement at least:
   - [ ] `val typeof`, which given a term `t` must compute either
         `None`, if there is no type for `t`, or `Some ty`, if ty is the type of term `t`.

You may add more definitions to each of these modules, and extend their signatures accordingly.
You may also create new compilation units (i.e. new `.ml` files).

1. You may, and _should_, extend the [testing module](./test/test_projet_pfa_23_24.ml) with additional
   tests, or replace it with a testing framework of your choice (using e.g. QCheck).

## PART II: Logistics of the project

## Fork

To realise your project and have it evaluated,
you have to

1. fork the git repository that contains this file, and
1. add G. BERNARDI and G. GEOFFROY with the role `Maintainer` to your fork.

Do it asap.

## Deadline

The final implementation must be in your fork by the

** 30th of April 2024, 23h59 **

Any code pushed to your fork after that time will be ignored.

## Requirements

### 1. Install OPAM

[OPAM](https://opam.ocaml.org/) is the package manager for OCaml. It
is the recommended way to install the OCaml compiler and OCaml
packages.

The following should work for macOS and Linux:

```sh
bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)"
```

### Recommended: editor integration

#### Emacs: Tuareg & Merlin

[Tuareg](https://github.com/ocaml/tuareg) is an OCaml major mode for
Emacs while [Merlin](https://github.com/ocaml/merlin) is an editor
service that provides modern IDE features for OCaml.

To install, run:

```sh
opam install tuareg merlin user-setup
```

#### VSCode: Ocaml LSP

Install the extension called **OCaml Platform** available in the
[Visual Studio
Marketplace](https://marketplace.visualstudio.com/items?itemName=ocamllabs.ocaml-platform)

This extension requires
[OCaml-LSP](https://github.com/ocaml/ocaml-lsp), an Language Server
Protocol(LSP) implementation for OCaml

To install, run:

```sh
opam install ocaml-lsp-server
```

## Development environment setup

If the required opam packages conflict with your default switch, you may setup a [local](https://opam.ocaml.org/blog/opam-local-switches/) Opam switch using the following commands:

```
$ opam switch create . --deps-only --with-doc --with-test
$ eval $(opam env)
```

## Build

To build the project, type:

```
$ dune build
```

For continuous build, use

```
$ dune build --watch
```

instead.

## Running your main file

To run your code you will have to implement
`let () = ...` in the file `main.ml`, and
then run it via

```
$ dune exec
```

## Testing your code

To test the project, type:

```
$ dune runtest
```

This can be combined with continuous build & test, using

```
$ dune runtest --watch
```