Hacker News Reader

Comment by ohazi | Hacker News Reader

There seem to be two big camps that preach a "learn this weird new programming paradigm because it'll help you see things from a new perspective and will make you a better engineer" message: the lispy languages, and the ML-like languages. Both of these languages categories give you functional programming as well as metaprogramming, which is great. Having tried both, I've found that the ML-derived languages tend to have a stronger type system that's more rigorously enforced at compile time. I personally find this much more valuable in practice than some of the dynamic magic that you can do with lisp.

There are some notable exceptions, of course, but part of this is just inherent to the design of lisp, and I think it's easy to end up with a type safety system that feels more like it's bolted on than part of the language.

View on HN

There are also plenty of Lisp programmers that think that it's a real tool to solve real problems, not just an educational oddity. There are a bunch of Lisps out there, and plenty of them are by no means toys. My laptop's initial RAM disk and init system are Scheme programs.

And it's not a Lisp per se, but WebAssembly's text format uses s-expressions[0]. It's likely that the "oddity" of Lisps will seem less odd as adoption increases if they stick with that.

[0]https://developer.mozilla.org/en-US/docs/WebAssembly/Underst...

I had no idea they did that! Thanks!

I was just thinking this morning about making Arc work in web assembly sometime.

gcc’s IR, “GIMPLE”, is also commonly printed in s-expression form.

As is LLVM's. I think JVM's might be too, but not 100% sure.

Haskell is also pretty much just a lisp with a whole lot of sugar added on.

How is Haskell a Lisp?

To me, a Lisp pretty necessarily needs to treat the structure of its code as mutable data, which seems kind of incompatible?

The evaluation model of both is quite similar though (reduction), and you can see it in the similarities between Core Haskell and Core Scheme.

AFAIK, there are very few truly built in types in Haskell. Most everything can be built out of data constructors and functions. That idea of many things being in language user space is pretty Lisp-y IMO.

The evaluation model is different. Lisp is using strict evaluation and Haskell is using lazy evaluation.

Haskell is statically typed, Lisp is not.

Lisp uses s-expressions for writing programs, Haskell does not.

Generally Haskell and Lisp are very different languages: in syntax, semantics and pragmatics (how the language is used).

No, it actually doesn't; that is a common misconception.

Lisp images can modify themselves at run-time by replacing global function bindings with new functions, not by mutating code.

Lisp macros must not in fact mutate the incoming source code which they transform.

> How is Haskell a Lisp?

The same way Lisp is a functional language. It has to do with how both languages are built from only a few basic primitives, and how both are based on Lambda calculus.

An ML is also not a Lisp, though.

> How is Haskell a Lisp?

... both communities care a lot about rose trees?

If you squint right, both monads and lisp S-expressions are rose trees.

Not to mention that one can get static typing in Lisps, if one wanted. See Typed Racket, for instance:

https://download.racket-lang.org/docs/5.0/pdf/ts-guide.pdf

I just listened to an interview with Philippe Kahn and he mentioned that the language he uses today is Scheme.

what are you using? I want to try it.

Not GP but could be Guile https://www.gnu.org/software/guile/

I use GuixSD https://gnu.org/s/guix

"Having tried both, I've found that the ML-derived languages tend to have a stronger type system that's more rigorously enforced at compile time. I personally find this much more valuable in practice than some of the dynamic magic that you can do with lisp."

You probably meant to contrast ML's static typing (not strong typing) with Lisps's dynamic typing. See "What To Know Before Debating Type Systems":

https://cdsmith.wordpress.com/2011/01/09/an-old-article-i-wr...

Sure, I meant static types + Hindley-Milner type inference, leading to a "type system that I like and feel comfortable with" (per your link), i.e. a stronger type system.

For another (type-theory) perspective - a 'dynamic language' can be automatically considered weakly typed if it can return an runtime exception due a failure to perform a runtime type coercion, or because the typesystem is not expressive enough to include a proof of totality. That makes the whole dynamic/static versus strong/weak distinction kind of meaningless.

> The functional and imperative languages are weakly typed, i.e. the result of computing the value of an expression e of type T is one of the following: [...]

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceMa...

As a matter ordinary meaning, I also feel it makes sense to talk about more strongly typed languages, because they can express 'stronger' guarantees about behavior. Eg. a proof that the code cannot deadlock.

> more rigorously enforced at compile time

'Compile time', like everything in the artificial science of computing, is a made up thing. We might reconsider if it's a useful idea to keep. Why must there be a specific point in time, when we verify interconnections within a little bundle of code, but later when the bundle of code integrates with a larger system we are completely fine with very different, loosely coupled connections?

The internet is dynamically typed. I just don't see static verification scaling to that level. But verification is still great - so maybe we need a way to verify connections between components as and when they bind. If we build a good model for this late bound 'negotiated safe' binding, the static model might become unnecessary (because you can do the verification whenever you choose, or at multiple times and different scales, as the 'bundle of code' integrates with larger and larger systems.)

"Compile time" is artificial, but the difference between static and dynamic is natural (in some sense, I realize these words are quite slippery). It emerges from the underlying mathematics. There's a real difference between correctness properties that I can prove without running my program and correctness properties that will introduce failures at runtime.

You're using a dynamic language (bash) to invoke your statically-typed-language-compiler and then to also invoke the binary it produces.

But what's the difference to say, having just a single dynamically typed language with library functions "type-check-my-code", which returns an encapsulated value, and "run-my-typechecked-code" which takes the encapsulated value as input? The whole process happens at "runtime" here.

The artificial static/runtime boundary is introduced by the way Unix implements files and processes. All statically typed languages are effectively supersets of the language of Unix. In Unix we can treat each executable binary as a library function (except that we have a massive overhead for calling it). The designers of Unix were well aware of this which is why from the POV of bash, there's no distinction between invoking a binary and invoking another script written in bash.

How much of the Unix binary and process bloat is really necessary though to say, concatenate N files? Even someone writing a C program will avoid calling cat and instead implement it themselves, or call a library that does it. Perhaps we need to reconsider where the boundary between type checking and running code should be.

runtime here means the runtime of target program, it has nothing to do with unix. If your program fails while executing due to a type error, it's not static type-checking.

I think sparkie has a very valid point. It has to do with Unix because a 'program' in Unix has specific meaning (and Windows is no different in this regard, btw). A Unix program doesn't map exactly to what a program means in the theoretical sense. E.g. two Unix processes talking over a socket are not thought of as single Unix program, even though they can be considered a single theoretical program. So there is a tendency to think in 'processes' not 'systems'. I elaborated a little more about this elsewhere in this thread (https://news.ycombinator.com/item?id=15581591).

But it has nothing to with typing, as typing means tying to a location in program, you can have processes communicating part of the same program, but the type-error will refer to a part of program and when the type-error is detected i.e. during execution of that part of program or some external part of program is what we are concerned here.

Example: You could think of an interpreter for a statically-typed language running various processes as the same program, but we still say the language is statically typed.

> You could think of an interpreter for a statically-typed language running various processes as the same program, but we still say the language is statically typed.

Is it statically typed for cross process messages though?

There certainly is a fundamental difference between what programmers refer to as compile-time and runtime. Naming is probably problematic; but mathematically you cannot prove all the properties of a program just by looking at its syntax, in general. Because this implies a solution to the halting problem. In other words, there is no program, given your program, that can verify it; whereas, there exists a program, given an input and your program, that can verify that your program outputs the correct thing (as long as the language can be emulated by a Turing machine). When it comes to programming languages, the distinction can be trickier, since you can technically get a python program and statically analyze it. So, "compile" time and "run"time are not necessarily perfect words but they belong to the programming terminology. The more crucial thing is, there is a mathematical difference between those two.

> mathematically you cannot prove all the properties of a program just by looking at its syntax, in general.

A solution that is often overlooked is to simply shrink the set of legal programs. Simply typed lambda calculus for instance has a perfectly decidable halting problem (which is, programs written in it always halt).

There are 2 ways to handle undecidable properties with static analysis: either reject programs for which you can't prove the property holds (you will reject correct programs), or accept programs for which you can't prove it doesn't (you will accept incorrect programs, and may use runtime checks to compensate).

Rejecting correct programs is a problem only to the extent one would like to write such a program in the first place. Take this expression for instance:

  if 2 + 2 = 4
  then "Yay!"
  else 0

It is a perfectly fine expression, of type `string`. Most type systems will reject it however because the two branches of the conditional don't have the same type. Thing is, we don't care about this program in practice, since the constant test expression screams code smell to begin with.

Yeah, but now you're arguing something else. Simply typed lambda calculus is not Turing-complete. With a Turing-complete language, you cannot decide the halting problem of an arbitrary sentence of that language. With a non-Turing-complete one, you potentially can. For example, Charity is one such non-Turing-complete language, for which, hypothetically, one can find an algorithm to decide halting of an arbitrary program. But most languages today are Turing-complete, because TC is a very easy property not to have, and it is very hard to construct non-TC but useful languages (eg, C++ metaprogramming is accidentally Turing complete, so is HTML+CSS). So, while what you explained is correct, it does not have direct implications on languages like Python, C++ etc. We still have different sort of properties while we're statically analyzing a TC language, and executing it with an input. This was what I was trying to explain.

Being Turing complete doesn't mean you cannot prove anything without solving the halting problem. Programs have many potentially undecidable properties, and halting is only one of them. It's also one of the strongest.

It doesn't matter which property you are looking at. If it's undecideable, you can sidestep the issue by forbidding programs for which the checker is not sure.

That doesn't mean you have to lose Turing Completeness. You just have to chose properties that don't imply that the program halts. Static typing for instance doesn't mean the language isn't Turing Complete. Simply typed lambda calculus is the exception here.

Where did I claim "you cannot prove anything without solving the halting problem" or "static typing means non Turing complete" exactly? I said nothing of this sort... IN TC languages you can prove some properties, but in general you cannot prove your program is correct. When I say in general, I mean exactly that. You keep bringing some specific cases where you can prove correctness, but that's beyond my point.

I sometimes workaround this by proving for "outputs the correct result, or loops forever". Here, you don't have to prove for halting, since your program is not expected to halt in some cases anyway. But then in some particular cases, you can prove that your algorithm is correct. You do not have to lose Turing-completeness to do this. But it gets trickier when you want to built a type system that can give all the bugs in your program, in general. You can definitely build something that finds all the bugs "for all intents and purposes" but not something that can be mathematically proven that will give you all of them. To be concrete, you can build a program, given arbitrary Python code, gives most of/all the bugs in this program. But you cannot build a program, given arbitrary Python code, that is proven that it will correctly know whether this program will output correct result for all possible inputs. You can do this for some restricted Python programs (as you've been arguing for last two comments) but in general you cannot do this, which brings us to this fundamental division.

> It emerges from the underlying mathematics.

Which mathematics?

(Lisp has its own math, for instance.)

Very fundamental ideas around computability, or total vs partial functions. There are some correctness properties that we can prove without running the underlying program, such that we can always accept or reject a given program. None of this is particular to lisp.

Fundamental ideas about computability include the model of the Turing machine, which has no notion of types, verification, or even functions whatsoever - there are just too many degrees of freedom.

I agree there are correctness properties we can prove without running a 'program', but how do we map the notion of a 'program' into the real world. Is a single function a program? A single module which includes multiple functions? A single executable? A single system that includes multiple processes communicating over a network? I'm arguing each of these is a 'program' and a Turing machine in the theoretical sense. Each of these programs is hooked up to other 'programs' outside of it. 'Compilation' requires the input to be static, but if we think about how things are in flux (you can change a function, switch out a shared library or upgrade and restart a running process, etc.) when do you verify that a 'program' is 'correct'?

This is what I mean by 'compile time is made-up' - it falls out of the current frame of thinking of one OS process = one program = static set of source files. It is possible to design systems that have no notion of 'compile time'. You could still have verification, but it could be incremental and spread out all through the lifetime of the running system. So the system would have no 'compile phase' - it would be running live and as you update parts of it, the updated parts would integrate with the rest of the system and do verification like things.

What on earth are you talking about?

> The internet is dynamically typed.

That's an incoherent claim.

Dynamic typing is where types belong to values. Static typing is where they apply to terms.

Really to call the former "typing" is misnomer. It's an abuse of the word "type" to mean "memory mode". It has not much relationship to typing in the logic/math/philosophy of logic sense in which types are sets and type relationships are those between sets.

It is the Curry-Howard isomorphism (https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...) which defines the correspondance between types in computer science and mathematics.

This is "static" only because the "dynamic" alternative isnt really an alternative at all, and really just a different kind of thing all together.

This crosses into incivility. That breaks the site guidelines. Please re-read them and don't do that when commenting here.

https://news.ycombinator.com/newsguidelines.html

I'm not sure how this is incivil?

The claim is logically incoherent: typing cannot be a property of the internet, in the same way tuesday cannot be pink nor can addition sound terrifying.

The claim is a category error: the internet cannot posses such a property.

In addition, to say, of something, that it is " is a made up thing " is a degree of hubris that is presumably reasonably met by being perplexed at overconfidence of the claim posed with such little correct information.

Is being perplexed more uncivil than hubris? Are we really policing people's language to this minute degree?

"What on earth are you talking about" is uncivil. Your comment didn't need that.

Actually you broke this guideline as well: "Please respond to the strongest plausible interpretation of what someone says, not a weaker one that's easier to criticize." It's possible that shalabhc intended to make a mathematical claim, but a stronger plausible interpretation is easy to come up with (e.g. "it's hard to enforce static guarantees across the software that interoperates on the internet").

The reason we ask people to follow this guideline is not so much that it's nicer, but that nitpicking things each other probably didn't say is tedious and detracts from good conversation, which is what we're really hoping for.

Static typing enables faster feedback loops. The kind of thing Bret Victor raves about.

In practice, I've been able to accomplish things with static typing that I hadn't the brainpower to do with dynamic typing, because even with a REPL, runtime errors came too late, and didn't meaningfully informed me of my mistakes.

As for why we switch to dynamic typing as we scale up, some of it probably has to do with trust. Computers communicating over the internet cannot trust each other, if they can even trust they are talking to one another to begin with. They have no choice but to perform lots of runtime checks to make sure they don't get pwned by the slightest remote mishap. Once you get to this point, static verifications become much less useful, and can often be skipped altogether.

> As for why we switch to dynamic typing as we scale up, some of it probably has to do with trust.

I'll note that we switch to 'dynamic' much before the question of trust arises. Whenever you do IPC between two OS processes you fully trust, communicate through a database or file, wire up a multi-process system with config files, etc. Most internal code at an organization is trusted, yet the communication between OS processes within an company uses dynamic messaging semantics.

I'll also point out that if you use a compiled shared library, or any system call you are forced to use the type system of C, which isn't particularly advanced.

It could be that we haven't developed dynamic messaging protocols that can bind safely and correctly. I'm arguing that if we have these, they might apply on a smaller scale too (objects within a 'process' or connections between shared libraries, etc.)

> Static typing enables faster feedback loops.

All of that only works on the small scale - where the type knowledge has to be fully shared within the entire program. As soon as you're writing code to call a service, static typing benefits are moot. The current solution is to create 'stubs', which doesn't scale well either. I am not arguing for 'dynamic typing everywhere', but rather about a different POV where we start looking at 'interconnections' at all levels the same way, and think about making the introspection and safe late binding in a standard, scalable way. Minimizing pre-shared knowledge would be one way to improve how this scales, for instance.

> Most internal code at an organization is trusted,

It is not.

We trust our colleagues not to be malicious, but we generally don't trust them not to make mistakes. Hence defensive programming.

The point is trust and typing seem orthogonal. E.g. I use static typing within one 'program' but 'dynamic' as soon as I split my program into two, even when the level of trust didn't change. Same thing when including my colleagues' code within my 'program' vs. calling it across program boundaries.

The point I'm trying to make is that 'static-typing style verification' which happens across different parts of a 'single program' doesn't extend to multiple programs or real systems. Maybe we should look at some kind of late bound dynamically bound verification - i.e. a protocol that is executed whenever one 'program' reaches out and connects to another, to determine if the connection is safe and correct. Do you think this has value?

What about typed Racket?

https://docs.racket-lang.org/ts-guide/beginning.html

Yeah, this was the "notable exception" I had in mind.

ML has metaprogramming? The only thing I know approaching that is template haskell, which is a weak form of metaprogramming (still powerful obviously).

Meanwhile, lisp is metaprogramming. No, it's not useful in many (or even most) applications, but when it is useful, you can bet there's some type of analogous pattern for a lisp-type language. Certainly still useful to learn along side ML. :)

Hell, the best quote to illustrate this is the article itself:

> A fun thing about it this is that once you’ve grokked it, you can think right away of better programming languages than Lisp, and you can think right away of better ways to write the meta descriptions than John did. This is the “POV = 80 IQ points” part.

In this sense, everyone should learn lisp, even if it's not the tool you intend to use.

> ML has metaprogramming? The only thing I know approaching that is template haskell, which is a weak form of metaprogramming (still powerful obviously).

Of course, it has had it for a very long time (a decade at least?), see camlp4/camlp5.

How often is camlp4/5 used among the typical OCaml programmer compared to how often macros are used among typical Lisp programmers?

How easy is camlp4/5 metaprogramming to read and write compared to Lisp macros?

This reminds me of Alan Perlis' admonition to "beware of the Turing tar-pit in which everything is possible but nothing of interest is easy."[1] and of a question John McCarthy asked Peter Norvig after the latter's talk about how Python was a Lisp:

"When he finished Peter took questions and to my surprise called first on the rumpled old guy who had wandered in just before the talk began and eased himself into a chair just across the aisle from me and a few rows up.

This guy had wild white hair and a scraggly white beard and looked hopelessly lost as if he had gotten separated from the tour group and wandered in mostly to rest his feet and just a little to see what we were all up to. My first thought was that he would be terribly disappointed by our bizarre topic and my second thought was that he would be about the right age, Stanford is just down the road, I think he is still at Stanford -- could it be?

"Yes, John?" Peter said.

I won't pretend to remember Lisp inventor John McCarthy's exact words which is odd because there were only about ten but he simply asked if Python could gracefully manipulate Python code as data.

"No, John, it can't," said Peter and nothing more, graciously assenting to the professor's critique, and McCarthy said no more though Peter waited a moment to see if he would and in the silence a thousand words were said."[2]

[1] - https://en.wikipedia.org/wiki/Turing_tarpit

[2] - http://smuglispweeny.blogspot.com/2008/02/ooh-ooh-my-turn-wh...

> How easy is camlp4/5 metaprogramming to read and write compared to Lisp macros?

Having implemented a non-trivial 'macro' in camlp4 and likewise in Scheme, I can confidently say: It's about the same level of difficult/pain. Which is to say that it's much too painful/annoying.

Though, I should say that Racket by all accounts from the literature has improved things massively, even going to so far as to implement "macro-based" type systems (search for "turnstile racket").

EDIT: Just a side point, but:

    A witty saying proves nothing
       - Voltaire

(No idea if Voltaire ever said that, but that's kind of the point.)

I've long desired a strongly-typed s-expression syntax that has the power of Haskell or Idris, but still looks and feels like the blank canvas that is Lisp.

https://github.com/lexi-lambda/hackett

https://lexi-lambda.github.io/blog/2017/05/27/realizing-hack...

Thanks!

Reply on news.ycombinator.com