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

81–90 of 99 posts

Re: A Path to Enlightenment in Programming Language Theory

#81

Post by nbouscal »

dschiptsov wrote: post #75
tel wrote: post #71

Earlier quoted context omitted.

I can't say it's only you, but I certainly don't agree.

Donald Knuth might say so too.) The problem, in my opinion, is same as with Category theory. While the math describing behavior of categories as abstractions is probably correct, the categories themselves are mere abstractions. Consider clouds (in the sky). One could try to categorize them, but it is useless, because each cloud is unique. Same goes for companies, people, etc. Categories are useful for crude approxima…

... You know that we do have a categorization of clouds, right? I think meteorologists would disagree with you about the utility of that categorization.

More to your point: whether you can do something without a tool has no bearing on whether or not it is a useful tool. You can write programs in machine code if you'd like to, but you're highly unlikely to be as productive as someone using a high-level programming language. Similarly, you can program without a type system if you'd like to, but you're highly likely to end up with runtime errors that you wouldn't have had you used a type system.

Re: A Path to Enlightenment in Programming Language Theory

#82

Post by nbouscal »

JesperRavn wrote: post #78
dschiptsov wrote: post #70

It is only me, or type theory is overrated and oversold?

It is certainly oversold. There is a typical discussion that goes A: I'm a simple Python programmer. Please tell me why I need types. B: Types let you catch many bugs that would otherwise cause compile time errors or require compile time checks or testing. A: But I've seen studies that suggest that static typing does not prevent bugs. B: When I said static typing, I meant dependently typed languages, which can expres…

I've spent a lot of time hanging out with pretty hardcore type theory people, and have never seen any of them recommend a dependently-typed language to a new programmer. In other words, you're pretty blatantly fighting a straw man.

Re: A Path to Enlightenment in Programming Language Theory

#83

Post by JesperRavn »

nbouscal wrote: post #82
JesperRavn wrote: post #78

Earlier quoted context omitted.

It is certainly oversold. There is a typical discussion that goes A: I'm a simple Python programmer. Please tell me why I need types. B: Types let you catch many bugs that would otherwise cause compile time errors or require compile time checks or testing. A: But I've seen studies that suggest that static typing does not prevent bugs. B: When I said static typing, I meant dependently typed languages, which can expres…

I've spent a lot of time hanging out with pretty hardcore type theory people, and have never seen any of them recommend a dependently-typed language to a new programmer. In other words, you're pretty blatantly fighting a straw man.

It's not about how experienced the programmer is. The problem is that people do a bate and switch when it comes to type theory, promising the benefits of dependent types even though there are no production languages that deliver these benefits.

Re: A Path to Enlightenment in Programming Language Theory

#84

Post by seanmcdirmid »

AnimalMuppet wrote: post #58
NotableAlamode wrote: post #49

Earlier quoted context omitted.

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

I'm not the one you were replying to, but maybe seanmcdirmid means this: https://en.wikipedia.org/wiki/Covariance_and_contravariance_... But I thought that was pretty well understood, so I don't know what he thinks is open...

For many popular type systems with generics, not really; e.g. see http://www.cs.cornell.edu/~ross/publications/mixedsite/mixed...

Re: A Path to Enlightenment in Programming Language Theory

#85

Post by [deleted] »

AnimalMuppet wrote: post #58
NotableAlamode wrote: post #49

Earlier quoted context omitted.

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

I'm not the one you were replying to, but maybe seanmcdirmid means this: https://en.wikipedia.org/wiki/Covariance_and_contravariance_... But I thought that was pretty well understood, so I don't know what he thinks is open...

[deleted]

Re: A Path to Enlightenment in Programming Language Theory

#86

Post by nrinaudo »

NotableAlamode wrote: post #49
seanmcdirmid wrote: post #46

Earlier quoted context omitted.

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?

It is possible that he's referring to mutable and covariant types being unsound.

As an example, let's assume that you have two classes, Cat and Dog, both inheriting from Animal, and that you have a covariant mutable List implementation.

Say you have a value of type List[Cat]. Since List is covariant, this value can legally be passed to a function that expects a parameter of type List[Animal].

Now, imagine you have a function that expects a List[Animal] and adds a Dog to it. That's a legal operation: Dog extends Animal and can thus be used this way.

Putting the two together, you have a perfectly legal way of adding a Dog to a List[Cat], which a sound type system should not allow. An example of that is Java's Array, which is both covariant and mutable, and that as a result can yield type errors at runtime.

Re: A Path to Enlightenment in Programming Language Theory

#87

Post by mafribe »

ihm wrote: post #41
mafribe wrote: post #5

Earlier quoted context omitted.

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/publica…

You mean Goubault-style homotopy stuff. I don't this this is very categorical, e.g. [2] produces a single category, so I wouldn't call this an example of categorical structure. The Gunawardena paper [1] doesn't exhibit categorical structure either.

Re: A Path to Enlightenment in Programming Language Theory

#88

Post by nandemo »

igravious wrote: post #28
mafribe wrote: post #16

Earlier quoted context omitted.

When I open Pierce TaPL and see immediately ML my heart sinks. I strongly recommend that you ignore this feeling and learn a modicum of ML coding. If you want to learn TAPL, just learn a bit of Ocaml. You don't need much. If you already speak C, a bit of Haskell and Ruby, you should be able to pick up enough Ocaml in a few hours/days. Programming in Ocaml is way easier than in Haskell or C. The only two things that a…

Really? I feel like C fits my brain, know what I mean? I don't even think that it was because I learnt it early on. It's a simple language, I feel. Why is programming way easier in Ocaml than in C? Setting aside that for me programming is way easier in C than in Ocaml because I know C and don't know Ocaml, what is it about Ocaml that is way easier than C? Anyway, my original point is that it is _cheating_ to explain…

> Today I'm going to learn how to build a car. First, take the engine from my Toyata... oh... um...

To the extent that the analogy works, it doesn't help your case: nobody these days builds or learns how to build a car from scratch, without access to an existing car. It's not only that you're typically making a modified version of an existing model: you also use a car to get to the factory, you use existing vehicles to transport raw materials and tools to the factory, etc.

In any case, as others have pointed out, it's not like you need to use a full {Lisp, Haskell, ML} compiler to implement (say) tail recursion. It's that you bootstrap: as soon as you have a minimal viable {Lisp, Haskell, ML} compiler, it makes sense to use that instead of C to implement other features.

Re: A Path to Enlightenment in Programming Language Theory

#89

Post by dschiptsov »

nbouscal wrote: post #81
dschiptsov wrote: post #75

Earlier quoted context omitted.

Donald Knuth might say so too.) The problem, in my opinion, is same as with Category theory. While the math describing behavior of categories as abstractions is probably correct, the categories themselves are mere abstractions. Consider clouds (in the sky). One could try to categorize them, but it is useless, because each cloud is unique. Same goes for companies, people, etc. Categories are useful for crude approxima…

... You know that we do have a categorization of clouds, right? I think meteorologists would disagree with you about the utility of that categorization. More to your point: whether you can do something without a tool has no bearing on whether or not it is a useful tool. You can write programs in machine code if you'd like to, but you're highly unlikely to be as productive as someone using a high-level programming lan…

Except when the type system restricts you to homogeneous data-structures in inherently heterogeneous world. Herbert Spencer, the philosopher, could tell us a lot about it.

As for crude and misleading clasdification - there is no shortage for them, especially in realms of psychology (hypohondric, sangvinic - all that nonsense) or economics and finance. The results of application of flawed economic/financial models based on flawed categories could be seen everywhere. For meteorology, please, ask anyone who lives in monsoon area - there is worse than coin-flipping accuracy when it comes to hill regions.)

Re: A Path to Enlightenment in Programming Language Theory

#90

Post by tel »

dschiptsov wrote: post #75
tel wrote: post #71

Earlier quoted context omitted.

I can't say it's only you, but I certainly don't agree.

Donald Knuth might say so too.) The problem, in my opinion, is same as with Category theory. While the math describing behavior of categories as abstractions is probably correct, the categories themselves are mere abstractions. Consider clouds (in the sky). One could try to categorize them, but it is useless, because each cloud is unique. Same goes for companies, people, etc. Categories are useful for crude approxima…

"Decent" programming is a wiggle word. I'm of course obliged to agree with you when you define it. In a similar way, decent programming can be done with Turing Machines, punch cards, raw circuitry, brainfuck, what-have-you. Each would require a notion of "decent" in line with the style of the tool, but there is no hard place to push against when defining "decent".

My belief about type theory is that it serves, for purposes of PL, as a massively more difficult challenge than merely making a programming language which also happens to spawn programming languages on accident.

This is really important because as we've seen—PL design without some deeper driving purpose or mechanism for making tradeoffs can wind up wherever you want it to be. LOLCODE is a real thing and without Type Theory the only way we can talk about our distaste for it is to say that it's "indecent" for deeply personal reasons.

Type Theory wouldn't accept this because its goal is to be a good foundational system for all logic and mathematics.

It's also important to note that Type Theory doesn't serve this purpose by being aligned to some arbitrary goal. It works because the goal of "being a good foundational system for all logic and mathematics" is not so dissimilar from the goal of a PL which might be "represent all interesting thoughts of a programmer in a computable fashion". If Type Theory happened to stumble across non-computable mechanisms then it would be a poor fit, but because it turns out to be the case that the best foundational system must respect computability... things match up.

And ultimately that's the joy of learning Type Theory and programming with it: things match up. I say this flippantly because I lack the words for the enormity of the "matching up" that occurs.

Before I knew Type Theory I felt that PLs were cute and arbitrary. It was interesting to learn them anthropologically, but frustrating to use them because I was building on foundations of sand. After learning Type Theory I understand where the hard places are, where the foundation exists, and I know how to build things which I feel confident can last hundreds of years.

Post reply on HN