untyped

.gitignore

@@ -0,0 +1,2 @@
+.stack-work/
+*~

CHANGELOG.md

@@ -0,0 +1,11 @@
+# Changelog for `lambda`
+
+All notable changes to this project will be documented in this file.
+
+The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
+and this project adheres to the
+[Haskell Package Versioning Policy](https://pvp.haskell.org/).
+
+## Unreleased
+
+## 0.1.0.0 - YYYY-MM-DD

LICENSE

@@ -0,0 +1,26 @@
+Copyright 2024 Author name here
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+1.  Redistributions of source code must retain the above copyright notice, this
+    list of conditions and the following disclaimer.
+
+2.  Redistributions in binary form must reproduce the above copyright notice,
+    this list of conditions and the following disclaimer in the documentation
+    and/or other materials provided with the distribution.
+
+3.  Neither the name of the copyright holder nor the names of its contributors
+    may be used to endorse or promote products derived from this software
+    without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

README.md

@@ -0,0 +1 @@
+# lambda

Setup.hs

@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain

app/Main.hs

@@ -0,0 +1,4 @@
+module Main (main) where
+
+main :: IO ()
+main = putStrLn "Hello, world"

lambda.cabal

@@ -0,0 +1,80 @@
+cabal-version: 2.2
+
+-- This file has been generated from package.yaml by hpack version 0.36.0.
+--
+-- see: https://github.com/sol/hpack
+
+name:           lambda
+version:        0.1.0.0
+description:    Please see the README on GitHub at <https://github.com/githubuser/lambda#readme>
+homepage:       https://github.com/githubuser/lambda#readme
+bug-reports:    https://github.com/githubuser/lambda/issues
+author:         Author name here
+maintainer:     example@example.com
+copyright:      2024 Author name here
+license:        BSD-3-Clause
+license-file:   LICENSE
+build-type:     Simple
+extra-source-files:
+    README.md
+    CHANGELOG.md
+
+source-repository head
+  type: git
+  location: https://github.com/githubuser/lambda
+
+library
+  exposed-modules:
+      Lib
+      Parser
+  other-modules:
+      Paths_lambda
+  autogen-modules:
+      Paths_lambda
+  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
+    , containers >=0.6
+    , megaparsec >=9.4
+    , prettyprinter >=1.7
+    , text >=2.0
+  default-language: Haskell2010
+
+executable lambda-exe
+  main-is: Main.hs
+  other-modules:
+      Paths_lambda
+  autogen-modules:
+      Paths_lambda
+  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
+    , containers >=0.6
+    , lambda
+    , megaparsec >=9.4
+    , prettyprinter >=1.7
+    , text >=2.0
+  default-language: Haskell2010
+
+test-suite lambda-test
+  type: exitcode-stdio-1.0
+  main-is: Spec.hs
+  other-modules:
+      Paths_lambda
+  autogen-modules:
+      Paths_lambda
+  hs-source-dirs:
+      test
+  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
+    , containers >=0.6
+    , lambda
+    , megaparsec >=9.4
+    , prettyprinter >=1.7
+    , text >=2.0
+  default-language: Haskell2010

package.yaml

@@ -0,0 +1,63 @@
+name:                lambda
+version:             0.1.0.0
+github:              "githubuser/lambda"
+license:             BSD-3-Clause
+author:              "Author name here"
+maintainer:          "example@example.com"
+copyright:           "2024 Author name here"
+
+extra-source-files:
+- README.md
+- CHANGELOG.md
+
+# Metadata used when publishing your package
+# synopsis:            Short description of your package
+# category:            Web
+
+# To avoid duplicated efforts in documentation and dealing with the
+# complications of embedding Haddock markup inside cabal files, it is
+# common to point users to the README.md file.
+description:         Please see the README on GitHub at <https://github.com/githubuser/lambda#readme>
+
+dependencies:
+- base >= 4.7 && < 5
+- megaparsec >= 9.4
+- text >= 2.0
+- prettyprinter >= 1.7
+- containers >= 0.6
+
+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:
+  lambda-exe:
+    main:                Main.hs
+    source-dirs:         app
+    ghc-options:
+    - -threaded
+    - -rtsopts
+    - -with-rtsopts=-N
+    dependencies:
+    - lambda
+
+tests:
+  lambda-test:
+    main:                Spec.hs
+    source-dirs:         test
+    ghc-options:
+    - -threaded
+    - -rtsopts
+    - -with-rtsopts=-N
+    dependencies:
+    - lambda

src/Lib.hs

@@ -0,0 +1,138 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# OPTIONS_GHC -Wno-missing-export-lists #-}
+
+module Lib where
+
+import Control.Monad (join)
+import Data.Function (on)
+import Data.List (elemIndex, find)
+import Data.Maybe (fromJust)
+import qualified Data.Set as Set
+import Prettyprinter (Pretty (..), hsep, parens, (<+>))
+
+type Var = String
+
+type Name = String
+
+data Term = Var !Var | App !Term !Term | Abs !Var !Term
+
+data DBTerm = DBFree !Name | DBVar !Int | DBApp !DBTerm !DBTerm | DBAbs !DBTerm deriving (Eq, Show)
+
+instance (Pretty Term) where
+  pretty (Var x) = pretty x
+  pretty (App t@(Abs _ _) s@(Abs _ _)) =
+    parens (pretty t) <+> parens (pretty s)
+  pretty (App t@(Abs _ _) s) =
+    parens (pretty t) <+> pretty s
+  pretty (App s t@(Abs _ _)) =
+    pretty s <+> parens (pretty t)
+  pretty (App s t@(App _ _)) =
+    pretty s <+> parens (pretty t)
+  pretty (App s t) = pretty s <+> pretty t
+  pretty t@(Abs _ _) =
+    let (vs, body) = getCurriedVars t
+     in "λ" <> hsep (pretty <$> vs) <> "." <+> pretty body
+
+instance (Show Term) where
+  show = show . pretty
+
+(<.>) :: Term -> Term -> Term
+(<.>) = App
+
+getCurriedVars :: Term -> ([Var], Term)
+getCurriedVars (Abs x t) =
+  let (vs, body) = getCurriedVars t
+   in (x : vs, body)
+getCurriedVars t = ([], t)
+
+subterms :: Term -> [Term]
+subterms t@(Var _) = [t]
+subterms t@(App m n) = t : subterms m ++ subterms n
+subterms t@(Abs _ m) = t : subterms m
+
+freeVars :: Term -> Set.Set Var
+freeVars (Var x) = Set.singleton x
+freeVars (App m n) = on Set.union freeVars m n
+freeVars (Abs x m) = Set.delete x $ freeVars m
+
+bindingVars :: Term -> Set.Set Var
+bindingVars (Var _) = Set.empty
+bindingVars (App m n) = on Set.union bindingVars m n
+bindingVars (Abs x m) = Set.insert x $ bindingVars m
+
+allVars :: Term -> Set.Set Var
+allVars = liftA2 Set.union freeVars bindingVars
+
+freeIn :: Var -> Term -> Bool
+freeIn = (. freeVars) . Set.member
+
+bindingIn :: Var -> Term -> Bool
+bindingIn = (. bindingVars) . Set.member
+
+freeOrBindingIn :: Var -> Term -> Bool
+freeOrBindingIn = join . on (||) . freeIn
+
+isCombinator :: Term -> Bool
+isCombinator = Set.null . freeVars
+
+alphaConv :: Var -> Var -> Term -> Term
+alphaConv _ _ t@(Var _) = t
+alphaConv _ _ t@(App _ _) = t
+alphaConv x y s@(Abs x' t) =
+  if y `freeIn` t || x /= x'
+    then s
+    else maybe s (Abs y) (alphaConv' t)
+  where
+    alphaConv' (Var x'') = if x == x'' then Just (Var y) else Just (Var x'')
+    alphaConv' (App m n) = App <$> alphaConv' m <*> alphaConv' n
+    alphaConv' t'@(Abs y' m)
+      | y == y' = Nothing
+      | x == y' = Just t'
+      | otherwise = Abs y' <$> alphaConv' m
+
+vars :: [Var]
+vars = ["x", "y", "z", "w", "u", "v"] ++ map ("x" <>) (show <$> [1 :: Integer ..])
+
+genNewVar :: Set.Set Var -> Var
+genNewVar vs = fromJust $ find (not . (`Set.member` vs)) vars
+
+subst :: Var -> Term -> Term -> Term
+subst x n m@(Var x') = if x == x' then n else m
+subst x n (App p q) = on App (subst x n) p q
+subst x n m@(Abs y p)
+  | y `freeIn` n = subst x n $ alphaConv y z m
+  | x == y = m
+  | otherwise = Abs y $ subst x n p
+  where
+    z = genNewVar $ on Set.union freeVars n p
+
+betaReduce :: Term -> Term
+betaReduce (Var x) = Var x
+betaReduce (Abs x m) = Abs x (betaReduce m)
+betaReduce (App (Abs x m) n) = subst x n m
+betaReduce (App m n) = on App betaReduce m n
+
+betaNf :: Term -> Bool
+betaNf (Var _) = True
+betaNf (App (Abs _ _) _) = False
+betaNf (App m n) = on (&&) betaNf m n
+betaNf (Abs _ m) = betaNf m
+
+findBetaNf :: Term -> Term
+findBetaNf = fromJust . find betaNf . iterate betaReduce
+
+findBetaNf' :: Term -> Term
+findBetaNf' t =
+  if betaNf t
+    then t
+    else findBetaNf' $ betaReduce t
+
+alphaEquiv :: Term -> Term -> Bool
+alphaEquiv = on (==) debruijnize
+
+debruijnize :: Term -> DBTerm
+debruijnize = helper []
+  where
+    helper vs (Var x) = maybe (DBFree x) DBVar $ elemIndex x vs
+    helper vs (App m n) = on DBApp (helper vs) m n
+    helper vs (Abs x m) = DBAbs $ helper (x : vs) m

src/Parser.hs

@@ -0,0 +1,66 @@
+{-# OPTIONS_GHC -Wno-missing-export-lists #-}
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+
+module Parser where
+
+import Control.Monad (void)
+import Data.Bifunctor (first)
+import Data.Void (Void)
+import Lib (Term (..))
+import Text.Megaparsec
+import Text.Megaparsec.Char
+import qualified Text.Megaparsec.Char.Lexer as L
+
+type Parser = Parsec Void String
+
+skipSpace :: Parser ()
+skipSpace =
+    L.space
+        space1
+        (L.skipLineComment "--")
+        (L.skipBlockCommentNested "(*" "*)")
+
+lexeme :: Parser a -> Parser a
+lexeme = L.lexeme skipSpace
+
+pVar :: Parser String
+pVar = label "variable" $ lexeme $ do
+    firstChar <- letterChar <|> char '_'
+    rest <- many $ alphaNumChar <|> char '_'
+    return $ firstChar : rest
+
+pLambda :: Parser ()
+pLambda = lexeme $ label "λ" $ void $ string "lambda" <|> string "λ"
+
+pAbs :: Parser Term
+pAbs = lexeme $ label "abstraction" $ do
+    vars <- between pLambda pDot (many pVar)
+    body <- pExpr
+    return $ foldr Abs body vars
+
+pApp :: Parser Term
+pApp = foldl1 App <$> some pTerm
+
+pDot :: Parser ()
+pDot = lexeme $ label "." $ void $ char '.'
+
+pTerm :: Parser Term
+pTerm =
+    lexeme $
+        label "term" $
+            choice
+                [ between (char '(') (char ')') pExpr
+                , Var <$> pVar
+                ]
+
+pExpr :: Parser Term
+pExpr = lexeme $ pAbs <|> pApp
+
+pAll :: String -> Either String Term
+pAll = first errorBundlePretty . parse (between skipSpace eof pExpr) ""
+
+unwrap :: Either a b -> b
+unwrap (Right x) = x
+
+p :: String -> Term
+p = unwrap . pAll

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/
+
+# Resolver to choose 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:
+#
+# resolver: lts-22.7
+# resolver: nightly-2024-01-20
+# resolver: ghc-9.6.4
+#
+# 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.
+#
+# resolver: ./custom-snapshot.yaml
+# resolver: https://example.com/snapshots/2023-01-01.yaml
+resolver:
+  url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/22/26.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 resolver.
+# 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 local 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: ">=2.15"
+#
+# 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

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: 8e7996960d864443a66eb4105338bbdd6830377b9f6f99cd5527ef73c10c01e7
+    size: 719128
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/22/26.yaml
+  original:
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/22/26.yaml

test/Spec.hs

@@ -0,0 +1,2 @@
+main :: IO ()
+main = putStrLn "Test suite not yet implemented"