https://github.com/EvolveYourMind/ts-lambda-calc

Skip to content
 
Sign up

  * Why GitHub?
      + Features
      + Mobile
      + Actions
      + Codespaces
      + Packages
      + Security
      + Code review
      + Issues
      + Integrations
      + GitHub Sponsors
      + Customer stories
  * Team
  * Enterprise
  * Explore
      + Explore GitHub
      + Learn and contribute
      + Topics
      + Collections
      + Trending
      + Learning Lab
      + Open source guides
      + Connect with others
      + The ReadME Project
      + Events
      + Community forum
      + GitHub Education
      + GitHub Stars program
  * Marketplace
  * Pricing
      + Plans
      + Compare plans
      + Contact Sales
      + Education

[                    ] 

  *  
    #
    In this repository All GitHub |
    Jump to |

  * No suggested jump to results

  *  
    #
    In this repository All GitHub |
    Jump to |
  *  
    #
    In this user All GitHub |
    Jump to |
  *  
    #
    In this repository All GitHub |
    Jump to |

Sign in
Sign up
{{ message }}

EvolveYourMind / ts-lambda-calc Public

  * Notifications
  * Fork 0
  * Star 1
  * 

Lambda Calculus at compile time in TypeScript. TS's type-system is
Turing-complete

1 star 0 forks
Star
Notifications

  * Code
  * Issues 0
  * Pull requests 0
  * Actions
  * Projects 0
  * Wiki
  * Security
  * Insights

More

  * Code
  * Issues
  * Pull requests
  * Actions
  * Projects
  * Wiki
  * Security
  * Insights

master
Switch branches/tags
[                    ]
Branches Tags
Could not load branches
Nothing to show
{{ refName }} default View all branches
Could not load tags
Nothing to show
{{ refName }} default
View all tags
1 branch 0 tags
Code

Latest commit

@EvolveYourMind
EvolveYourMind Update readme
...
c6e187b Dec 15, 2021
Update readme
c6e187b

Git stats

  * 13 commits

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
.gitignore
Init core
Dec 12, 2021
Demo.ts
Add demo
Dec 15, 2021
Equality.ts
Init core
Dec 12, 2021
Fact.ts
Add factorial
Dec 15, 2021
Lang.ts
Init core
Dec 12, 2021
Parser.ts
Improve parser
Dec 15, 2021
README.md
Update readme
Dec 15, 2021
Semantics.ts
Reformat
Dec 15, 2021
package.json
Init core
Dec 12, 2021
tsconfig.json
Init core
Dec 12, 2021
yarn.lock
Init core
Dec 12, 2021
View code
ts-lambda-calc Examples Intro Arithmetics Factorial and limitations

README.md

 ts-lambda-calc

Lambda calculus at type-level with TypeScript.

The project includes:

  * a parser which transforms raw strings representing lambda
    expressions into an ASTs
  * an evaluator which reduces ASTs
  * a stringifyier which transforms an AST back into a string

Try it out in the TypeScript Playground!

 Examples

 Intro

When parsing the string (lx.x) y,

  * the parser produces App<Func<Var<"x">, "x">, Var<"y">>
  * the evaluator derives Var<"y">
  * the stringifier produces y:

import { Parse, } from "./Parser"
import { Eval, Stringify } from "./Semantics"
type raw = `(lx.x) y`
type parsed = Parse<raw>
type evaluated = Eval<parsed>
type stringified = Stringify<evaluated>

 Arithmetics

The following example shows simple arithmetic operations with Church
Encoding:

type ZERO = "(lf.(lx.x))"
type SUCC = "(la.(lf.(lx.(a f) (f x))))"
type ADD = `(la.(lb.(b ${SUCC} a)))`

type zero = Parse<ZERO>
type succ = Parse<SUCC>
type one = Parse<`${SUCC} ${ZERO}`>
type two = Parse<`${SUCC} (${SUCC} ${ZERO})`>

type rawOne = Stringify<one> // ((la.(lf.(lx.((a f) (f x))))) (lf.(lx.x)))

type rawTwo = Stringify<two> // ( 
                             //  (la.(lf.(lx.((a f) (f x))))) 
                             //   ((la.(lf.(lx.((a f) (f x))))) (lf.(lx.x)))
                             // )

type evalZero = Stringify<Eval<zero>>  // (lf.(lx.x))
type evalOne = Stringify<Eval<one>>  // (lf.(lx.(f x)))
type evalTwo = Stringify<Eval<two>>  // (lf.(lx.(f (f x))))

// 3 + 2 = 5
type parsed = Parse<`${ADD} (${SUCC} (${SUCC} (${SUCC} ${ZERO}))) (${SUCC} (${SUCC} ${ZERO}))`>
type rawParsed = Stringify<parsed> // (((la.(lb.((b (la.(lf.(lx.((a f) (f x)))))) a))) 
                                   // ((la.(lf.(lx.((a f) (f x))))) 
                                   //   ((la.(lf.(lx.((a f) (f x)))))
                                   //     ((la.(lf.(lx.((a f) (f x))))) 
                                   //       (lf.(lx.x)))))) 
                                   // ((la.(lf.(lx.((a f) (f x))))) 
                                   //   ((la.(lf.(lx.((a f) (f x))))) 
                                   //     (lf.(lx.x)))))

type evaluated = Stringify<Eval<parsed>> // (lf.(lxx.(f (f (f (f (f xx)))))))

 Factorial and limitations

There is an implementation of factorial in Fact.ts, but unfortunately
the compiler has hardcoded type-instantiation depth limits and fails
with Type instantiation is excessively deep and possibly infinite.

About

Lambda Calculus at compile time in TypeScript. TS's type-system is
Turing-complete

Resources

Readme

Stars

1 star

Watchers

1 watching

Forks

0 forks

Releases

No releases published

Packages 0

No packages published

Languages

  * TypeScript 100.0%

  * (c) 2021 GitHub, Inc.
  * Terms
  * Privacy
  * Security
  * Status
  * Docs

 

  * Contact GitHub
  * Pricing
  * API
  * Training
  * Blog
  * About

You can't perform that action at this time.
You signed in with another tab or window. Reload to refresh your
session. You signed out in another tab or window. Reload to refresh
your session.