3 ms·
This is a nice post! Jeremy Siek wrote a similar post a few years ago: http://siek.blogspot.co.uk/2012/07/crash-course-on-notation-in-programming.html http://s
by neel_k 9y ago
This is a nice post! Jeremy Siek wrote a similar post a few years ago:
http://siek.blogspot.co.uk/2012/07/crash-course-on-notation-in-programming.html http://siek.blogspot.co.uk/2012/07/crash-course-on-notation-...
If I could add one thing to these two posts, it would be to learn Prolog.
We write inference rules top-down ("from these premises, we draw this conclusion"), but we often read them bottom-up ("given this goal, what facts could have lead to it?").
This double-vision thing, where you simultaneously view a set of inference rules in both a deductive and goal-directed fashion, is IMO one of the main stumbling blocks for people new to type theory. Luckily[1], however, it's fundamentally the same intuition that Prolog programmers develop -- and learning new programming languages is usually easy for programmers.
[1] It's not really by luck, of course: Prolog is called a logic programming language for a reason...
- BlahBoy3 9y agoJeremy was one of my professors last semester at IU! Really smart guy- nice to see his blog post getting some recognition here.
- chubot 9y agoDo you have any recommendations on learning Prolog with the goal of writing practical/real type systems? Ideally a book that has runnable example programs? I had bookmarked this awhile ago but haven't gone through it: Writing custom type systems for Python in Prolog https://news.ycombinator.com/item?id=12108041 https://news.ycombinator.com/item?id=12108041
- mcguire 9y agoWell, hmph. I've been meaning to experiment with Prolog-as-a-type-system-for-a-language for a long time. The wayback machine has a valid link to the article: https://web.archive.org/web/20170216030548/http://code.alehander42.me/prolog_type_systems https://web.archive.org/web/20170216030548/http://code.aleha...