diff options
| -rw-r--r-- | app/Main.hs | 3 | ||||
| -rw-r--r-- | mili.cabal | 2 | ||||
| -rw-r--r-- | readme.md | 33 | ||||
| -rw-r--r-- | samples/logic.mili | 14 | ||||
| -rw-r--r-- | src/Data/Mili.hs | 45 | ||||
| -rw-r--r-- | src/Language/Mili/Analyzer.hs | 20 | ||||
| -rw-r--r-- | src/Language/Mili/Compiler.hs | 19 | ||||
| -rw-r--r-- | src/Language/Mili/Parser.hs | 2 | ||||
| -rw-r--r-- | src/Language/Mili/Reducer.hs | 25 | ||||
| -rw-r--r-- | src/Language/Mili/Typer.hs | 42 |
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 @@ -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: @@ -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, [])) |