LISPoggers

A statically typed poggers Lisp in Lean. LISPoggers is an acronym for “Lisp Is Simply Poggers”.

Features

• [ ] Data types
  • [ ] Type constructors
  • [ ] Lists
  • [ ] Maps
• [ ] Pattern matching
• [ ] Functions
• [ ] Macros

Algebraic Data types

Every structure can be represented by a data type, every datatype is represented by a map of dependencies and a list of constructors that hold types.

(data <dependencies>
  (<constructor> <type>*)*)

Booleans

Simplest datatype example:

(def Bool
  (data {}
    (false)
    (true)))

Naturals

I still need to think about its syntax:

(def Nat
  (data {}
    (zero)
    (inc %))) ;; TODO: recursive datatype syntax

Lists

Generic datatypes receive its parameters as dependencies:

(def List
  (data {a Type}
    (empty)
    (cons a (List a)))) ;; TODO: recursive datatype syntax

Maps

Runtime values exists and can be used on type level, so it can be used on datatypes definitions

(def Map
  (data {k Type
         v Type}
    (empty)
    (cons k v (Map k v)))) ;; TODO: recursive datatype syntax

Pattern matching

(match <expr>
  (<pattern> <expr>)
  (<pattern> <expr>))

Matching over booleans

(match <expr>
  (false <expr>)
  (true <expr>))

Functions

(fn <param>
  <param type>
  <return type>

  <expr>)

Function application

(<fn> <expr>)

;; as in

((fn foo
   Bool
   Bool

   (not foo))
 bar)

Macros

Basically the same as functions but it runs on compile time, so it also has access to types as values.

(macro <param>
  <param type>
  <return type>

  <expr>)

Macro application

(<macro> <expr>)

Complete BNF grammar

<expr> ::= <identifier> | <list> | <map>
<list> ::= "(" <divider> <expr> (<divider> <expr>)* <divider> ")"
<map> ::= "{" <divider> <expr> (<divider> <expr>)* <divider>"}"
<identifier> ::= ([a-z] | [A-Z])+
<divider> ::= (" " | "\n")*

Compiler

flowchart TD
  A[Raw Source Code] --> B[CST]
  B --> C[AST]
  C --> D[Macro Expansion]
  D --> E[Source Compiled to KekwVM Bytecode]
  C --> G[Type Checking Compiled to KekwVM Bytecode]
  C -.- J[Types Checking Interpreter]
  J --> K[Type Checking Evaluation]
  K --> I[Source Type Tree]

Loading

Virtual Machine

flowchart TD
  L[Source as Bytecode] --> M{KekwVM}
  M{KekwVM} --> N[Code Execution]
  O[Type Checking as Bytecode] --> M{KekwVM}
  M{KekwVM} --> P[Type Tree]

Loading