youtu.be/U3GQePblz4M
What is the easiest language?
01.02.2025 06:02
👍 59
🔁 16
💬 0
📌 1
Not explicity, but I was trying out the imperative-ish do syntax, and I believe that uses partial functions when desugared. For example:
private def infiniteLoop: Nat := Id.run do
let mut n: Nat := 0
while true do
n := n + 1
n
Blundered into my first infinite loop bug in Lean - and it seems Lean isn't really as set-up to help rule out certain runtime issues ("panics" and non-termination) as I had initially assumed. A teeny bit disappointed!
I would love a chiller version of AOC where all the problems are first-week level of difficulty.
Nice! I'm really thrown by Lean's imperative syntax in do blocks - for loops, while loops, mutation. I need to read up on what's going on!
"Falling in love" and "thinking it sucks" are both limiting perspectives on TypeScript. It's a remarkable piece of pragmatic programming language tech that bolts some sanity on top of JS and its ecosystem - but all the warts of JS are all still there. The Web should aspire to better.
Day 8 Advent of Code in Lean: github.com/mdr/aoc-2024...
I keep trying to migrate this one and the video gets corrupted. It’s just that powerful!
#FunctionalProgramming #Haskell #OCamel #Programming
React but for TUIs would be fun, I bet that exists already
Day 5 of #AdventofCode in Lean: github.com/chenson2018/...
One of my favorite days so far, came out very cleanly. Having quicksort in the language is nice. I enjoyed writing the function to get the middle of an Array with a provably correct index, though ran into some decidable equality trickiness.
What does a partial def do?
github.com/mdr/aoc-2024...
I stole and ported this "diagonals" function for today's puzzle. It might be interesting to prove some properties about it, e.g. that the elements of `join (diagonals grid)` are the same (ignoring order) as the elements of `join grid`.
It would work, but the extra wrappers would make me sad:
[ShapeCircle (Circle 3.0), ShapeSquare (Square 4.0)]
How do you find it compared to the proprietary models?
Day 4 Advent of Code in Lean: github.com/mdr/aoc-2024...
I suspect I might begin to fall behind the daily pace soon! Today's was a straightforward puzzle, but it took me a while to get both parts working as a Lean novice.
Are you thinking along the lines of:
data Circle = Circle { radius :: Double }
data Square = Square { side :: Double }
data Shape where
CircleShape :: Circle -> Shape
SquareShape :: Square -> Shape
filterCircles :: [Shape] -> [Circle]
A Shape must be a Circle or a Square. In Scala, I can write
def findCircles(shapes: List[Shape]): List[Circle]
In Haskell (and other FP languages), I'm stuck with:
findCircles :: [Shape] -> [Shape]
Is there a way to achieve the expressivity of the former if you lack subtypes?
PostHog is a top tier name for (amongst other things) a session replay tool!
I hadn't come across Dave Farley before, but he talks a lot of sense!
Microservices are just technical debt: www.youtube.com/watch?v=LltD...
Day 3 Lean Advent of Code solution:
github.com/mdr/aoc-2024...
I used regexes (but there was enough unpacking of matches that I suspect parser combinators would have been cleaner), and State monad to turn on/off instructions (probably overkill).
Me too! I did Unison last year, and Idris the year before. I suspect I might only get through a dozen puzzles or so, but I like the excuse to tinker with something new.
Day 2 Advent of Code solution in Lean: github.com/mdr/aoc-2024...
Lean's syntax sugar where you can call certain functions as if they were methods or properties - e.g "report.differences.toSet" - is very pleasant, especially if your day job is OO languages.
I'm trying to learn a little #leanlang theorem proving as well as use it as a programming language for Advent of Code. I would especially like to get to where I could start to prove some simple properties about programs!
🎁 Just in time for your #AdventOfCode puzzles, the latest Unison version, 0.5.29 contains a few code rendering improvements and a hefty performance boost for some programs using the standard interpreter.
I like Lean's Nested Actions syntax
lean-lang.org/lean4/doc/do...
Day 1 Advent of Code solution in Lean
github.com/mdr/aoc-2024...
Thanks! Where does the Discord server live?
I did look at the Lean Zulip, it does feel a bit intimidating though!
