diff options
| -rw-r--r-- | .gitignore | 2 | ||||
| -rw-r--r-- | Setup.hs | 2 | ||||
| -rw-r--r-- | app/Main.hs | 45 | ||||
| -rw-r--r-- | mili.cabal | 59 | ||||
| -rw-r--r-- | notes | 4 | ||||
| -rw-r--r-- | package.yaml | 45 | ||||
| -rw-r--r-- | readme.md | 12 | ||||
| -rw-r--r-- | samples/test.lil | 11 | ||||
| -rw-r--r-- | src/Data/Mili.hs | 13 | ||||
| -rw-r--r-- | src/Language/Mili/Analyzer.hs | 76 | ||||
| -rw-r--r-- | src/Language/Mili/Parser.hs | 127 | ||||
| -rw-r--r-- | src/Language/Mili/Reducer.hs | 9 | ||||
| -rw-r--r-- | stack.yaml | 67 | ||||
| -rw-r--r-- | stack.yaml.lock | 13 |
14 files changed, 485 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..c368d45 --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +.stack-work/ +*~
\ No newline at end of file diff --git a/Setup.hs b/Setup.hs new file mode 100644 index 0000000..9a994af --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/app/Main.hs b/app/Main.hs new file mode 100644 index 0000000..b0a3aca --- /dev/null +++ b/app/Main.hs @@ -0,0 +1,45 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Main + ( main + ) where + +import Data.Mili ( Term(..) ) +import qualified Data.Text as T +import Language.Mili.Analyzer ( linearity ) +import Language.Mili.Parser ( parseProgram ) +import Language.Mili.Reducer ( nf ) +import Options.Applicative ( (<**>) + , Parser + , execParser + , fullDesc + , header + , helper + , info + ) + +data ArgMode = ArgEval + +newtype Args = Args + { _argMode :: ArgMode + } + +args :: Parser Args +args = pure $ Args ArgEval + +pipeline :: T.Text -> Either String Term +pipeline program = parseProgram program >>= linearity + +actions :: Args -> IO () +actions Args { _argMode = ArgEval } = do + program <- getContents + case pipeline (T.pack program) of + Left err -> putStrLn err + Right out -> + let term = show out + normal = show $ nf out + in putStrLn $ term <> "\n" <> normal + +main :: IO () +main = execParser opts >>= actions + where opts = info (args <**> helper) (fullDesc <> header "bruijn but linear") diff --git a/mili.cabal b/mili.cabal new file mode 100644 index 0000000..fc756f0 --- /dev/null +++ b/mili.cabal @@ -0,0 +1,59 @@ +cabal-version: 1.12 + +-- This file has been generated from package.yaml by hpack version 0.37.0. +-- +-- see: https://github.com/sol/hpack + +name: mili +version: 0.1.0.0 +description: Please see the README on GitHub at <https://github.com/marvinborner/mili#readme> +homepage: https://github.com/marvinborner/mili#readme +bug-reports: https://github.com/marvinborner/mili/issues +author: Marvin Borner +maintainer: develop@marvinborner.de +copyright: 2024 Marvin Borner +license: MIT +build-type: Simple +extra-source-files: + readme.md + +source-repository head + type: git + location: https://github.com/marvinborner/mili + +library + exposed-modules: + Data.Mili + Language.Mili.Analyzer + Language.Mili.Parser + Language.Mili.Reducer + other-modules: + Paths_mili + hs-source-dirs: + src + ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints + build-depends: + base >=4.7 && <5 + , megaparsec + , mtl + , optparse-applicative + , text + , unordered-containers + default-language: Haskell2010 + +executable mili-exe + main-is: Main.hs + other-modules: + Paths_mili + hs-source-dirs: + app + ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N + build-depends: + base >=4.7 && <5 + , megaparsec + , mili + , mtl + , optparse-applicative + , text + , unordered-containers + default-language: Haskell2010 @@ -0,0 +1,4 @@ +<+0> <-0> +<<-0>| |<+0>> +<|<+0>>| |<<-0>|> +<|<<-0>|>| |<|<+0>>|> diff --git a/package.yaml b/package.yaml new file mode 100644 index 0000000..42d3d37 --- /dev/null +++ b/package.yaml @@ -0,0 +1,45 @@ +name: mili +version: 0.1.0.0 +github: "marvinborner/mili" +license: MIT +author: "Marvin Borner" +maintainer: "develop@marvinborner.de" +copyright: "2024 Marvin Borner" + +extra-source-files: +- readme.md + +description: Please see the README on GitHub at <https://github.com/marvinborner/mili#readme> + +dependencies: +- base >= 4.7 && < 5 +- optparse-applicative +- megaparsec +- unordered-containers +- mtl +- text + +ghc-options: +- -Wall +- -Wcompat +- -Widentities +- -Wincomplete-record-updates +- -Wincomplete-uni-patterns +- -Wmissing-export-lists +- -Wmissing-home-modules +- -Wpartial-fields +- -Wredundant-constraints + +library: + source-dirs: src + +executables: + mili-exe: + main: Main.hs + source-dirs: app + ghc-options: + - -threaded + - -rtsopts + - -with-rtsopts=-N + dependencies: + - mili diff --git a/readme.md b/readme.md new file mode 100644 index 0000000..2ab9678 --- /dev/null +++ b/readme.md @@ -0,0 +1,12 @@ +# mili + +> Linear lambda calculus with linear types, de Bruijn levels and +> unbounded minimization + +Linear lambda calculus is a restricted version of the lambda calculus in +which every variable occurs exactly once. This typically implies linear +normalization and therefore Turing incompleteness. + +We extend the linear lambda calculus with bounded iteration and +unbounded minimization such that it barely becomes Turing complete, +while still benefitting from the advantages of syntactic linearity. diff --git a/samples/test.lil b/samples/test.lil new file mode 100644 index 0000000..e0ed6fd --- /dev/null +++ b/samples/test.lil @@ -0,0 +1,11 @@ +foo = [ + huh = [[[0 1 2]]] + huh 0 +] + +bar = [ + huh = ([[[0 2 1]]] 0) + huh 0 +] + +foo bar diff --git a/src/Data/Mili.hs b/src/Data/Mili.hs new file mode 100644 index 0000000..b407d00 --- /dev/null +++ b/src/Data/Mili.hs @@ -0,0 +1,13 @@ +module Data.Mili + ( Term(..) + ) where + +data Term = Abs Term -- | Abstraction + | App Term Term -- | Application + | Lvl Int -- | de Bruijn level + +instance Show Term where + showsPrec _ (Abs m) = showString "[" . shows m . showString "]" + showsPrec _ (App m n) = + showString "(" . shows m . showString " " . shows n . showString ")" + showsPrec _ (Lvl i) = shows i diff --git a/src/Language/Mili/Analyzer.hs b/src/Language/Mili/Analyzer.hs new file mode 100644 index 0000000..a85e990 --- /dev/null +++ b/src/Language/Mili/Analyzer.hs @@ -0,0 +1,76 @@ +module Language.Mili.Analyzer + ( linearity + ) where + +import Data.HashMap.Strict ( HashMap ) +import qualified Data.HashMap.Strict as M +import Data.List ( intercalate + , isSuffixOf + ) +import Data.Mili ( Term(..) ) + +-- | A trace specifies the exact path to any subterm +type Trace = [Breadcrumb] + +data Breadcrumb = South -- | Down into abstraction + | West -- | Left hand side of application + | East -- | Right hand side of application + deriving (Eq, Show) + +-- | Map abstractions to a hashmap such that de Bruijn levels correspond to traces +-- | of abstractions at that level +traceAbs :: Term -> HashMap Int [Trace] +traceAbs = go 0 [] + where + go n t (Abs m) = + M.unionWith (++) (go (n + 1) (South : t) m) (M.singleton n [t]) + go n t (App a b) = M.unionWith (++) (go n (West : t) a) (go n (East : t) b) + go _ _ (Lvl _ ) = M.empty + +-- | Map de Bruijn levels to a hashmap such that de Bruijn levels correspond to +-- | traces of de Bruijn levels at that level +traceLvl :: Term -> HashMap Int [Trace] +traceLvl = go [] + where + go t (Abs m ) = go (South : t) m + go t (App a b) = M.unionWith (++) (go (West : t) a) (go (East : t) b) + go t (Lvl l ) = M.singleton l [t] + +-- | Unify two two mapped traces to find levels at which the traces are no suffixes +-- | Level traces not being a suffix of abstraction traces implies nonlinearity +-- TODO: Proof? +unifyTraces :: HashMap Int [Trace] -> HashMap Int [Trace] -> HashMap Int [Bool] +unifyTraces traceA traceB = M.fromList $ map zipMap allKeys + where + allKeys = M.keys (traceA `M.union` traceB) + left key = M.lookupDefault [[]] key traceA + right key = M.lookupDefault [[]] key traceB + zipMap key + | length (left key) == length (right key) + = (key, zipWith isSuffixOf (left key) (right key)) + | otherwise + = (key, [False]) + +linearityError + :: HashMap Int [Trace] -> HashMap Int [Trace] -> HashMap Int [Bool] -> String +linearityError absTrace lvlTrace = pretty . filter (any not . snd) . M.toList + where + pretty = intercalate "\n" . map + (\(depth, _) -> + "Linearity divergence in depth " + <> show depth + <> "\n\t" + <> show (M.lookupDefault [[]] depth absTrace) + <> "\nvs\n\t" + <> show (M.lookupDefault [[]] depth lvlTrace) + ) + +linearity :: Term -> Either String Term +linearity t = + let absTrace = traceAbs t + lvlTrace = traceLvl t + unified = unifyTraces absTrace lvlTrace + isLinear = all (all id) unified + in if isLinear + then Right t + else Left $ linearityError absTrace lvlTrace unified diff --git a/src/Language/Mili/Parser.hs b/src/Language/Mili/Parser.hs new file mode 100644 index 0000000..bd61254 --- /dev/null +++ b/src/Language/Mili/Parser.hs @@ -0,0 +1,127 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Language.Mili.Parser + ( parseProgram + ) where + +import Control.Monad ( void ) +import Control.Monad.State +import Data.HashMap.Strict ( HashMap ) +import qualified Data.HashMap.Strict as M +import Data.Mili ( Term(..) ) +import Data.Text ( Text ) +import qualified Data.Text as T +import Data.Void +import Prelude hiding ( abs ) +import Text.Megaparsec hiding ( State ) +import Text.Megaparsec.Char +import qualified Text.Megaparsec.Char.Lexer as L + +type Parser = ParsecT Void Text (State ParserState) +data ParserState = PS + { _map :: HashMap Text Term + , _depth :: Int + } + +-- | single line comment +lineComment :: Parser () +lineComment = L.skipLineComment "--" + +-- | multiline comment +blockComment :: Parser () +blockComment = L.skipBlockComment "{-" "-}" + +parens :: Parser a -> Parser a +parens = between (symbol "(") (symbol ")") + +-- | space consumer including comments +spaceConsumer :: String -> Parser () +spaceConsumer s = L.space (void $ oneOf s) lineComment blockComment + +-- | multiple spaces with comments +spaces :: Parser () +spaces = spaceConsumer (" \t" :: String) + +-- | multiple spaces and newlines with comments +anySpaces :: Parser () +anySpaces = spaceConsumer (" \t\r\n" :: String) + +-- | arbitrary symbol consumer +symbol :: Text -> Parser Text +symbol = string + +-- | symbol consumer with arbitrary spaces behind +startSymbol :: Text -> Parser Text +startSymbol t = symbol t <* anySpaces + +-- | abstraction, entering increases the abstraction depth +-- TODO: There's a bug in here with open terms backtracking to increment lol +abs :: Parser Term +abs = between (startSymbol "[") (symbol "]") (Abs <$> (inc *> block <* dec)) + where + inc = modify $ \r@(PS { _depth = d }) -> r { _depth = d + 1 } + dec = modify $ \r@(PS { _depth = d }) -> r { _depth = d - 1 } + +-- | de Bruijn index, parsed to de Bruijn level +idx :: Parser Term +idx = do + n <- L.decimal + PS { _depth = d } <- get + case d - n - 1 of + i | i < 0 -> fail "open term" + | otherwise -> pure $ Lvl i + +-- | single identifier, directly parsed to corresponding term +def :: Parser Term +def = do + name <- identifier + PS { _map = names } <- get + case M.lookup name names of + Just t -> pure t + Nothing -> fail $ T.unpack name <> " is not in scope" + +-- | single lambda term, potentially a left application fold of many +term :: Parser Term +term = try chain <|> once + where + once = abs <|> idx <|> def <|> parens block + chain = foldl1 App <$> sepEndBy1 (try once) (char ' ') + +-- | single identifier, a-z +identifier :: Parser Text +identifier = T.pack <$> some lowerChar + +-- | single definition, <identifier> = <term> +definition :: Parser () +definition = do + name <- identifier + _ <- spaces + _ <- startSymbol "=" + _ <- spaces + body <- term + modify $ \r@(PS { _map = m }) -> r { _map = M.insert name body m } + +-- | many definitions, seperated by newline or semicolon +definitions :: Parser [()] +definitions = endBy (try definition) (oneOf (";\n" :: String) <* anySpaces) + +-- | single "let..in" block: many definitions before a single term +block :: Parser Term +block = do + (PS { _map = m }) <- get -- backup + b <- definitions *> term + _ <- anySpaces + modify $ \r -> r { _map = m } -- restore + pure b + +-- TODO: add preprocessor commands? +program :: Parser Term +program = block + +parseProgram :: Text -> Either String Term +parseProgram s = prettify $ evalState + (runParserT (anySpaces *> program <* anySpaces <* eof) "" s) + PS { _map = M.empty, _depth = 0 } + where + prettify (Right t ) = Right t + prettify (Left err) = Left $ errorBundlePretty err diff --git a/src/Language/Mili/Reducer.hs b/src/Language/Mili/Reducer.hs new file mode 100644 index 0000000..a65e018 --- /dev/null +++ b/src/Language/Mili/Reducer.hs @@ -0,0 +1,9 @@ +module Language.Mili.Reducer + ( nf + ) where + +import Data.Mili ( Term(..) ) + +-- | Reduce term to normal form +nf :: Term -> Term +nf m = m diff --git a/stack.yaml b/stack.yaml new file mode 100644 index 0000000..4854f5a --- /dev/null +++ b/stack.yaml @@ -0,0 +1,67 @@ +# This file was automatically generated by 'stack init' +# +# Some commonly used options have been documented as comments in this file. +# For advanced use and comprehensive documentation of the format, please see: +# https://docs.haskellstack.org/en/stable/yaml_configuration/ + +# A 'specific' Stackage snapshot or a compiler version. +# A snapshot resolver dictates the compiler version and the set of packages +# to be used for project dependencies. For example: +# +# snapshot: lts-22.28 +# snapshot: nightly-2024-07-05 +# snapshot: ghc-9.6.6 +# +# The location of a snapshot can be provided as a file or url. Stack assumes +# a snapshot provided as a file might change, whereas a url resource does not. +# +# snapshot: ./custom-snapshot.yaml +# snapshot: https://example.com/snapshots/2024-01-01.yaml +snapshot: + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/22/34.yaml + +# User packages to be built. +# Various formats can be used as shown in the example below. +# +# packages: +# - some-directory +# - https://example.com/foo/bar/baz-0.0.2.tar.gz +# subdirs: +# - auto-update +# - wai +packages: +- . +# Dependency packages to be pulled from upstream that are not in the snapshot. +# These entries can reference officially published versions as well as +# forks / in-progress versions pinned to a git hash. For example: +# +# extra-deps: +# - acme-missiles-0.3 +# - git: https://github.com/commercialhaskell/stack.git +# commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a +# +# extra-deps: [] + +# Override default flag values for project packages and extra-deps +# flags: {} + +# Extra package databases containing global packages +# extra-package-dbs: [] + +# Control whether we use the GHC we find on the path +# system-ghc: true +# +# Require a specific version of Stack, using version ranges +# require-stack-version: -any # Default +# require-stack-version: ">=3.1" +# +# Override the architecture used by Stack, especially useful on Windows +# arch: i386 +# arch: x86_64 +# +# Extra directories used by Stack for building +# extra-include-dirs: [/path/to/dir] +# extra-lib-dirs: [/path/to/dir] +# +# Allow a newer minor version of GHC than the snapshot specifies +# compiler-check: newer-minor diff --git a/stack.yaml.lock b/stack.yaml.lock new file mode 100644 index 0000000..e60110a --- /dev/null +++ b/stack.yaml.lock @@ -0,0 +1,13 @@ +# This file was autogenerated by Stack. +# You should not edit this file by hand. +# For more information, please see the documentation at: +# https://docs.haskellstack.org/en/stable/lock_files + +packages: [] +snapshots: +- completed: + sha256: edbd50d7e7c85c13ad5f5835ae2db92fab1e9cf05ecf85340e2622ec0a303df1 + size: 720020 + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/22/34.yaml + original: + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/22/34.yaml |