# minilang

A minimal functional language to learn and experiment with type systems.

* http://www.cse.chalmers.se/~bengt/papers/GKminiTT.pdf
* https://homotopytypetheory.org/2017/09/16/a-hands-on-introduction-to-cubicaltt/
* https://github.com/kino3/Mini-TT


# Agenda

## Notes

* How do we make a language?
  * How do you make a baby?
  * Things we use everyday but don't know how it works?
* Why?
  * empower and free oneself
  * Uxntal -> 100 rabbits
* How do I talk about my world/domain?
  * would it not make sense to find better ways to express it?
  * ensure code complexity does not map 1-1 with domain complexity
* What would it entail?
  * reuse "simple" existing language focusing on _understanding_
  * parser -> interpreter -> pretty-printer
* If I can make my own language, I can bring the language _where_ I
  need it or want it to be

* starting point: how to talk to a machine?

## Plan A

* (5') Intro:
  * How to talk to machines?
  * not reinvent the wheel -> use existing knowledge
* Collective coding
  * (5') play with parser/pretty-printer -> relate internal representation w/ external representation (human readable)
    * representation for humans vs. for machines
  * (45') focus on the interpreter
    * introduce the rules of the λ-calculus
    * implement evaluator
      * use the leaderboard
      * use the web UI for checking/troubleshooting
  * (20') simply typed λ-calculus
  * (5') type inference
* (5') Closing thoughts
  * we'll be exchanging beers for knowledge

## Plan B

* (5') Intro:
  * How to talk to machines?
  * not reinvent the wheel -> use existing knowledge
* Collective coding
  * (15-20') play with parser/pretty-printer/interpreter -> relate internal representation w/ external representation (human readable)
    * representation for humans vs. for machines
    * boolean algebra (together)
  * (45') focus on the type-checker
    * motivated by the fact it's easier to write with types
    * simply typed version
    * Problem: can we leverage the types to write stuff?
    * need to modify evaluator to introduce primitive interpretation
  * (10') type inference
* (10') Closing thoughts
  * we'll be exchanging beers for knowledge