chore: cleanup

Author: miguel-nascimento

README.md

@@ -0,0 +1,26 @@
+# Algorithm J
+
+Hindley–Milner Algorithm J implementation in Rust.
+
+## Showcase
+
+[![asciicast](https://asciinema.org/a/NT4YdX250se2wjcyOZi0Df8cx.svg)](https://asciinema.org/a/NT4YdX250se2wjcyOZi0Df8cx)
+
+## Usage
+
+To run the repl, use the following command:
+
+```rust
+$ cargo run
+```
+
+If you want to type check a file, use the following command:
+
+```rust
+$ cargo run <filename>
+```
+
+## References
+
+- [Hindley–Milner Wikipedia page](https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system)
+- [How OCaml type checker works -- or what polymorphism and garbage collection have in common](https://okmij.org/ftp/ML/generalization.html)

examples/example.hm

@@ -1,9 +1,14 @@
-let id = fun x -> x;
 let unit = id ();
 let perform = fun x -> x ();
 
+let id = fun x -> x;
 let true = fun x -> fun y -> x;
 let false = fun x -> fun y -> y;
 let if = fun b -> fun x -> fun y -> b x y;
-let add = fun m -> fun n -> fun f -> fun x ->  m f (n f x);
 
+let zero = fun f -> fun x -> x;
+let one = fun f -> fun x -> f x;
+let two = fun f -> fun x -> f f x;
+
+let succ = fun n -> fun f -> fun x -> f (n f x);
+let pred = fun n -> fun f -> fun x -> n (fun g -> fun h -> h (g f)) (fun u -> x) (fun u -> u);

src/grammar.lalrpop

@@ -30,12 +30,7 @@ Let: Expr = {
 };
 
 Terminal: Expr = {
-    Int => Expr::Int(<>),
     "()" => Expr::Unit,
     Ident => Expr::Identifier(<>),
     "(" <Expr> ")",
 };
-
-Int: i32 = {
-    r"[0-9]+" => i32::from_str(<>).unwrap(),
-};

src/hm.rs

@@ -1,7 +1,7 @@
-use crate::syntax::Expr;
 /// Implementation of the Hindley-Milner type system
 /// https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system
 /// using the Algorithm J
+use crate::syntax::Expr;
 use anyhow::{anyhow, bail};
 use std::{
     cell::RefCell,
@@ -151,20 +151,6 @@ impl Type {
         })))
     }
 
-    /// Unwrap the inner type of a Bound Var
-    /// let bound_var = Expr::Var(Rc::new(RefCell::new { value: TypeVar::Bound { t: Type::Int } }));
-    /// assert_eq!(bound_var.unwrap_boundvar(), Some(Type::Int))
-    /// ```
-    pub fn unwrap_boundvar(&self) -> Option<Type> {
-        match self {
-            Type::Var(tv) => match &*tv.borrow() {
-                TypeVar::Bound { t } => Some(t.clone()),
-                _ => None,
-            },
-            _ => None,
-        }
-    }
-
     /// Replace vars that can be found in the table. Leave they if not found
     fn replace_vars(&self, table: &HashMap<VarId, Type>) -> Self {
         match self {
@@ -213,7 +199,7 @@ impl Type {
         }
     }
 
-    /// Unify algorithm in J performs mutation, so it doesnt return another type
+    /// Unify algorithm in J performs mutation.
     pub fn unify(&self, other: &Type) -> anyhow::Result<()> {
         match (self, other) {
             (Type::Unit, Type::Unit) => Ok(()),
@@ -226,10 +212,6 @@ impl Type {
                 match &mut *var {
                     TypeVar::Bound { t: a } => a.unify(b),
                     TypeVar::Unbound { id, level } => {
-                        // FIXME: check if its right
-                        // if &self == &other {
-                        //     return Ok(());
-                        // }
                         if b.occurs_check(*id, *level.borrow()) {
                             bail!("Type Error (occurs check)");
                         }
@@ -248,11 +230,6 @@ impl Type {
                 match &mut *var {
                     TypeVar::Bound { t: b } => b.unify(a),
                     TypeVar::Unbound { id, level } => {
-                        // FIXME: check if its right
-                        // if &self == &other {
-                        //     return Ok(());
-                        // }
-
                         if a.occurs_check(*id, *level.borrow()) {
                             bail!("Type Error (occurs check)");
                         }
@@ -293,10 +270,6 @@ impl Env {
             // -----------------------
             // Γ ⊢ () : unit
             Expr::Unit => Ok(Type::Unit),
-            // Int rule
-            // -----------------------
-            // Γ ⊢ n where n is Int : Int
-            Expr::Int(_) => Ok(Type::Int),
             // Var rule
             // x : polytype_a ∈ Γ  t = inst(polytype_a)
             // -----------------------

src/main.rs

@@ -1,6 +1,9 @@
 use std::{collections::HashMap, sync::atomic::Ordering};
 
-use algo_j::{hm::{Env, TYPEVAR_ID}, syntax::expand_all_lets};
+use algo_j::{
+    hm::{Env, TYPEVAR_ID},
+    syntax::expand_all_lets,
+};
 use colored::Colorize;
 use lalrpop_util::lalrpop_mod;
 

src/syntax.rs

@@ -10,9 +10,6 @@ pub enum Expr {
     /// Identifier
     /// `x`
     Identifier(String),
-    /// Int values
-    /// `123`
-    Int(i32),
     /// Lambda abstraction
     /// `\x -> e`
     Lambda(String, Box<Expr>),
@@ -33,7 +30,6 @@ impl Display for Expr {
         match self {
             Expr::Unit => write!(f, "()"),
             Expr::Identifier(id) => write!(f, "{id}"),
-            Expr::Int(int) => write!(f, "{}", int),
             Expr::Lambda(x, body) => write!(f, "fun {} -> {}", x, body),
             Expr::Apply(e1, e2) => {
                 if should_parenthesize(e1) {