My little lambda calculus primer is on the HN front-page this morning.

· · Web · 2 · 9 · 17

@neauoire I learned that a while ago now but this looks like a fun refresher :)

@neauoire Gratz! Or commiserations, depending on how trollsome HN is on the day.

I enjoyed the primer the other day though - thank you. Still don't understand the Lambda Calculus Urge to Make Animal Analogies but I far prefer the digestibility of your version to the long essay format.

@seachaint It's aimed at people(like myself) who don't have a math background. I find it a bit of a shame that such a beautiful concept is hidden behind incomprehensible wikipedia pages.

@neauoire That's awesome.
I love it when such things are translated from academese to anything else.
Like how Zig accidentally taught me that dependent types are actually easy, without ever mentioning any of the things you will find in articles about it written in academese.

@owl @neauoire @seachaint Does Zig have dependent types? 👀

Also I'm curious, what other introductions did you have to dependent types? There is a lot of academic stuff, but The Little Typer and Type Driven Development in Idris seem reasonably un-academic to me. Did you try those?

@csepp @seachaint As far as I understand it yes, some flavour of it.
Types can depend on values and live in the same world and can be manipulated like values. With the restriction that types only exist at compile-time, which makes sense for a systems language. I believe ATS is the same in that regard.
"Generic" type params are just params that go along with the others, and you return types to create instances of them.
Those resources sound familiar but I'm not sure. :)
@neauoire @seachaint

@csepp I did try Idris at some point, and made some minor contributions, but Zig was the first time I started using anything like that to make programs I felt I could understand, both reading the source and what comes out the other end.
@seachaint @neauoire

@neauoire I appreciate analogies, I also lack a formal maths background. I just find it kind of amusing how Lambda peeps seem to love inventing animal analogies: the bird one is ok, the crocodile one was just odd.

It sure beats trying to endure people explaining Monads (Yunno, the monoid endofunctors, 'obviously'). Although ever since I realised that >50% of popular monad explanations are entirely incorrect I've found that amusing, too. :)

Anyways your version is my new go-to bookmark for reference on Lambda

Sign in to participate in the conversation

Revel in the marvels of the universe. We are a collective of forward-thinking individuals who strive to better ourselves and our surroundings through constant creation. We express ourselves through music, art, games, and writing. We also put great value in play. A warm welcome to any like-minded people who feel these ideals resonate with them.