diff --git a/purescript/README.md b/purescript/README.md index aef2410..5d09b7a 100644 --- a/purescript/README.md +++ b/purescript/README.md @@ -10,9 +10,11 @@ | [existentials-blog](./existentials-blog) | Perhaps supposed to turn into a blog about existentials? | | [existentials](./existentials) | Experiment regarding the Church-encoding of existential types | | [gadts](./gadts) | Experiment regarding ways to encode GADTs in Purescript | +| [lambda-calculus](./lambda-calculus) | Lambda calculus evaluator | | [lune](./lune) | Failed effect-system project | | [maps](./maps) | Attempt at implementing maps with membership proofs | | [proofs](./proofs) | Attempt at expressing mathematical proofs using Purescript's effect system | +| [purebird](./purebird) | Flappy-bird game | | [purpleflow](./purpleflow) | Unfinished dependently-typed programming language | | [slice](./slice) | Basic benchmarks and a `Slice` type | | [sprint](./sprint) | Failled effect-system based on typelevel lists | diff --git a/purescript/lambda-calculus/.gitignore b/purescript/lambda-calculus/.gitignore new file mode 100644 index 0000000..39af3d6 --- /dev/null +++ b/purescript/lambda-calculus/.gitignore @@ -0,0 +1,11 @@ +/bower_components/ +/node_modules/ +/.pulp-cache/ +/output/ +/generated-docs/ +/.psc-package/ +/.psc* +/.purs* +/.psa* +/.spago +index.js diff --git a/purescript/lambda-calculus/packages.dhall b/purescript/lambda-calculus/packages.dhall new file mode 100644 index 0000000..9becfd7 --- /dev/null +++ b/purescript/lambda-calculus/packages.dhall @@ -0,0 +1,4 @@ +let upstream = + https://github.com/purescript/package-sets/releases/download/psc-0.14.1-20210516/packages.dhall sha256:f5e978371d4cdc4b916add9011021509c8d869f4c3f6d0d2694c0e03a85046c8 + +in upstream diff --git a/purescript/lambda-calculus/spago.dhall b/purescript/lambda-calculus/spago.dhall new file mode 100644 index 0000000..2899968 --- /dev/null +++ b/purescript/lambda-calculus/spago.dhall @@ -0,0 +1,30 @@ +{ name = "lc" +, dependencies = + [ "aff" + , "arrays" + , "console" + , "control" + , "effect" + , "either" + , "fixed-points" + , "foldable-traversable" + , "identity" + , "lists" + , "matryoshka" + , "maybe" + , "node-buffer" + , "node-process" + , "node-streams" + , "nonempty" + , "parsing" + , "prelude" + , "psci-support" + , "refs" + , "strings" + , "transformers" + , "tuples" + , "unordered-collections" + ] +, packages = ./packages.dhall +, sources = [ "src/**/*.purs", "test/**/*.purs" ] +} diff --git a/purescript/lambda-calculus/src/Main.purs b/purescript/lambda-calculus/src/Main.purs new file mode 100644 index 0000000..8e0dbdf --- /dev/null +++ b/purescript/lambda-calculus/src/Main.purs @@ -0,0 +1,272 @@ +module Main where + +import Prelude + +import Control.Alt ((<|>)) +import Control.Lazy (fix) +import Control.Monad.Reader (ask, local, runReader) +import Control.Plus (empty) +import Data.Array (reverse) +import Data.Array as Array +import Data.Array.NonEmpty (some) +import Data.Array.NonEmpty as NonEmptyArray +import Data.Either (Either(..)) +import Data.Foldable (foldl, foldlDefault) +import Data.Foldable as Foldable +import Data.Functor.Mu (Mu(..)) +import Data.HashMap as HashMap +import Data.Identity (Identity) +import Data.List (List(..), (:)) +import Data.Maybe (Maybe(..), fromMaybe, maybe) +import Data.NonEmpty (NonEmpty(..)) +import Data.String (joinWith) +import Data.Traversable (class Foldable, class Traversable, foldrDefault, traverseDefault) +import Data.Tuple.Nested ((/\)) +import Effect (Effect) +import Effect.Aff (Aff, effectCanceler, launchAff_, makeAff) +import Effect.Class.Console (logShow) +import Effect.Ref as Ref +import Matryoshka (class Corecursive, cata, embed, project) +import Node.Encoding (Encoding(..)) +import Node.Process (stdin) +import Node.Stream (Readable, onDataString, onEnd, onError, pause) +import Text.Parsing.Parser (ParseError, Parser, runParser) +import Text.Parsing.Parser.String (oneOf) +import Text.Parsing.Parser.Token (GenLanguageDef(..), GenTokenParser, LanguageDef, alphaNum, letter, makeTokenParser) + +readText :: forall w. Readable w -> Aff (Maybe String) +readText r = makeAff $ \res -> do + dataRef <- Ref.new "" + onDataString r UTF8 \chunk -> + Ref.modify_ (_ <> chunk) dataRef + onEnd r do + allData <- Ref.read dataRef + res $ Right (Just allData) + onError r $ Left >>> res + pure $ effectCanceler (pause r) + +main :: Effect Unit +main = launchAff_ do + text <- fromMaybe " " <$> readText stdin + case parseLambdaCalculus text of + Left err -> logShow err + Right ast -> logShow $ project $ reduce $ introduceDeBrujinIndices ast + + +---------- Types +data AstF v f + = Call f f + | Lambda String f + | Var v + +type Ast v = Mu (AstF v) + +data DeBrujin + = Bound Int String + | Free String + +derive instance functorAst :: Functor (AstF v) + +instance foldableAst :: Foldable (AstF v) where + foldMap f = case _ of + Call function argument -> f function <> f argument + Var _ -> mempty + Lambda _ body -> f body + + foldr f = foldrDefault f + foldl f = foldlDefault f + +instance traversableAst :: Traversable (AstF v) where + sequence = case _ of + Call f a -> Call <$> f <*> a + Lambda name body -> Lambda name <$> body + Var v -> pure $ Var v + + traverse = traverseDefault + +instance showAst :: Show (AstF DeBrujin (Ast DeBrujin)) where + show :: AstF DeBrujin (Ast DeBrujin) -> String + show = case _ of + Var (Free name) -> name + Var (Bound _ name) -> name + Call function argument + -> withParensIf (project function) needsParensLeft + <> " " + <> withParensIf (project argument) needsParensRight + Lambda name body -> showLambdas (name : Nil) (project body) + where + showLambdas names (Lambda name body) = showLambdas (name:names) (project body) + showLambdas Nil body = show body + showLambdas names body + = "\\" + <> joinWith " " (reverse $ Array.fromFoldable names) + <> ". " + <> show body + + withParensIf term predicate = if predicate term + then "(" <> show term <> ")" + else show term + + needsParensLeft = case _ of + Lambda _ _ -> true + _ -> false + + needsParensRight = case _ of + Call _ _ -> true + Lambda _ _ -> true + _ -> false + +data Error + = NotInScope Int String + +---------- Constructors +call :: forall t v. Corecursive t (AstF v) => t -> t -> t +call f a = embed (Call f a) + +var :: forall t v. Corecursive t (AstF v) => v -> t +var = Var >>> embed + +lambda :: forall t v. Corecursive t (AstF v) => String -> t -> t +lambda l t = embed (Lambda l t) + +---------- Reduction +introduceDeBrujinIndices :: Ast String -> Ast DeBrujin +introduceDeBrujinIndices i = cata go i # flip runReader HashMap.empty + where + go = case _ of + Var name -> ado + indices <- ask + in var $ maybe (Free name) (\index -> Bound index name) $ HashMap.lookup name indices + Call func arg -> call <$> func <*> arg + Lambda name body -> lambda name <$> local updateContext body + where + updateContext m = ((+) one <$> m) `HashMap.union` HashMap.singleton name zero + +betaReduction :: Ast DeBrujin -> Ast DeBrujin +betaReduction = cata case _ of + Var v -> var v + Call function argument -> do + case project function of + Lambda _ body -> betaReduction $ unshift $ substitute 0 (shift argument) body + _ -> call function argument + Lambda name body -> lambda name body + +etaReduction :: Ast DeBrujin -> Ast DeBrujin +etaReduction = cata case _ of + Var v -> var v + Call f a -> call f a + Lambda _ (In (Call term (In (Var (Bound 0 _))))) | not (occurs 0 term) -> unshift term + Lambda name l -> lambda name l + +substitute :: Int -> Ast DeBrujin -> Ast DeBrujin -> Ast DeBrujin +substitute at with within = cata go within # flip runReader (at /\ with) + where + go = case _ of + Call f a -> call <$> f <*> a + Var (Bound index name) -> ado + at' /\ with' <- ask + in if index == at' then with' else var (Bound index name) + Var v -> pure $ var v + Lambda name body -> lambda name <$> local updateContext body + where updateContext (at' /\ with') = (at' + 1) /\ shift with' + +shiftBy :: Int -> Ast DeBrujin -> Ast DeBrujin +shiftBy amount term = cata go term 0 + where + go = case _ of + Var (Bound index name) -> \over -> var $ flip Bound name if index < over then index else index + amount + Var v -> const $ var v + Call f a -> \over -> call (f over) (a over) + Lambda name body -> \over -> lambda name $ body (over + 1) + + +shift :: Ast DeBrujin -> Ast DeBrujin +shift = shiftBy 1 + +unshift :: Ast DeBrujin -> Ast DeBrujin +unshift = shiftBy (-1) + +occurs :: Int -> Ast DeBrujin -> Boolean +occurs = flip (cata go) + where + go = case _ of + Var (Bound index _) -> (==) index + Call f a -> f || a + Lambda _ body -> (+) 1 >>> body + _ -> const false + +reduce :: Ast DeBrujin -> Ast DeBrujin +reduce = betaReduction >>> etaReduction + +---------- Parser +-- | Punctuation to start the declaration of a lambda expression. +lambdaStarts :: Array String +lambdaStarts = [ "\\", "λ" ] + +-- | Punctuation to start the declaration of the body of a lambda expression. +lambdaBodyStarts :: Array String +lambdaBodyStarts = [ "->", "." ] + +-- | Declaration for lambda calculus (with comments). +-- | This is used to generate the lexer +language :: LanguageDef +language = + LanguageDef + { commentStart: "{-" + , commentEnd: "-}" + , commentLine: "--" + , nestedComments: true + , opStart: empty + , opLetter: empty + , caseSensitive: true + , reservedOpNames: lambdaStarts <> lambdaBodyStarts + , reservedNames: [] + , identStart: letter + , identLetter: alphaNum <|> oneOf [ '_', '\'' ] + } + +-- | The lexer +tokenParser :: GenTokenParser String Identity +tokenParser = makeTokenParser language + +-- | Parsers which run in the identity monad and parse strings +type LambdaParser r + = Parser String r + +-- | Parser for individual lambda calculus expressions. +-- | This references itself so we use it within a fixpoint operator +expression' :: LambdaParser (Ast String) -> LambdaParser (Ast String) +expression' expr = do + -- expression'' <- atom + (NonEmpty expression'' args) <- NonEmptyArray.toNonEmpty <$> some atom + pure $ foldl call expression'' args + where + { parens, identifier, reservedOp } = tokenParser + + atom :: LambdaParser (Ast String) + atom = wrapped <|> lambdaExpr <|> variable + + wrapped :: LambdaParser (Ast String) + wrapped = parens expr + + variable :: LambdaParser (Ast String) + variable = var <$> identifier + + lambdaExpr :: LambdaParser (Ast String) + lambdaExpr = do + Foldable.oneOf $ reservedOp <$> lambdaStarts + (NonEmpty arg args) <- NonEmptyArray.toNonEmpty <$> NonEmptyArray.reverse <$> some identifier + Foldable.oneOf $ reservedOp <$> lambdaBodyStarts + body <- expr + let + baseAst = lambda arg body + pure $ foldl (flip lambda) baseAst args + +-- | Parser for lambda calculus. +expression :: LambdaParser (Ast String) +expression = fix expression' + +-- | Try parsing a string into a lambda calculus ast. +parseLambdaCalculus :: String -> Either ParseError (Ast String) +parseLambdaCalculus = flip runParser expression + diff --git a/purescript/lambda-calculus/test/Main.purs b/purescript/lambda-calculus/test/Main.purs new file mode 100644 index 0000000..f91f98c --- /dev/null +++ b/purescript/lambda-calculus/test/Main.purs @@ -0,0 +1,11 @@ +module Test.Main where + +import Prelude + +import Effect (Effect) +import Effect.Class.Console (log) + +main :: Effect Unit +main = do + log "🍝" + log "You should add some tests."