diff --git a/README.md b/README.md index 1d72a0f..cfe570d 100644 --- a/README.md +++ b/README.md @@ -1,33 +1,59 @@ -# Lambda Calculus -This is a simple programming language derived from lambda calculus, -using the Hindley-Milner type system, plus `letrec` and `callcc`. +# The Ivo Programming Language +Ivo (IPA: /aɪvoʊ/) is a programming language intended +as a tool for its author to explore interesting programming language features. -## Usage -Run the program using `stack run` (or run the tests with `stack test`). +Ivo is currently in a very early stage of development +and most likely is not of any practical or academic interest; +however, that may change in the future. +This README serves to document the language as it currently stands, +not what the language one day hopes to be. -Type in your expression at the prompt: `>> `. -Yourexpression will be evaluated to normal form using the call-by-value evaluation strategy and then printed. +## Using the Ivo interpreter +You may run the Ivo interpreter using `stack run`; +the interpreter does not take any arguments. + +Type in your command, definition, or expression at the prompt: `>> `. +Expressions will be typechecked, evaluated using call-by-value, and then printed. Exit the prompt with `Ctrl-d` (or equivalent). -## Commands -Instead of entering an expression in the REPL, you may enter a command. +### Interpreter commands These commands are available: -* `:load `: Execute a program in the interpreter, importing all definitions. * `:clear`: Clear all of your variable definitions. + +* `:load `: + + Execute a file containing Ivo definitions and expressions in the interpreter. + Variables already defined in the interpreter will be defined in the file; + variables defined by the file will be defined in the interpreter. + + The filename may contain spaces, but trailing whitespace will be trimmed. + * `:check `: - * If the first argument is `off`, then expressions will be evaluated even if they do not typecheck. - * If the second argument is `always`, inferred types will always be printed. - If it is `decls`, then only declarations will have their inferred types printed. - Otherwise, the type of expressions is never printed. + + * If the first argument is `on`, + then expressions will only be evaluated and definitions will only be added + only if typechecking succeeds. + + * If the second argument is `always`, then inferred types will always be printed; + if it is `decls`, then only the inferred types of declarations will be printed; + otherwise, the type of expressions are never printed.' + * The default values are `on` `decls`. + * `:trace `: - * If the argument is `local`, intermediate expressions will be printed as the evaluator evaluates them. - * If the argument is `global`, the *entire* expression will be printed each evaluator step. + + * If the argument is `local`, intermediate expressions will be printed + as they are evaluated; + + * If the argument is `global`, the *entire* expression will be printed + with each evaluation step. + * The default value is `off`. -## Syntax +## The Ivo language +### Syntax The parser's error messages currently are virtually useless, so be very careful with your syntax. * Variable names: any sequence of letters. @@ -55,7 +81,7 @@ allow declarations (`let(rec) x = E` without multiple definitions `in ...`), which make your definitions available for the rest of the program's execution. You must separate your declarations and expressions with `;`. -## Types +### Types Types are checked/inferred using the Hindley-Milner type inference algorithm. * Functions: `a -> b` (constructed by `\x. e`) @@ -68,18 +94,19 @@ Types are checked/inferred using the Hindley-Milner type inference algorithm. * Characters: `Char` (constructed by `Char`, which takes a `Nat`) * Universal quantification (forall): `∀a b. t` -## Builtins +### Builtins Builtins are variables that correspond with a built-in language feature that cannot be replicated by user-written code. They still are just variables though; they do not receive special syntactic treatment. -* `callcc : ∀a b. (((a -> b) -> a) -> a)`: [the call-with-current-continuation control flow operator](https://en.wikipedia.org/wiki/Call-with-current-continuation). +* `callcc : ∀a b. (((a -> b) -> a) -> a)`: + [the call-with-current-continuation control flow operator](https://en.wikipedia.org/wiki/Call-with-current-continuation). Continuations are printed as `λ!. ... ! ...`, like a lambda abstraction with an argument named `!` which is used exactly once; however, continuations are *not* the same as lambda abstractions because they perform the side effect of modifying the current continuation, -and this is *not* valid syntax you can input into the REPL. +and this is *not* valid syntax you can enter into the REPL. -## Example code -You can see some example code in `examples.lc`. +### Example code +You can see some example code in `examples/examples.ivo`. diff --git a/app/Main.hs b/app/Main.hs index a2435d0..042a9ce 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -1,6 +1,6 @@ module Main (main) where -import LambdaCalculus +import Ivo import Control.Exception (IOException, catch) import Data.Maybe (isJust) diff --git a/examples.lc b/examples/examples.ivo similarity index 100% rename from examples.lc rename to examples/examples.ivo diff --git a/package.yaml b/package.yaml index c6e991b..9569ebd 100644 --- a/package.yaml +++ b/package.yaml @@ -1,13 +1,13 @@ -name: jtm-lambda-calculus +name: ivo version: 0.1.0.0 -github: "jamestmartin/lambda-calculus" +github: "ivolang/ivo" license: GPL-3 author: "James Martin" maintainer: "james@jtmar.me" -copyright: "2019-2020 James Martin" -synopsis: "A simple implementation of the lambda calculus." -category: LambdaCalculus -description: Please see the README on GitHub at +copyright: "2019-2021 James Martin" +synopsis: "A useless programming language for useless people." +category: Language +description: Please see the README on GitHub at extra-source-files: - README.md @@ -63,7 +63,7 @@ library: - -Wno-missing-import-lists executables: - jtm-lambda-calculus: + ivo: main: Main.hs source-dirs: app ghc-options: @@ -75,12 +75,12 @@ executables: - -Wno-monomorphism-restriction - -Wno-unused-do-bind dependencies: - - jtm-lambda-calculus + - ivo - exceptions >= 0.10.4 && < 0.11 - haskeline >= 0.8 && < 1 tests: - jtm-lambda-calculus-test: + ivo-test: main: Spec.hs source-dirs: test ghc-options: @@ -89,6 +89,6 @@ tests: - -rtsopts - -with-rtsopts=-N dependencies: - - jtm-lambda-calculus + - ivo - tasty >= 1.2 && < 2 - tasty-hunit >= 0.10 && < 0.11 diff --git a/src/LambdaCalculus.hs b/src/Ivo.hs similarity index 58% rename from src/LambdaCalculus.hs rename to src/Ivo.hs index e11a9e1..d3ed975 100644 --- a/src/LambdaCalculus.hs +++ b/src/Ivo.hs @@ -1,15 +1,15 @@ -module LambdaCalculus - ( module LambdaCalculus.Evaluator - , module LambdaCalculus.Expression - , module LambdaCalculus.Syntax - , module LambdaCalculus.Types +module Ivo + ( module Ivo.Evaluator + , module Ivo.Expression + , module Ivo.Syntax + , module Ivo.Types , parseCheck, parseEval, unparseCheck, unparseEval ) where -import LambdaCalculus.Evaluator -import LambdaCalculus.Expression -import LambdaCalculus.Syntax -import LambdaCalculus.Types +import Ivo.Evaluator +import Ivo.Expression +import Ivo.Syntax +import Ivo.Types parseCheck :: Text -> Either ParseError CheckExpr parseCheck = fmap ast2check . parseAST diff --git a/src/LambdaCalculus/Evaluator.hs b/src/Ivo/Evaluator.hs similarity index 97% rename from src/LambdaCalculus/Evaluator.hs rename to src/Ivo/Evaluator.hs index 9b4ef2c..54367ec 100644 --- a/src/LambdaCalculus/Evaluator.hs +++ b/src/Ivo/Evaluator.hs @@ -1,4 +1,4 @@ -module LambdaCalculus.Evaluator +module Ivo.Evaluator ( Expr (..), Ctr (..), Pat, ExprF (..), PatF (..), VoidF, UnitF (..), Text , Eval, EvalExpr, EvalX, EvalXF (..) , pattern AppFE, pattern CtrE, pattern CtrFE @@ -6,8 +6,8 @@ module LambdaCalculus.Evaluator , eval, evalTrace, evalTraceGlobal ) where -import LambdaCalculus.Evaluator.Base -import LambdaCalculus.Evaluator.Continuation +import Ivo.Evaluator.Base +import Ivo.Evaluator.Continuation import Control.Monad.Except (MonadError, ExceptT, throwError, runExceptT) import Control.Monad.Loops (iterateM_) diff --git a/src/LambdaCalculus/Evaluator/Base.hs b/src/Ivo/Evaluator/Base.hs similarity index 97% rename from src/LambdaCalculus/Evaluator/Base.hs rename to src/Ivo/Evaluator/Base.hs index 111dff6..d814d63 100644 --- a/src/LambdaCalculus/Evaluator/Base.hs +++ b/src/Ivo/Evaluator/Base.hs @@ -1,4 +1,4 @@ -module LambdaCalculus.Evaluator.Base +module Ivo.Evaluator.Base ( Identity (..) , Expr (..), Ctr (..), Pat, ExprF (..), PatF (..), VoidF, UnitF (..), Text , substitute, substitute1, rename, rename1, free, bound, used @@ -7,7 +7,7 @@ module LambdaCalculus.Evaluator.Base , pattern ContE, pattern ContFE, pattern CallCCE, pattern CallCCFE ) where -import LambdaCalculus.Expression.Base +import Ivo.Expression.Base import Control.Monad (forM) import Control.Monad.Reader (asks) diff --git a/src/LambdaCalculus/Evaluator/Continuation.hs b/src/Ivo/Evaluator/Continuation.hs similarity index 89% rename from src/LambdaCalculus/Evaluator/Continuation.hs rename to src/Ivo/Evaluator/Continuation.hs index fa77e8a..bf22ceb 100644 --- a/src/LambdaCalculus/Evaluator/Continuation.hs +++ b/src/Ivo/Evaluator/Continuation.hs @@ -1,9 +1,9 @@ -module LambdaCalculus.Evaluator.Continuation +module Ivo.Evaluator.Continuation ( Continuation, continue, continue1 , ContinuationCrumb (..) ) where -import LambdaCalculus.Evaluator.Base +import Ivo.Evaluator.Base import Data.List (foldl') diff --git a/src/LambdaCalculus/Expression.hs b/src/Ivo/Expression.hs similarity index 96% rename from src/LambdaCalculus/Expression.hs rename to src/Ivo/Expression.hs index b2524fa..08c3baf 100644 --- a/src/LambdaCalculus/Expression.hs +++ b/src/Ivo/Expression.hs @@ -1,4 +1,4 @@ -module LambdaCalculus.Expression +module Ivo.Expression ( Expr (..), Ctr (..), Pat, ExprF (..), PatF (..), DefF (..), VoidF, UnitF (..), Text , substitute, substitute1, rename, free, bound, used , Eval, EvalExpr, EvalX, EvalXF (..), Identity (..) @@ -15,9 +15,9 @@ module LambdaCalculus.Expression , builtins ) where -import LambdaCalculus.Evaluator.Base -import LambdaCalculus.Syntax.Base -import LambdaCalculus.Types.Base +import Ivo.Evaluator.Base +import Ivo.Syntax.Base +import Ivo.Types.Base import Data.Functor.Foldable (cata, hoist) import Data.HashMap.Strict (HashMap) diff --git a/src/LambdaCalculus/Expression/Base.hs b/src/Ivo/Expression/Base.hs similarity index 99% rename from src/LambdaCalculus/Expression/Base.hs rename to src/Ivo/Expression/Base.hs index 62ea39f..34f1cb2 100644 --- a/src/LambdaCalculus/Expression/Base.hs +++ b/src/Ivo/Expression/Base.hs @@ -1,6 +1,6 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE UndecidableInstances #-} -module LambdaCalculus.Expression.Base +module Ivo.Expression.Base ( Text, VoidF, UnitF (..), absurd' , Expr (..), Ctr (..), Pat, Def, AppArgs, AbsArgs, LetArgs, CtrArgs, XExpr , ExprF (..), PatF (..), DefF (..), AppArgsF, LetArgsF, CtrArgsF, XExprF diff --git a/src/Ivo/Syntax.hs b/src/Ivo/Syntax.hs new file mode 100644 index 0000000..763c20a --- /dev/null +++ b/src/Ivo/Syntax.hs @@ -0,0 +1,7 @@ +module Ivo.Syntax + ( module Ivo.Syntax.Parser + , module Ivo.Syntax.Printer + ) where + +import Ivo.Syntax.Parser +import Ivo.Syntax.Printer diff --git a/src/LambdaCalculus/Syntax/Base.hs b/src/Ivo/Syntax/Base.hs similarity index 98% rename from src/LambdaCalculus/Syntax/Base.hs rename to src/Ivo/Syntax/Base.hs index 039b899..011edbd 100644 --- a/src/LambdaCalculus/Syntax/Base.hs +++ b/src/Ivo/Syntax/Base.hs @@ -1,4 +1,4 @@ -module LambdaCalculus.Syntax.Base +module Ivo.Syntax.Base ( Expr (..), ExprF (..), Ctr (..), Pat, Def, DefF (..), PatF (..), VoidF, Text, NonEmpty (..) , substitute, substitute1, rename, rename1, free, bound, used , Parse, AST, ASTF, ASTX, ASTXF (..), NonEmptyDefFs (..) @@ -8,7 +8,7 @@ module LambdaCalculus.Syntax.Base , simplify ) where -import LambdaCalculus.Expression.Base +import Ivo.Expression.Base import Data.Functor.Foldable (embed, project) import Data.List.NonEmpty (NonEmpty (..), toList) diff --git a/src/LambdaCalculus/Syntax/Parser.hs b/src/Ivo/Syntax/Parser.hs similarity index 98% rename from src/LambdaCalculus/Syntax/Parser.hs rename to src/Ivo/Syntax/Parser.hs index dc029ce..1be06c1 100644 --- a/src/LambdaCalculus/Syntax/Parser.hs +++ b/src/Ivo/Syntax/Parser.hs @@ -1,11 +1,11 @@ -module LambdaCalculus.Syntax.Parser +module Ivo.Syntax.Parser ( ParseError, parse , DeclOrExprAST, ProgramAST , parseAST, parseDeclOrExpr, parseProgram , astParser, declOrExprParser, programParser ) where -import LambdaCalculus.Syntax.Base +import Ivo.Syntax.Base import Data.List.NonEmpty (fromList) import Data.Text qualified as T diff --git a/src/LambdaCalculus/Syntax/Printer.hs b/src/Ivo/Syntax/Printer.hs similarity index 97% rename from src/LambdaCalculus/Syntax/Printer.hs rename to src/Ivo/Syntax/Printer.hs index 6742943..850a2c2 100644 --- a/src/LambdaCalculus/Syntax/Printer.hs +++ b/src/Ivo/Syntax/Printer.hs @@ -1,6 +1,6 @@ -module LambdaCalculus.Syntax.Printer (unparseAST) where +module Ivo.Syntax.Printer (unparseAST) where -import LambdaCalculus.Syntax.Base +import Ivo.Syntax.Base import Data.Functor.Base (NonEmptyF (NonEmptyF)) import Data.Functor.Foldable (cata) diff --git a/src/LambdaCalculus/Types.hs b/src/Ivo/Types.hs similarity index 98% rename from src/LambdaCalculus/Types.hs rename to src/Ivo/Types.hs index 97bacd0..65fa19c 100644 --- a/src/LambdaCalculus/Types.hs +++ b/src/Ivo/Types.hs @@ -1,9 +1,9 @@ -module LambdaCalculus.Types - ( module LambdaCalculus.Types.Base +module Ivo.Types + ( module Ivo.Types.Base , infer ) where -import LambdaCalculus.Types.Base +import Ivo.Types.Base import Control.Applicative ((<|>)) import Control.Monad (when) diff --git a/src/LambdaCalculus/Types/Base.hs b/src/Ivo/Types/Base.hs similarity index 99% rename from src/LambdaCalculus/Types/Base.hs rename to src/Ivo/Types/Base.hs index 91f2494..1eb426d 100644 --- a/src/LambdaCalculus/Types/Base.hs +++ b/src/Ivo/Types/Base.hs @@ -1,5 +1,5 @@ {-# LANGUAGE TemplateHaskell #-} -module LambdaCalculus.Types.Base +module Ivo.Types.Base ( Identity (..) , Expr (..), Ctr (..), Pat, ExprF (..), PatF (..), VoidF, UnitF (..), Text , substitute, substitute1, rename, rename1, free, bound, used @@ -24,7 +24,7 @@ import Data.HashMap.Strict qualified as HM import Data.List (foldl1') import Data.Text qualified as T import Data.Traversable (for) -import LambdaCalculus.Expression.Base +import Ivo.Expression.Base data Check type CheckExpr = Expr Check diff --git a/src/LambdaCalculus/Syntax.hs b/src/LambdaCalculus/Syntax.hs deleted file mode 100644 index 3304d05..0000000 --- a/src/LambdaCalculus/Syntax.hs +++ /dev/null @@ -1,7 +0,0 @@ -module LambdaCalculus.Syntax - ( module LambdaCalculus.Syntax.Parser - , module LambdaCalculus.Syntax.Printer - ) where - -import LambdaCalculus.Syntax.Parser -import LambdaCalculus.Syntax.Printer diff --git a/test/Spec.hs b/test/Spec.hs index cc30b39..2786c80 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -1,4 +1,4 @@ -import LambdaCalculus +import Ivo import Test.Tasty import Test.Tasty.HUnit