updated TODOs

README.org

@@ -80,8 +80,11 @@ The error messages currently aren't terrible, but it would be nice to have, e.g.
 *** TODO Improve β-equivalence check
 The check for β-equivalence could certainly be a lot smarter. Right now it just fully normalizes both terms and checks if the normal forms are equal, which isn't the best strategy. This is much less of an issue without [[Inductive Definitions][inductive definitions]]/recursion, as far less computation gets done in general, let alone at the type level. That being said, it's certainly not a bad idea.
 
-*** TODO Better testing
+*** DONE Better testing
 Using some kind of testing framework, like [[https://hackage.haskell.org/package/QuickCheck][QuickCheck]] and/or [[https://hackage.haskell.org/package/HUnit][HUnit]] seems like a good idea. I would like to avoid regressions as I keep working on this, and a suite of unit tests would make me feel much more comfortable.
 
+*** DONE Switch to =Text=
+Currently I use =String= everywhere. Switching to =Text= should be straightforward, and would improve performance and Unicode support.
+
 *** TODO TUI
 This is definitely a stretch goal, but I'm imagining a TUI split into two panels. On the left you can see the term you are building with holes in it. On the right you have the focused hole's type as well as the types of everything in scope (like Coq and Lean show while you're in the middle of a proof). Then you can interact with the system by entering commands (e.g. =intros=, =apply=, etc.) which changes the proof term on the left. You'd also just be able to type in the left window as well, and edit the proof term directly. This way you'd get the benefits of working with tactics, making it way faster to construct proof terms, and the benefits of working with proof terms directly, namely transparency and simplicity. I'll probably want to look into [[https://hackage.haskell.org/package/brick][brick]] in order to make this happen.

app/Main.hs

@@ -3,16 +3,17 @@ module Main where
 import Check
 import Expr
 import Parser
+import qualified Data.Text.IO as T
 import System.IO
 
 main :: IO ()
 main = do
-    _ <- putStr "> "
+    _ <- T.putStr "> "
     _ <- hFlush stdout
-    input <- getLine
+    input <- T.getLine
     case pAll input of
-        Left err -> putStrLn err
+        Left err -> T.putStrLn err
         Right expr -> case findType [] expr of
-            Right ty -> putStrLn $ pretty expr ++ " : " ++ pretty ty
+            Right ty -> T.putStrLn $ pretty expr <> " : " <> pretty ty
             Left err -> print err
     main

dependent-lambda.cabal

@@ -39,6 +39,8 @@ library dependent-lambda-lib
                       , parser-combinators
                       , mtl
     default-language:   Haskell2010
+    default-extensions: OverloadedStrings
+                      , GADTs
 
 common warnings
     ghc-options: -Wall
@@ -49,8 +51,11 @@ executable dependent-lambda
 
     build-depends:      base ^>=4.19.1.0
                       , dependent-lambda-lib
+                      , text
     hs-source-dirs:     app
     default-language:   Haskell2010
+    default-extensions: OverloadedStrings
+                      , GADTs
 
 test-suite tests
     type:               exitcode-stdio-1.0
@@ -60,6 +65,9 @@ test-suite tests
                       , CheckTests
     build-depends:      base ^>=4.19.1.0
                       , HUnit
+                      , text
                       , dependent-lambda-lib
     hs-source-dirs:     tests
     default-language:   Haskell2010
+    default-extensions: OverloadedStrings
+                      , GADTs

lib/Check.hs

@@ -1,21 +1,23 @@
 module Check (TypeCheckError (..), CheckResult (..), findType) where
 
-import Control.Monad.Except ( MonadError(throwError) )
+import Control.Monad.Except (MonadError (throwError))
 import Data.List (intercalate, (!?))
+import Data.Text (Text)
+import qualified Data.Text as T
 
 import Control.Monad (unless)
 import Expr
 
 type Context = [Expr]
 
-data TypeCheckError = SquareUntyped | UnboundVariable String | NotASort Expr Expr | ExpectedPiType Expr Expr | NotEquivalent Expr Expr Expr
+data TypeCheckError = SquareUntyped | UnboundVariable Text | NotASort Expr Expr | ExpectedPiType Expr Expr | NotEquivalent Expr Expr Expr deriving (Eq)
 
 instance Show TypeCheckError where
     show SquareUntyped = "□ does not have a type"
-    show (UnboundVariable x) = "Unbound variable: " ++ x
-    show (NotASort x t) = "Expected " ++ pretty x ++ " to have type * or □, instead found " ++ pretty t
-    show (ExpectedPiType m a) = pretty m ++ " : " ++ pretty a ++ " is not a function"
-    show (NotEquivalent a a' e) = "Cannot unify " ++ pretty a ++ " with " ++ pretty a' ++ " when evaluating " ++ pretty e
+    show (UnboundVariable x) = "Unbound variable: " ++ T.unpack x
+    show (NotASort x t) = "Expected " ++ prettyS x ++ " to have type * or □, instead found " ++ prettyS t
+    show (ExpectedPiType m a) = prettyS m ++ " : " ++ prettyS a ++ " is not a function"
+    show (NotEquivalent a a' e) = "Cannot unify " ++ prettyS a ++ " with " ++ prettyS a' ++ " when evaluating " ++ prettyS e
 
 type CheckResult = Either TypeCheckError
 

lib/Expr.hs

@@ -1,16 +1,16 @@
-{-# LANGUAGE GADTs #-}
-
 module Expr where
 
 import Data.Function (on)
+import Data.Text (Text)
+import qualified Data.Text as T
 
 data Expr where
-    Var :: Integer -> String -> Expr
+    Var :: Integer -> Text -> Expr
     Star :: Expr
     Square :: Expr
     App :: Expr -> Expr -> Expr
-    Abs :: String -> Expr -> Expr -> Expr
-    Pi :: String -> Expr -> Expr -> Expr
+    Abs :: Text -> Expr -> Expr -> Expr
+    Pi :: Text -> Expr -> Expr -> Expr
     deriving (Show)
 
 instance Eq Expr where
@@ -32,58 +32,61 @@ occursFree n (Pi _ a b) = occursFree n a || occursFree (n + 1) b
 
 {- --------------------- PRETTY PRINTING ----------------------------- -}
 
-parenthesize :: String -> String
-parenthesize s = "(" ++ s ++ ")"
+parenthesize :: Text -> Text
+parenthesize s = T.concat ["(", s, ")"]
 
-collectLambdas :: Expr -> ([(String, Expr)], Expr)
+collectLambdas :: Expr -> ([(Text, Expr)], Expr)
 collectLambdas (Abs x ty body) = ((x, ty) : params, final)
   where
     (params, final) = collectLambdas body
 collectLambdas e = ([], e)
 
-collectPis :: Expr -> ([(String, Expr)], Expr)
+collectPis :: Expr -> ([(Text, Expr)], Expr)
 collectPis p@(Pi "" _ _) = ([], p)
 collectPis (Pi x ty body) = ((x, ty) : params, final)
   where
     (params, final) = collectPis body
 collectPis e = ([], e)
 
-groupParams :: [(String, Expr)] -> [([String], Expr)]
+groupParams :: [(Text, Expr)] -> [([Text], Expr)]
 groupParams = foldr addParam []
   where
-    addParam :: (String, Expr) -> [([String], Expr)] -> [([String], Expr)]
+    addParam :: (Text, Expr) -> [([Text], Expr)] -> [([Text], Expr)]
     addParam (x, t) [] = [([x], t)]
     addParam (x, t) l@((xs, s) : rest)
         | incIndices t == s = (x : xs, t) : rest
         | otherwise = ([x], t) : l
 
-showParamGroup :: ([String], Expr) -> String
-showParamGroup (ids, ty) = parenthesize $ unwords ids ++ " : " ++ pretty ty
+showParamGroup :: ([Text], Expr) -> Text
+showParamGroup (ids, ty) = parenthesize $ T.unwords ids <> " : " <> pretty ty
 
-helper :: Integer -> Expr -> String
+helper :: Integer -> Expr -> Text
 helper _ (Var _ s) = s
 helper _ Star = "*"
 helper _ Square = "□"
 helper k (App e1 e2) = if k > 3 then parenthesize res else res
   where
-    res = helper 3 e1 ++ " " ++ helper 4 e2
+    res = helper 3 e1 <> " " <> helper 4 e2
 helper k (Pi "" t1 t2) = if k > 2 then parenthesize res else res
   where
-    res = helper 3 t1 ++ " -> " ++ helper 2 t2
+    res = helper 3 t1 <> " -> " <> helper 2 t2
 helper k e@(Pi{}) = if k > 2 then parenthesize res else res
   where
     (params, body) = collectPis e
     grouped = showParamGroup <$> groupParams params
-    res = "∏ " ++ unwords grouped ++ " . " ++ pretty body
+    res = "∏ " <> T.unwords grouped <> " . " <> pretty body
 helper k e@(Abs{}) = if k >= 1 then parenthesize res else res
   where
     (params, body) = collectLambdas e
     grouped = showParamGroup <$> groupParams params
-    res = "λ " ++ unwords grouped ++ " . " ++ pretty body
+    res = "λ " <> T.unwords grouped <> " . " <> pretty body
 
-pretty :: Expr -> String
+pretty :: Expr -> Text
 pretty = helper 0
 
+prettyS :: Expr -> String
+prettyS = T.unpack . pretty
+
 {- --------------- ACTUAL MATH STUFF ---------------- -}
 
 isSort :: Expr -> Bool

lib/Parser.hs

@@ -7,20 +7,22 @@ import Data.Functor.Identity
 import Data.List (elemIndex)
 import Data.List.NonEmpty (NonEmpty ((:|)))
 import qualified Data.List.NonEmpty as NE
+import Data.Text (Text)
+import qualified Data.Text as T
 import Expr (Expr (..), incIndices)
 import Text.Megaparsec hiding (State)
 import Text.Megaparsec.Char
 import qualified Text.Megaparsec.Char.Lexer as L
 
-type InnerState = [String]
+type InnerState = [Text]
 
-data CustomErrors = UnboundVariable String [String] deriving (Eq, Ord, Show)
+data CustomErrors = UnboundVariable Text [Text] deriving (Eq, Ord, Show)
 
 instance ShowErrorComponent CustomErrors where
     showErrorComponent (UnboundVariable var bound) =
-        "Unbound variable: " ++ var ++ ". Did you mean one of: " ++ unwords bound ++ "?"
+        "Unbound variable: " ++ T.unpack var ++ ". Did you mean one of: " ++ T.unpack (T.unwords bound) ++ "?"
 
-type Parser = ParsecT CustomErrors String (State InnerState)
+type Parser = ParsecT CustomErrors Text (State InnerState)
 
 skipSpace :: Parser ()
 skipSpace =
@@ -32,11 +34,11 @@ skipSpace =
 lexeme :: Parser a -> Parser a
 lexeme = L.lexeme skipSpace
 
-pIdentifier :: Parser String
+pIdentifier :: Parser Text
 pIdentifier = label "identifier" $ lexeme $ do
     firstChar <- letterChar <|> char '_'
     rest <- many $ alphaNumChar <|> char '_'
-    return $ firstChar : rest
+    return $ T.pack (firstChar : rest) -- Still need T.pack here as we're building from chars
 
 pVar :: Parser Expr
 pVar = label "variable" $ lexeme $ do
@@ -46,12 +48,10 @@ pVar = label "variable" $ lexeme $ do
         Just i -> return $ Var (fromIntegral i) var
         Nothing -> customFailure $ UnboundVariable var binders
 
-defChoice :: NE.NonEmpty String -> Parser ()
-defChoice options = lexeme $ label labelText $ void $ choice $ NE.map string options
-  where
-    labelText = NE.head options
+defChoice :: NE.NonEmpty Text -> Parser ()
+defChoice options = lexeme $ label (T.unpack $ NE.head options) $ void $ choice $ NE.map chunk options
 
-pParamGroup :: Parser [(String, Expr)]
+pParamGroup :: Parser [(Text, Expr)]
 pParamGroup = lexeme $ label "parameter group" $ between (char '(') (char ')') $ do
     idents <- some pIdentifier
     _ <- defChoice $ ":" :| []
@@ -59,7 +59,7 @@ pParamGroup = lexeme $ label "parameter group" $ between (char '(') (char ')') $
     modify (flip (foldl $ flip (:)) idents)
     pure $ zip idents (iterate incIndices ty)
 
-pParams :: Parser [(String, Expr)]
+pParams :: Parser [(Text, Expr)]
 pParams = concat <$> some pParamGroup
 
 pLAbs :: Parser Expr
@@ -112,5 +112,5 @@ pAppTerm = lexeme $ pLAbs <|> pPAbs <|> pApp
 pExpr :: Parser Expr
 pExpr = lexeme $ try pArrow <|> pAppTerm
 
-pAll :: String -> Either String Expr
-pAll input = first errorBundlePretty $ fst $ runIdentity $ runStateT (runParserT pExpr "" input) []
+pAll :: Text -> Either Text Expr
+pAll input = first (T.pack . errorBundlePretty) $ fst $ runIdentity $ runStateT (runParserT pExpr "" input) []

tests/CheckTests.hs

@@ -1 +1,75 @@
-module CheckTests where
+module CheckTests (tests) where
+
+import Check
+import Expr (Expr (..))
+import Test.HUnit
+
+sort :: Test
+sort = TestCase $ assertEqual "*" (Right Square) (findType [] Star)
+
+stlc :: Test
+stlc =
+    TestCase $
+        assertEqual
+            "fun (x : A) (y : B) . x"
+            (Right $ Pi "" (Var 0 "A") (Pi "" (Var 2 "B") (Var 2 "A")))
+            (findType [Star, Star] $ Abs "x" (Var 0 "A") (Abs "y" (Var 2 "B") (Var 1 "x")))
+
+polyIdent :: Test
+polyIdent =
+    TestCase $
+        assertEqual
+            "fun (A : *) (x : A) . x"
+            (Right $ Pi "A" Star (Pi "" (Var 0 "A") (Var 1 "A")))
+            (findType [] (Abs "A" Star (Abs "x" (Var 0 "A") (Var 0 "x"))))
+
+typeCons :: Test
+typeCons =
+    TestCase $
+        assertEqual
+            "fun (A B : *) . A -> B"
+            (Right $ Pi "" Star (Pi "" Star Star))
+            (findType [] (Abs "A" Star (Abs "B" Star (Pi "" (Var 1 "A") (Var 1 "B")))))
+
+useTypeCons :: Test
+useTypeCons =
+    TestCase $
+        assertEqual
+            "fun (C : * -> *) (A : *) (x : C A) . x"
+            (Right $ Pi "C" (Pi "" Star Star) (Pi "A" Star (Pi "" (App (Var 1 "C") (Var 0 "A")) (App (Var 2 "C") (Var 1 "A")))))
+            (findType [] $ Abs "C" (Pi "" Star Star) (Abs "A" Star (Abs "x" (App (Var 1 "C") (Var 0 "A")) (Var 0 "x"))))
+
+dependent :: Test
+dependent =
+    TestCase $
+        assertEqual
+            "fun (S : *) (x : S) . S -> S"
+            (Right $ Pi "S" Star (Pi "" (Var 0 "S") Star))
+            (findType [] $ Abs "S" Star (Abs "x" (Var 0 "S") (Pi "" (Var 1 "S") (Var 2 "S"))))
+
+useDependent :: Test
+useDependent =
+    TestCase $
+        assertEqual
+            "fun (S : *) (P : S -> *) (x : S) . P x"
+            (Right $ Pi "S" Star (Pi "" (Pi "" (Var 0 "S") Star) (Pi "" (Var 1 "S") Star)))
+            (findType [] $ Abs "S" Star (Abs "P" (Pi "" (Var 0 "S") Star) (Abs "x" (Var 1 "S") (App (Var 1 "P") (Var 0 "x")))))
+
+big :: Test
+big =
+    TestCase $
+        assertEqual
+            "fun (S : *) (P Q : S -> *) (H : forall (x : S), P x -> Q x) (G : forall (x : S), P x) (x : S) . H x (G x)"
+            (Right $ Pi "S" Star (Pi "P" (Pi "" (Var 0 "S") Star) (Pi "Q" (Pi "" (Var 1 "S") Star) (Pi "" (Pi "x" (Var 2 "S") (Pi "" (App (Var 2 "P") (Var 0 "x")) (App (Var 2 "Q") (Var 1 "x")))) (Pi "" (Pi "x" (Var 3 "S") (App (Var 3 "P") (Var 0 "x"))) (Pi "x" (Var 4 "S") (App (Var 3 "Q") (Var 0 "x"))))))))
+            (findType [] $ Abs "S" Star (Abs "P" (Pi "" (Var 0 "S") Star) (Abs "Q" (Pi "" (Var 1 "S") Star) (Abs "H" (Pi "x" (Var 2 "S") (Pi "" (App (Var 2 "P") (Var 0 "x")) (App (Var 2 "Q") (Var 1 "x")))) (Abs "G" (Pi "x" (Var 3 "S") (App (Var 3 "P") (Var 0 "x"))) (Abs "x" (Var 4 "S") (App (App (Var 2 "H") (Var 0 "x")) (App (Var 1 "G") (Var 0 "x")))))))))
+
+tests :: Test
+tests =
+    TestList
+        [ TestLabel "sort" sort
+        , TestLabel "λ→" stlc
+        , TestLabel "λ2" polyIdent
+        , TestLabel "λω" (TestList [typeCons, useTypeCons])
+        , TestLabel "λP2" (TestList [dependent, useDependent])
+        , TestLabel "λC" big
+        ]

tests/ParserTests.hs

@@ -1,5 +1,7 @@
 module ParserTests (tests) where
 
+import Data.Text (Text)
+import qualified Data.Text as T
 import Expr (Expr (..))
 import Parser (pAll)
 import Test.HUnit

tests/Tests.hs

@@ -1,13 +1,18 @@
 module Main where
 
+import qualified CheckTests as C
 import qualified ExprTests as E
 import qualified ParserTests as P
 import qualified System.Exit as Exit
 import Test.HUnit
 
 tests :: Test
-tests = TestList [ TestLabel "ExprTests" E.tests
-                 , TestLabel "ParserTests" P.tests]
+tests =
+    TestList
+        [ TestLabel "ExprTests" E.tests
+        , TestLabel "ParserTests" P.tests
+        , TestLabel "CheckTests" C.tests
+        ]
 
 main :: IO ()
 main = do