From 7e9714839c12dbe8b9386f933c8b14d49567ae79 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Mon, 3 Nov 2025 19:49:48 +0100 Subject: draft plan --- lambda-calcul/haskell/README.md | 58 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 58 insertions(+) diff --git a/lambda-calcul/haskell/README.md b/lambda-calcul/haskell/README.md index 096627c..d568ace 100644 --- a/lambda-calcul/haskell/README.md +++ b/lambda-calcul/haskell/README.md @@ -6,3 +6,61 @@ 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 -- cgit v1.3.1