Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

A Path to Enlightenment in Programming Language Theory

steshaw.org

Post reply on HN
Print view View original

41–50 of 99 posts

Re: A Path to Enlightenment in Programming Language Theory

#41

Post by ihm »

mafribe wrote: post #5
psibi wrote: post #2

How much does algebra contribute to learning Type theory ? I'm currently working on the How to prove it book. I thought, I would jump to TAPL after finishing that.

I also don't think studying algebra helps you directly with programming language theory. However algebra is of indirect help if you want to learn category theory, because the latter is a direct generalisation of the former. It is rather difficult for a non-mathematician to pick up category theory from scratch without having first seen the the algebra that category theory abstracts from. Universal properties, category…

> In other sub-fields (e.g. OO, logic programming and concurrency), category theory has not so far proven terribly useful.

I wouldn't say that. I don't know about OO and logic programming, but there's a good amount of categorical/homotopical structure lurking around concurrency. See for example [1], [2] or [3].

[1] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.9...

[2] http://www.researchgate.net/publication/2108154_A_model_cate...

[3] https://en.wikipedia.org/wiki/Directed_algebraic_topology

Re: A Path to Enlightenment in Programming Language Theory

#42

Post by swah »

igravious wrote: post #6

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! Always when I read these I see, "get your Haskell compiler and..." and I'm like, if I knew Haskell well enough to do that I wouldn't be doing this tutorial in the first place. Case in point…

That's something I liked about jonesforth (https://raw.githubusercontent.com/AlexandreAbreu/jonesforth/...) ! but its not a lambda calculus interpreter I guess.

Re: A Path to Enlightenment in Programming Language Theory

#43

Post by tel »

igravious wrote: post #6

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! Always when I read these I see, "get your Haskell compiler and..." and I'm like, if I knew Haskell well enough to do that I wouldn't be doing this tutorial in the first place. Case in point…

If LLVM is good enough for you... http://www.stephendiehl.com/llvm/ and http://dev.stephendiehl.com/fun/ (in progress)

Re: A Path to Enlightenment in Programming Language Theory

#44

Post by tel »

psibi wrote: post #2

How much does algebra contribute to learning Type theory ? I'm currently working on the How to prove it book. I thought, I would jump to TAPL after finishing that.

It's not a direct dependency in the sense that algebra is a direct dependency of, say, algebraic topology.

Instead it's more like a guiding friend. A lot of PL theorists are well-versed in algebra and use it at least stylistically to do their work. If you are familiar with algebra you'll recognize it all over.

But you can definitely get by without it for a while.

The only downside is that you may go a little more slowly due to a general lack of analogies and you may have a difficult time finding resources which don't use algebraic examples.

But honestly, a lot of PL (in fact, TAPL) don't really depend upon abstract algebra much at all.

Re: A Path to Enlightenment in Programming Language Theory

#45

Post by habitue »

NotableAlamode wrote: post #37
habitue wrote: post #20

Earlier quoted context omitted.

I agree with you it'd be useful to see how you might implement lambdas in a language like C. But after that first example, implementing other more complicated language constructs in C, instead of learning ML/haskell is going to be more time fighting C, and less time learning anything new. The lack of side-effects and equational reasoning in functional languages let you get a lot of details out of your way. That being…

The lack of side-effects and equational reasoning in functional languages let you get a lot of details out of your way. Actually ... You (kind-of/sort-of) need side effects when implementing a language with higher-order functions. You at least need it for generating fresh variables to avoid free name capture. Yes, I know you can do this with a monad, but this is not going to help a beginner. It's much easier to maint…

The way I did it was just recursively pass down an accumulator argument to generate De Bruijn index-like variable names, rather than keeping a global counter

Point taken though that it's a bit simpler with global state

Re: A Path to Enlightenment in Programming Language Theory

#46

Post by seanmcdirmid »

NotableAlamode wrote: post #40
seanmcdirmid wrote: post #12

Earlier quoted context omitted.

PL theory has never been dominated by OOP, except for those theories specifically related to it. Just take a look at a POPL '95 proceedings. FP starts from math, for OO math had to be shoe horned into successful existing work that didn't care about it that much.

The semantics of OO languages is really messy and complicated and probably has the least well understood theory of all sequential forms of computing.

Not just that, but we still don't really know how to combine subtyping and generics very well. The soundness question when considering variance is still quite open, and it shows in the poor support for type inference in OO languages (in spite of heroic efforts made in languages like Scala).

Much of this has to do with the root: most of our PL theory was basically designed for FP, and applying them to OOP has been predictably difficult. Most PL theoreticians are more interested in FP than OOP, so progress is quite slow (though see work done by Ross Tate, Igarashi, etc...for progress).

Re: A Path to Enlightenment in Programming Language Theory

#47

Post by AnimalMuppet »

panic wrote: post #9

In practice, most programming languages are not purely or even mostly functional. So why is everything on this list about functional programming?

Note the word "enlightenment" in the title. Everything on the list is about functional programming languages because the author believes that, once you are enlightened, of course you're going to use functional programming languages.

If you find that condescending and/or narrow-minded, you're not alone. There are more things in programming language theory than are dreamt of in their philosophy (to steal a line from Shakespeare).

Re: A Path to Enlightenment in Programming Language Theory

#48

Post by sklogic »

igravious wrote: post #6

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! Always when I read these I see, "get your Haskell compiler and..." and I'm like, if I knew Haskell well enough to do that I wouldn't be doing this tutorial in the first place. Case in point…

There is no point in doing such things in C, since C is just too low level.

What is normally done is a very simple and stupid, but extensible language bootstrapped with C (or whatever else), and then grown up to a level when it's convenient to implement a functional language compiler (i.e., at least higher order functions and some pattern matching).

I wrote about such a bootstrap some time ago: https://combinatorylogic.wordpress.com/2015/01/14/bootstrapp...

Re: A Path to Enlightenment in Programming Language Theory

#49

Post by NotableAlamode »

seanmcdirmid wrote: post #46
NotableAlamode wrote: post #40

Earlier quoted context omitted.

The semantics of OO languages is really messy and complicated and probably has the least well understood theory of all sequential forms of computing.

Not just that, but we still don't really know how to combine subtyping and generics very well. The soundness question when considering variance is still quite open, and it shows in the poor support for type inference in OO languages (in spite of heroic efforts made in languages like Scala). Much of this has to do with the root: most of our PL theory was basically designed for FP, and applying them to OOP has been pre…

    soundness question when considering variance
What is this question? Have you got a reference?

Re: A Path to Enlightenment in Programming Language Theory

#50

Post by igravious »

tel wrote: post #43
igravious wrote: post #6

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! Always when I read these I see, "get your Haskell compiler and..." and I'm like, if I knew Haskell well enough to do that I wouldn't be doing this tutorial in the first place. Case in point…

If LLVM is good enough for you... http://www.stephendiehl.com/llvm/ and http://dev.stephendiehl.com/fun/ (in progress)

Thank you, indeed it is :)
Post reply on HN