From 42c1331809934f7e37c4f31904267f7aa356efea Mon Sep 17 00:00:00 2001 From: William Ball Date: Thu, 20 Jun 2024 14:31:39 -0700 Subject: [PATCH] untyped --- .gitignore | 2 + CHANGELOG.md | 11 ++++ LICENSE | 26 +++++++++ README.md | 1 + Setup.hs | 2 + app/Main.hs | 4 ++ lambda.cabal | 80 ++++++++++++++++++++++++++++ package.yaml | 63 ++++++++++++++++++++++ src/Lib.hs | 138 ++++++++++++++++++++++++++++++++++++++++++++++++ src/Parser.hs | 66 +++++++++++++++++++++++ stack.yaml | 67 +++++++++++++++++++++++ stack.yaml.lock | 13 +++++ test/Spec.hs | 2 + 13 files changed, 475 insertions(+) create mode 100644 .gitignore create mode 100644 CHANGELOG.md create mode 100644 LICENSE create mode 100644 README.md create mode 100644 Setup.hs create mode 100644 app/Main.hs create mode 100644 lambda.cabal create mode 100644 package.yaml create mode 100644 src/Lib.hs create mode 100644 src/Parser.hs create mode 100644 stack.yaml create mode 100644 stack.yaml.lock create mode 100644 test/Spec.hs 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/CHANGELOG.md b/CHANGELOG.md new file mode 100644 index 0000000..08478ca --- /dev/null +++ b/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 diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..9c707ba --- /dev/null +++ b/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. diff --git a/README.md b/README.md new file mode 100644 index 0000000..d69472b --- /dev/null +++ b/README.md @@ -0,0 +1 @@ +# lambda 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..12066fd --- /dev/null +++ b/app/Main.hs @@ -0,0 +1,4 @@ +module Main (main) where + +main :: IO () +main = putStrLn "Hello, world" diff --git a/lambda.cabal b/lambda.cabal new file mode 100644 index 0000000..c041bf7 --- /dev/null +++ b/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 +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 diff --git a/package.yaml b/package.yaml new file mode 100644 index 0000000..280555c --- /dev/null +++ b/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 + +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 diff --git a/src/Lib.hs b/src/Lib.hs new file mode 100644 index 0000000..5039abe --- /dev/null +++ b/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 diff --git a/src/Parser.hs b/src/Parser.hs new file mode 100644 index 0000000..a043719 --- /dev/null +++ b/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 diff --git a/stack.yaml b/stack.yaml new file mode 100644 index 0000000..18242db --- /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/ + +# 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 diff --git a/stack.yaml.lock b/stack.yaml.lock new file mode 100644 index 0000000..93e9db4 --- /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: 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 diff --git a/test/Spec.hs b/test/Spec.hs new file mode 100644 index 0000000..cd4753f --- /dev/null +++ b/test/Spec.hs @@ -0,0 +1,2 @@ +main :: IO () +main = putStrLn "Test suite not yet implemented"