Initial typingHEADmain

10 files changed, 135 insertions, 70 deletions

diff --git a/app/Main.hs b/app/Main.hs
index 06843fc..5d4d978 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -11,6 +11,7 @@ import qualified Data.Text                     as T
 import           Language.Mili.Analyzer         ( linearity )
 import           Language.Mili.Parser           ( parseProgram )
 import           Language.Mili.Reducer          ( nf )
+import           Language.Mili.Typer            ( typeCheck )
 import           Options.Applicative            ( (<**>)
                                                 , Parser
                                                 , execParser
@@ -30,7 +31,7 @@ args :: Parser Args
 args = pure $ Args ArgEval
 
 pipeline :: T.Text -> Either String Term
-pipeline program = parseProgram program >>= linearity
+pipeline program = parseProgram program >>= linearity >>= typeCheck
 
 actions :: Args -> IO ()
 actions Args { _argMode = ArgEval } = do
diff --git a/mili.cabal b/mili.cabal
index fc756f0..a52f740 100644
--- a/mili.cabal
+++ b/mili.cabal
@@ -25,8 +25,10 @@ library
   exposed-modules:
       Data.Mili
       Language.Mili.Analyzer
+      Language.Mili.Compiler
       Language.Mili.Parser
       Language.Mili.Reducer
+      Language.Mili.Typer
   other-modules:
       Paths_mili
   hs-source-dirs:
diff --git a/readme.md b/readme.md
index 7d0378d..c49f396 100644
--- a/readme.md
+++ b/readme.md
@@ -1,44 +1,49 @@
 # mili
 
 > Minimal linear lambda calculus with linear types, de Bruijn indices
-> and unbounded iteration/minimization
+> and unbounded iteration
 
 Linear lambda calculus is a restricted version of the lambda calculus in
 which every variable occurs exactly once. This typically implies ptime
 normalization and therefore Turing incompleteness.
 
-We extend the linear lambda calculus with unbounded
-iteration/minimization such that it barely becomes Turing complete,
-while still benefitting from the advantages of syntactic linearity.
+We extend the linear lambda calculus with unbounded iteration such that
+it barely becomes Turing complete, while still benefitting from the
+advantages of syntactic linearity.
 
 ## core
 
 Mili's core syntactic representation consists of only five constructs:
 
 ``` haskell
-data Term = Abs Int Term                    -- | Abstraction at level
-          | App Term Term                   -- | Application
-          | Lvl Int                         -- | de Bruijn level
-          | Num Nat                         -- | Peano numeral
-          | Rec (Term, Term) Term Term Term -- | Unbounded iteration
+data Term = Abs Int Term                 -- | Abstraction at level
+          | App Term Term                -- | Application
+          | Lvl Int                      -- | de Bruijn level
+          | Num Nat                      -- | Peano numeral
+          | Rec Term Term Term Term Term -- | Unbounded iteration
 ```
 
-Lets and Pairs are only used in the higher-level syntax. This allows us
-to use a minimal abstract reduction machine.
+Lets and Pairs are only used in the higher-level syntax. There are no
+erasers or duplicators. This allows us to use a minimal abstract
+reduction machine as well as a linear type system.
+
+In general, a more elegant encoding would be *tagless*, as can be seen
+in an implementation by [by Oleg
+Kiselyov](https://okmij.org/ftp/tagless-final/course/LinearLC.hs).
+However, tagless encodings are hard to work with and can't be compiled.
 
 ## roadmap
 
 -   [x] basic syntax
 -   [x] linearity check
 -   [x] basic reduction
--   [ ] type syntax
 -   [ ] type checking
--   [ ] reduction shortcut
+-   [ ] syntax that embeds linearity (levels?)
+-   [ ] compile to LLVM stack machine + reduction shortcut
 -   [ ] preprocessor
     -   [ ] `:test`
     -   [ ] `:import`
 -   [ ] more examples
--   [ ] compile to LLVM stack machine
 
 ## references
 
diff --git a/samples/logic.mili b/samples/logic.mili
new file mode 100644
index 0000000..ce6470c
--- /dev/null
+++ b/samples/logic.mili
@@ -0,0 +1,14 @@
+-- garbage collection hack
+gc = [0 [0] [0] [0]]
+
+true = [[[0 2 1]]]
+false = [[[0 1 2]]]
+
+not = [[[2 0 1]]]
+
+and = [[1 0 false [[gc 0 1]]]]
+nand = [[not (and 1 0)]]
+or = [[1 true 0 [[gc 0 1]]]]
+nor = [[not (or 1 0)]]
+
+([0] <0>)
diff --git a/src/Data/Mili.hs b/src/Data/Mili.hs
index c10b24f..de709f1 100644
--- a/src/Data/Mili.hs
+++ b/src/Data/Mili.hs
@@ -3,7 +3,6 @@
 module Data.Mili
   ( Term(..)
   , Nat(..)
-  , foldM
   , fold
   , shift
   ) where
@@ -44,31 +43,6 @@ instance Show Term where
       . showString ", "
       . shows w
 
-foldM
-  :: Monad m
-  => (Int -> Term -> m Term)
-  -> (Term -> Term -> m Term)
-  -> (Int -> m Term)
-  -> (Nat -> m Term)
-  -> (Term -> Term -> Term -> Term -> Term -> m Term)
-  -> Term
-  -> m Term
-foldM abs app lvl num rec (Abs d m) = foldM abs app lvl num rec m >>= abs d
-foldM abs app lvl num rec (App a b) = do
-  a' <- foldM abs app lvl num rec a
-  b' <- foldM abs app lvl num rec b
-  app a' b'
-foldM _   _   lvl _   _   (Lvl i          ) = pure i >>= lvl
-foldM _   _   _   num _   (Num Z          ) = pure Z >>= num
-foldM abs app lvl num rec (Num (S m)) = foldM abs app lvl num rec m >>= num . S
-foldM abs app lvl num rec (Rec t1 t2 u v w) = do
-  t1' <- foldM abs app lvl num rec t1
-  t2' <- foldM abs app lvl num rec t2
-  u'  <- foldM abs app lvl num rec u
-  v'  <- foldM abs app lvl num rec v
-  w'  <- foldM abs app lvl num rec w
-  rec t1' t2' u' v' w'
-
 fold
   :: (Int -> Term -> Term)
   -> (Term -> Term -> Term)
@@ -77,13 +51,18 @@ fold
   -> (Term -> Term -> Term -> Term -> Term -> Term)
   -> Term
   -> Term
-fold abs app lvl num rec term = runIdentity $ foldM
-  (\d m -> pure $ abs d m)
-  (\a b -> pure $ app a b)
-  (pure . lvl)
-  (pure . num)
-  (\t1 t2 u v w -> pure $ rec t1 t2 u v w)
-  term
+fold abs app lvl num rec (Abs l m) = abs l $ fold abs app lvl num rec m
+fold abs app lvl num rec (App a b) =
+  app (fold abs app lvl num rec a) (fold abs app lvl num rec b)
+fold _   _   lvl _   _   (Lvl n          ) = lvl n
+fold _   _   _   num _   (Num Z          ) = num Z
+fold abs app lvl num rec (Num (S t)) = num $ S $ fold abs app lvl num rec t
+fold abs app lvl num rec (Rec t1 t2 u v w) = rec
+  (fold abs app lvl num rec t1)
+  (fold abs app lvl num rec t2)
+  (fold abs app lvl num rec u)
+  (fold abs app lvl num rec v)
+  (fold abs app lvl num rec w)
 
 shift :: Int -> Term -> Term
 shift 0 = id
diff --git a/src/Language/Mili/Analyzer.hs b/src/Language/Mili/Analyzer.hs
index d4996ee..37c4437 100644
--- a/src/Language/Mili/Analyzer.hs
+++ b/src/Language/Mili/Analyzer.hs
@@ -37,10 +37,10 @@ traceAbs = go 0 [Root]
   go n t (Abs _ m) =
     M.unionWith (++) (go (n + 1) (AbsD : t) m) (M.singleton n [t])
   go n t (App a b) = M.unionWith (++) (go n (AppL : t) a) (go n (AppR : t) b)
-  go _ _ (Lvl _             ) = M.empty
-  go _ _ (Num Z             ) = M.empty
-  go n t (Num (S i)         ) = go n (NumS : t) i
-  go n t (Rec (t1, t2) u v w) = foldl1
+  go _ _ (Lvl _          ) = M.empty
+  go _ _ (Num Z          ) = M.empty
+  go n t (Num (S i)      ) = go n (NumS : t) i
+  go n t (Rec t1 t2 u v w) = foldl1
     (M.unionWith (++))
     [ go n (RecT1 : t) t1
     , go n (RecT2 : t) t2
@@ -56,12 +56,12 @@ traceAbs = go 0 [Root]
 traceLvl :: Term -> HashMap Int [Trace]
 traceLvl = go [Root]
  where
-  go t (Abs _ m           ) = go (AbsD : t) m
-  go t (App a b) = M.unionWith (++) (go (AppL : t) a) (go (AppR : t) b)
-  go t (Lvl l             ) = M.singleton l [t]
-  go _ (Num Z             ) = M.empty
-  go t (Num (S i)         ) = go (NumS : t) i
-  go t (Rec (t1, t2) u v w) = foldl1
+  go t (Abs _ m        ) = go (AbsD : t) m
+  go t (App a b        ) = M.unionWith (++) (go (AppL : t) a) (go (AppR : t) b)
+  go t (Lvl l          ) = M.singleton l [t]
+  go _ (Num Z          ) = M.empty
+  go t (Num (S i)      ) = go (NumS : t) i
+  go t (Rec t1 t2 u v w) = foldl1
     (M.unionWith (++))
     [ go (RecT1 : t) t1
     , go (RecT2 : t) t2
diff --git a/src/Language/Mili/Compiler.hs b/src/Language/Mili/Compiler.hs
new file mode 100644
index 0000000..ab23767
--- /dev/null
+++ b/src/Language/Mili/Compiler.hs
@@ -0,0 +1,19 @@
+-- MIT License, Copyright (c) 2024 Marvin Borner
+
+module Language.Mili.Compiler
+  ( compile
+  ) where
+
+import           Data.Mili                      ( Nat(..)
+                                                , Term(..)
+                                                , shift
+                                                )
+
+data Comp = CAbs String Comp                  -- | Abstraction with pointer
+              | CApp Comp Comp                -- | Application
+              | CVar                          -- | Namless variable
+              | CNum Nat                      -- | Peano numeral
+              | CRec Comp Comp Comp Comp Comp -- | Unbounded iteration
+
+compile :: Term -> Comp
+compile t = CVar
diff --git a/src/Language/Mili/Parser.hs b/src/Language/Mili/Parser.hs
index b9f7881..0854ab1 100644
--- a/src/Language/Mili/Parser.hs
+++ b/src/Language/Mili/Parser.hs
@@ -115,7 +115,7 @@ rec = do
   _  <- spaces
   _  <- startSymbol ","
   w  <- term
-  pure $ Rec (t1, t2) u v w
+  pure $ Rec t1 t2 u v w
 
 -- | single identifier, directly parsed to corresponding term
 def :: Parser Term
diff --git a/src/Language/Mili/Reducer.hs b/src/Language/Mili/Reducer.hs
index dc8c9bd..27ac029 100644
--- a/src/Language/Mili/Reducer.hs
+++ b/src/Language/Mili/Reducer.hs
@@ -13,25 +13,28 @@ data Singleton = TermTag Term | RecTag Term Term Term Term
 
 -- TODO: There will only ever be one substitution, so don't iterate the entire tree!
 -- WARNING: This function also shifts the substituted term and the levels of the parent!
+-- TODO: replace with foldM?
+-- In compilation this won't be necessary since Abs can have a direct pointer to the variable
 subst :: Int -> Int -> Term -> Term -> Term
 subst c l (Abs d m) s = Abs (d - 1) $ subst (c + 1) l m s
 subst c l (App a b) s = App (subst c l a s) (subst c l b s)
 subst c l (Lvl i) s | l == i    = shift c s
                     | otherwise = Lvl $ i - 1
-subst _ _ (Num Z             ) _ = Num Z
-subst c l (Num (S m)         ) s = Num $ S $ subst c l m s
-subst c l (Rec (t1, t2) u v w) s = Rec (subst c l t1 s, subst c l t2 s)
-                                       (subst c l u s)
-                                       (subst c l v s)
-                                       (subst c l w s)
+subst _ _ (Num Z          ) _ = Num Z
+subst c l (Num (S m)      ) s = Num $ S $ subst c l m s
+subst c l (Rec t1 t2 u v w) s = Rec (subst c l t1 s)
+                                    (subst c l t2 s)
+                                    (subst c l u s)
+                                    (subst c l v s)
+                                    (subst c l w s)
 
 machine :: Term -> [Singleton] -> Term
-machine (App a b           ) s                    = machine a (TermTag b : s)
-machine (Abs l u           ) (TermTag t : s)      = machine (subst 0 l u t) s
-machine (Rec (t1, t2) u v w) s = machine t1 (RecTag t2 u v w : s)
-machine (Num Z             ) (RecTag _ u _ _ : s) = machine u s
+machine (App a b        ) s                    = machine a (TermTag b : s)
+machine (Abs l u        ) (TermTag t : s)      = machine (subst 0 l u t) s
+machine (Rec t1 t2 u v w) s = machine t1 (RecTag t2 u v w : s)
+machine (Num Z          ) (RecTag _ u _ _ : s) = machine u s
 machine (Num (S t1)) ((RecTag t2 u v w) : s) =
-  machine v (TermTag (Rec (App w t1, App w t2) u v w) : s)
+  machine v (TermTag (Rec (App w t1) (App w t2) u v w) : s)
 machine (Num (S t)) s = Num $ S $ machine t s -- TODO: ??
 machine t           _ = t
 
diff --git a/src/Language/Mili/Typer.hs b/src/Language/Mili/Typer.hs
new file mode 100644
index 0000000..d6b453b
--- /dev/null
+++ b/src/Language/Mili/Typer.hs
@@ -0,0 +1,42 @@
+-- MIT License, Copyright (c) 2024 Marvin Borner
+
+module Language.Mili.Typer
+  ( typeCheck
+  ) where
+
+import           Control.Monad.State
+import           Data.HashMap.Strict            ( HashMap )
+import qualified Data.HashMap.Strict           as M
+import           Data.Mili                      ( Nat(..)
+                                                , Term(..)
+                                                )
+
+data Type = Number | Lolli Type Type
+  deriving (Show, Eq)
+type Context = HashMap Int Type
+
+-- | Convert de Bruijn levels to unique variables
+annotate :: Term -> State (Int, [Int]) Term
+annotate (Abs _ m) = do
+  (s, ls) <- get
+  put (s + 1, s : ls)
+  an <- annotate m
+  modify $ \(s', _) -> (s', ls)
+  pure $ Abs s an
+annotate (App a b) = (App <$> annotate a) <*> annotate b
+annotate (Lvl i  ) = do
+  (_, ls) <- get
+  pure $ Lvl $ ls !! (length ls - i - 1)
+annotate (Num Z    ) = pure $ Num Z
+annotate (Num (S m)) = Num . S <$> annotate m
+annotate (Rec t1 t2 u v w) =
+  Rec
+    <$> annotate t1
+    <*> annotate t2
+    <*> annotate u
+    <*> annotate v
+    <*> annotate w
+
+typeCheck :: Term -> Either String Term
+typeCheck t =
+  Left $ show (inferGamma M.empty M.empty $ evalState (annotate t) (0, []))