Merge unification and system-f branches into main

.github/workflows/ci.yaml

@@ -25,7 +25,7 @@ jobs:
           stack-version: 'latest'
 
       - name: Build
-        run: stack build free-foil-hm
+        run: stack build free-foil-typecheck
 
       - name: Test
         run: stack test

.github/workflows/haddock.yaml

@@ -20,7 +20,7 @@ jobs:
           stack-version: 'latest'
 
       - name: Build Haddock
-        run: stack haddock free-foil-hm
+        run: stack haddock free-foil-typecheck
 
       - name: Detect Haddock path
         run: echo "HADDOCK_DIR_PATH=$(stack path --local-doc-root)" >> $GITHUB_ENV

README.md

@@ -16,13 +16,17 @@ Current goals are:
 
 ## Current progress
 
-At the moment, our work in this repository is divided into two branches: [`system-f`](https://github.com/evermake/free-foil-typecheck/tree/system-f) and [`unification`](https://github.com/evermake/free-foil-typecheck/tree/unification), where you can find our current results on bidirectional typing and Hindley-Milner-style type inference, respectively. Currently, we're working on implementation of type checking and type inference algorithms for a concrete small language.
+Our work in this repository contains implementations of bidirectional typing (System F) and Hindley-Milner-style type inference. Currently, we're working on implementing type checking and type inference algorithms for a concrete small language.
 
-Both branches have the same directory structure:
-- `grammar/` — BNFC grammar describing our concrete language syntax.
-- `src/` — source code of type checker.
-- `app/` — source code of REPL and interpreter binaries for playing with the current implementation.
-- `test/` — scripts and test-cases with input programs for testing type checker functionality.
+The repository has the following directory structure:
+- `grammar/` — BNFC grammars describing concrete language syntaxes.
+- `src/` — source code of type inference and type checking algorithms.
+- `app/` — source code of REPL and interpreter binaries for playing with the current implementations.
+- `test/` — scripts and test-cases with input programs for testing type checkers functionality.
+
+Contents of the mentioned directories are divided for Hindley-Milner and System F implementations.
+
+---
 
 [^1]: Nikolai Kudasov, Renata Shakirova, Egor Shalagin, and Karina Tyulebaeva. 2024. Free Foil: Generating Efficient and Scope-Safe Abstract Syntax. In 2024 4th International Conference on Code Quality (ICCQ). 1–16. https://doi.org/10.1109/ICCQ60895.2024.10576867
 [^2]: Abdelrahman Abounegm, Nikolai Kudasov, and Alexey Stepanov. 2024. Teaching Type Systems Implementation with Stella, an Extensible Statically Typed Programming Language. In Proceedings of the Thirteenth Workshop on Trends in Functional Programming in Education, South Orange, New Jersey, USA, 9th January 2024 (Electronic Proceedings in Theoretical Computer Science, Vol. 405), Stephen Chang (Ed.). Open Publishing Association, 1–19. https://doi.org/10.4204/EPTCS.405.1

Setup.hs

@@ -36,12 +36,22 @@ main =
                 [ "chcp.com" | isWindows ] <>
                 [ "chcp.com 65001" | isWindows ] <>
                 [ "cp grammar/hindley-milner.cf grammar/Parser.cf"  -- Workaround to customize generated package name
-                , "bnfc --haskell -d -p HM --generic -o src grammar/Parser.cf"
+                , "bnfc --haskell -d -p FreeFoilTypecheck.HindleyMilner --generic -o src grammar/Parser.cf"
                 , "rm grammar/Parser.cf"
-                , "cd src/HM/Parser"
+                , "cd src/FreeFoilTypecheck/HindleyMilner/Parser"
                 , "alex Lex.x"
                 , "happy Par.y"
                 , "true"
+                , "cd ../../../.."
+                ] <>
+                [ "cp grammar/system-f.cf grammar/Parser.cf"  -- Workaround to customize generated package name
+                , "bnfc --haskell -d -p FreeFoilTypecheck.SystemF --generic -o src grammar/Parser.cf"
+                , "rm grammar/Parser.cf"
+                , "cd src/FreeFoilTypecheck/SystemF/Parser"
+                , "alex Lex.x"
+                , "happy Par.y"
+                , "true"
+                , "cd ../../../.."
                 ]
 
             fullCommand = [fmt|bash -c ' {command} '|]

app/HindleyMilner/Interpreter.hs

@@ -0,0 +1,18 @@
+module Main where
+
+import FreeFoilTypecheck.HindleyMilner.Interpret
+import System.Exit
+
+main :: IO ()
+main = do
+  sourceCode <- getContents
+  case interpret sourceCode of
+    Success (outExpr, _) -> putStrLn (show outExpr)
+    Failure errorKind errorMsg -> do
+      putStrLn errorMsg
+      exitWith (ExitFailure (errorCode errorKind))
+
+errorCode :: ErrorKind -> Int
+errorCode ParsingError = 1
+errorCode TypecheckingError = 2
+errorCode EvaluationError = 3

app/Repl.hs → app/HindleyMilner/Repl.hs

@@ -1,10 +1,10 @@
 module Main where
 
-import           Control.Monad.Foil (emptyScope, emptyNameMap)
-import           HM.Eval
-import           HM.Parser.Par
-import           HM.Syntax          (toExpClosed)
-import           HM.Typecheck
+import Control.Monad.Foil (emptyScope)
+import FreeFoilTypecheck.HindleyMilner.Eval
+import FreeFoilTypecheck.HindleyMilner.Parser.Par
+import FreeFoilTypecheck.HindleyMilner.Syntax (toExpClosed)
+import FreeFoilTypecheck.HindleyMilner.Typecheck
 
 main :: IO ()
 main = do
@@ -15,10 +15,10 @@ repl :: String -> String
 repl input =
   case toExpClosed <$> pExp tokens of
     Left err -> "Parsing error: " ++ err
-    Right e -> case inferType emptyNameMap e of
+    Right e -> case inferTypeNewClosed e of
       Left err -> "Typechecking error: " ++ err
       Right _type -> case eval emptyScope e of
-        Left err     -> "Evaluation error: " ++ err
+        Left err -> "Evaluation error: " ++ err
         Right outExp -> show outExp
   where
     tokens = myLexer input

app/Interpreter.hs → app/SystemF/Interpreter.hs

@@ -1,9 +1,10 @@
 module Main where
 
-import HM.Interpret
+import FreeFoilTypecheck.SystemF.Interpret
 import System.Exit
 
 main :: IO ()
+-- main = undefined
 main = do
   sourceCode <- getContents
   case interpret sourceCode of

app/SystemF/Repl.hs

@@ -0,0 +1,24 @@
+module Main where
+
+import           Control.Monad.Foil (emptyNameMap)
+import           FreeFoilTypecheck.SystemF.Eval
+import           FreeFoilTypecheck.SystemF.Parser.Par
+import           FreeFoilTypecheck.SystemF.Syntax          (toTermClosed)
+import           FreeFoilTypecheck.SystemF.Typecheck
+
+main :: IO ()
+main = do
+  putStrLn "Welcome to REPL!\n"
+  interact (unlines . map repl . lines)
+
+repl :: String -> String
+repl input =
+  case toTermClosed <$> pTerm tokens of
+    Left err -> "Parsing error: " ++ err
+    Right e -> case inferType emptyNameMap e of
+      Left err -> "Typechecking error: " ++ err
+      Right _type -> case eval emptyNameMap e of
+        Left err     -> "Evaluation error: " ++ err
+        Right outExp -> show outExp
+  where
+    tokens = myLexer input