TE
TechEcho
Home24h TopNewestBestAskShowJobs
GitHubTwitter
Home

TechEcho

A tech news platform built with Next.js, providing global tech news and discussions.

GitHubTwitter

Home

HomeNewestBestAskShowJobs

Resources

HackerNews APIOriginal HackerNewsNext.js

© 2025 TechEcho. All rights reserved.

A Path to Enlightenment in Programming Language Theory

155 pointsby jcurboalmost 10 years ago

6 comments

igraviousalmost 10 years ago
What is always missing for me in these lists is a tutorial for knocking together a small lambda calculus + dependently typed interpreter in C. Not ML, Not Ocaml, not, Haskell, not any language that has _already_ got lambdas in it!<p>Always when I read these I see, &quot;get your Haskell compiler and...&quot; and I&#x27;m like, if I knew Haskell well enough to do that I wouldn&#x27;t be doing this tutorial in the first place.<p>Case in point, article says &quot;particularly for programming pracitioners who didn’t learn it at school.&quot; -- Correct! I taught myself Basic, I taught myself a bit of x86 assembler, most importantly, I taught myself C. My working mental model of a computer is the C machine model. And even now, now that I know Ruby with its lambdas, I know that Ruby is written in C. And the Linux kernel. And Nginx (C++ maybe? Dunno). And on, and on.<p>Show me the tutorial where I can build, _in C_ a bare bones working (tail recursion) implementation of the lambda calculus with type inference and dependent (algebraic?) types and I&#x27;ll shake your hand and call you a champion.<p>Closest I&#x27;ve seen is Make A Lisp - <a href="https:&#x2F;&#x2F;github.com&#x2F;kanaka&#x2F;mal" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;kanaka&#x2F;mal</a> but I don&#x27;t think it has the sweet types and tail recursion and other good stuff. PS: bonus points if Regexen are native type :)<p>(Open to suggestions (I am))
评论 #9761272 未加载
评论 #9761374 未加载
评论 #9760922 未加载
评论 #9761018 未加载
评论 #9761762 未加载
评论 #9761608 未加载
评论 #9761614 未加载
评论 #9761613 未加载
评论 #9762378 未加载
jcurboalmost 10 years ago
I spotted this on Twitter [0] and it was timely for me because I&#x27;ve been sorta building my own learning path lately. After learning Haskell a few years ago I got really interested in PLT, type theory, and other higher math (like CT) and also things like formal program verification and automated solvers. So I started trying to decide on a good self-study path (as a guy with a day job who&#x27;s not going to be starting a Ph.D. anytime soon). I ran across this very helpful Reddit thread [1] and so far I&#x27;m thinking of the following path. I&#x27;m starting with <i>How to Prove It</i>, because I never did a lot of proof solving in college (and that was &gt;10 yrs ago anyway) and it&#x27;s a good basis for further work. Then I have two branches.<p>The first is for abstract algebra and CT, because I find them interesting and they&#x27;re useful for understanding Haskell, that currently consists of Pinter&#x27;s <i>A Book of Abstract Algebra</i>, then <i>Conceptual Mathematics</i> by Lawvere and Schanuel, then Awodey&#x27;s CT book, which is a path straight out of that Reddit thread.<p>The second is for PLT&#x2F;type theory, and starts with <i>Software Foundations</i> by Pierce, then <i>Types and Programming Languages</i> by Pierce, then <i>Practical Foundations for Programming Languages</i> by Harper (for completeness, as I have heard pros and cons for both), then maybe moving to <i>Advanced Topics in Types and Programming Languages</i> and such. Mix in some Oregon Programming Language Summer School (OPLSS) [2] videos here and there when they fit. (OPLSS sounds great and I&#x27;m glad their videos are online)<p>[0] <a href="https:&#x2F;&#x2F;twitter.com&#x2F;manisha72617183&#x2F;status&#x2F;613016587696648192" rel="nofollow">https:&#x2F;&#x2F;twitter.com&#x2F;manisha72617183&#x2F;status&#x2F;61301658769664819...</a><p>[1] <a href="http:&#x2F;&#x2F;www.reddit.com&#x2F;r&#x2F;haskell&#x2F;comments&#x2F;29reb7&#x2F;first_or_second_edition_of_introduction_to&#x2F;" rel="nofollow">http:&#x2F;&#x2F;www.reddit.com&#x2F;r&#x2F;haskell&#x2F;comments&#x2F;29reb7&#x2F;first_or_sec...</a><p>[2] <a href="http:&#x2F;&#x2F;www.cs.uoregon.edu&#x2F;research&#x2F;summerschool&#x2F;" rel="nofollow">http:&#x2F;&#x2F;www.cs.uoregon.edu&#x2F;research&#x2F;summerschool&#x2F;</a>
评论 #9771818 未加载
javajoshalmost 10 years ago
I&#x27;d like to find a jargon-free path. There&#x27;s too much gravitas, and hence ego, in the words.<p>It&#x27;s kind of like astronomy - you can (and should) start with looking up, and notice that the stars rotate around the north star. Terms like right ascension, azimuth, celestial spheres, plane of the ecliptic, etc...these are impressive and important sounding and they really get in the way of understanding.<p>It&#x27;s not arbitrary picking astronomy as my example, because in the end <i>computers are physical systems</i>. They are quite unique because they are capable of actions that look like violations of the second law - e.g. you can quite easily reverse a program that simulates gas diffusion, and simulate putting that gas back in a jar - that is, you can define an incredibly delicate system, and reset it for nothing, like being able to use a kitchen for anything and then clean it instantly, for free. More generally, all of a computers negentropy can be recovered for little or no cost after arbitrary disorder! They are also unique because they can rapidly and accurately and repeatedly traverse very specific state spaces, which is unlike anything in the universe, including the human brain.<p>As a physical system, a computer extends through time, and it&#x27;s state is in general time dependent. Coupling signals across time is, I believe, what programming is about. We have special names (jargon!) for different signals - we call signals that come earlier &quot;programming&quot; and signals that come later &quot;runtime input&quot;. But only useful distinction is between signals that arise from outside the system, and those which arise inside (that is, <i>programming</i> and <i>input</i> are the same; but input arising from <i>results of a function call</i> are profoundly different). It&#x27;s useful because only the latter can recurse, which is both a source of error, but also the only possible way &quot;intelligence&quot; (or any really complicated behavior) could possibly express. The only other thing that matters is the shape of the system state - which constrains, in some ways, the kinds of states the system can achieve (or, because it&#x27;s a universal machine, it constrains the general patterns of state traversal in some hand-wavy sense).<p>I built something that demonstrates these ideas, if anyone&#x27;s interested.
psibialmost 10 years ago
How much does algebra contribute to learning Type theory ? I&#x27;m currently working on the How to prove it book. I thought, I would jump to TAPL after finishing that.
评论 #9760832 未加载
评论 #9761625 未加载
评论 #9761849 未加载
评论 #9760794 未加载
评论 #9760770 未加载
dschiptsovalmost 10 years ago
It is only me, or type theory is overrated and oversold?
评论 #9762269 未加载
评论 #9762296 未加载
评论 #9762877 未加载
panicalmost 10 years ago
In practice, most programming languages are not purely or even mostly functional. So why is everything on this list about functional programming?
评论 #9761191 未加载
评论 #9761859 未加载
评论 #9761687 未加载
评论 #9761106 未加载