Hacker News Reader

> The thing about Turing-complete languages is that the only real dimmension of power is their expressiveness - i.e. how much boilerplate do you have to write to implement something

Have fun implementing your compile-time Common Lisp typechecker.

I mean, you can do it. I have friends implementing a typechecker for Python, and it works. As for me, I'm very happy to have someone else implementing/debugging/maintaining a typechecker for me so i can do other things with my time, like watch cats climb into boxes on youtube.

Common Lisp has a compile-time typechecker.

But anyway, that's kind of my point. Typechecker is the kind of excess feature the principle of least power would like you to reject.

In practical terms I need a typechecker to write code at anything like the rate I do, with anything like the defect rate I achieve. But that's possibly sophistry. I agree the principle is not quite right (or at least not quite absolute) as stated; using extra power has a high but finite cost, it is occasionally worth using more power than you strictly need if the benefit is high enough.

I think there's a second dimension of languages to consider, namely how hard it is to write incorrect code. To some extent these goals are conflicting, in that preventing incorrect things often means disallowing some shorter correct solutions.

> I could use the same reasoning to justify writing my code in Common Lisp instead.

Maybe you should then. I find it too hard to restrict my code in lisps: if I want a certain part of my code to be in a DSL-like constrained sublanguage, there's no standardized way to express that, only ad-hoc macros.

> It makes sense in non-Turing-complete languages though (configurations, DSLs) - because there by "least power" one means power in the computational sense.

I think non-Turing-complete general-purpose languages are possible. I'm very excited for Idris.

> I find it too hard to restrict my code in lisps: if I want a certain part of my code to be in a DSL-like constrained sublanguage, there's no standardized way to express that, only ad-hoc macros.

There is a standardized way - via "ad-hoc" macros. Except they're not really more "ad-hoc" than using classes and traits in Scala is "ad-hoc".

Maybe 'aninhumer has a point - restricting the language is kind of the opposite goal of making it expressive/powerful.

> I think non-Turing-complete general-purpose languages are possible. I'm very excited for Idris.

Idris is not Turing-complete? :o.

[0] - https://news.ycombinator.com/item?id=11470569

> There is a standardized way - via "ad-hoc" macros. Except they're not really more "ad-hoc" than using classes and traits in Scala is "ad-hoc".

They're not standardized enough to have good common tooling around restricted embedded DSLs. If you use the type system to enforce restrictions around certain areas of Scala code, every Scala tool understands it. IME a lot of lisp programmers end up writing their own tool integration, because there is no standard for that kind of restriction (macros can be arbitrary code; in practice programmers restrict themselves to sensible macros, but in a way that isn't exposed to tooling).

> Idris is not Turing-complete? :o.

In practice there are escape hatches, but it's a total language: your function must come with a proof that it terminates.

> [Idris] is a total language: your function must come with a proof that it terminates.

So, you can't express the programs that never terminate, but can you express all the programs that would terminate?

Point in case, you probably shouldn't ever want to use a language for the specific feature that could express a non-deterministic program.

> So, you can't express the programs that never terminate, but can you express all the programs that would terminate?

This gets philosophical - would the program "Y {f => x => if(x is a proof of the inconsistency of PA via the Goedel encoding) 0 else f(x+1) } 0" terminate? If you assume consistency of PA then no.

> Point in case, you probably shouldn't ever want to use a language for the specific feature that could express a non-deterministic program.

Well the mu operator or equivalent (informally, the inverse operator) is an extremely useful feature. Many useful programs can't be written strictly primitive recursively (as a trivial example, you can't compute the Ackermann function). I have hope that we can find more restricted versions of mu that let us express all the programs we want to, but that's a decidedly nontrivial problem.

>Maybe 'aninhumer has a point - restricting the language is kind of the opposite goal of making it expressive/powerful.

My point was more that safety is a separate, important metric of language quality. It often conflicts with expressiveness, but not necessarily.

See also SPJ's "Haskell is Useless" video: https://www.youtube.com/watch?v=iSmkqocn0oQ

I was going to say Scala's secret weapon was in it's non-turing-complete typesystem.

Unfortunately, Scala's typesystem is turing complete.