A toy STLC implementation.
Haskell Emacs Lisp Shell
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
etc
examples
scripts
src
.gitignore
.travis.yml
LICENSE
README.md
Setup.hs
dash.cabal

README.md

dash

A toy lambda calculus implementation that will be simply typed one day.

Silly examples

(Highlighted as ocaml, because I'm not sure which language is closest to dash's Skye syntax).

Function definition

fun x:nat y:nat := x:nat.

Function application

(fun x:nat := x:nat) | 3.   (* 3 *)

Global context insertion

  • (NOTE: Does not yet exist)
  • (NOTE 2: Later on, with proper type inference, a lot of this syntax will clean up)
let a:nat := 1.
let const:nat=>nat=>nat := (fun x:nat y:nat := x:nat).

Local context insertion

  • (NOTE: Does not yet exist)
  • (NOTE 2: Later on, with proper type inference, a lot of this syntax will clean up)
let constThree:nat=>nat := (fun x:nat := a:nat) where a:nat := 3.

License

BSD-3, but it's a toy and you probably don't want it.