5 ms·

You said a lot of stuff, and I disagree with most of it, but I'm open to dialogue. > with almost no one in industry applying these lessons Straight-up incorre

by dvt 5y ago

You said a lot of stuff, and I disagree with most of it, but I'm open to dialogue. > with almost no one in industry applying these lessons Straight-up incorrect. Language designers think long and hard about how typings work in their languages. Rob Pike, Ken Thompson, and Russ Cox deliberated generics for like a decade[1] before finally allowing them in Go. > a proper type system I'm not sure exactly what you mean by "proper" -- but "rigid" type systems are extremely cumbersome to use practically. (Typed) λ-calculus is an academic example; Haskell is a real-world example. > not too hard to retrofit dependent types (just don’t bother with Turing-incompleteness) Hard disagree. It actually is extremely hard: type resolution is undecidable, for one. So you need to carefully design type resolution in a way that the "edges" of types don't (or can't) break the runtime too badly. > why not go the extensible route of letting anyone hook into the “type checking” phase Absolutely terrible idea, for many reasons, but mainly because, if C/C++ macros are any indication, people will abuse any kind of compile-time (or pre-processing) trickery you give them access to. > write your own domain-specific checker, even I guess I'm in the opposite camp here, I think domain specific languages are an absolute dumpster fire of abstraction and 99.9% of the time completely exceed the scope of the problem they're trying to solve. The purpose of a programming language is to be applicable to many classes of problems, and DSLs fly in the face of that pretty common-sense tenet. [1] https://research.swtch.com/generic https://research.swtch.com/generic

wlib 5y ago
I’m on my phone so I can’t really give this the response that it’s owed, but most of what I want to say is that I don’t think we disagree as much as you think. My mention of languages being the wrong approach to general programming is a key aspect of my position. You’re right that DSL’s are usually not a great idea, but that seems like more of an issue with the “syntax-chasing”. The affordances that a syntax forces upon everyone are why it takes a decade to add generics to Go and why macros are even used to begin with. As we see from the various notations used for equivalent math, we probably we be better off encoding the structure as a flexible semantics graph and then “projecting the syntax” however the programmer wants. Keep in mind that what I write is about possibilities more than what you would be forced to do every project. You wouldn’t expect everyone to import random type systems more than you would expect everyone of write and import their own random crypto system libraries. Some of the most popular languages out there have absolutely zero static checks. Would it be so bad to write a Turing complete static check function? Why do we care so much about decidability that we can’t even consider it in useful exceptions? Also, do you think macros a la lisp would be so bad if they had more powerful type systems backing them up and more flexible editors to understand them?
- dvt 5y ago
  > Would it be so bad to write a Turing complete static check function? I think most type systems are, in fact, Turing complete (there's a fun proof somewhere that TypeScript is, for example). And most typed languages (Go, C++, Java, TypeScript) have pretty mature static type-checkers, unless I'm misunderstanding your ask.
  - creata 5y ago
    "Typing is Hard" is a popular list of languages and the decidability of typechecking in them: https://3fx.ch/typing-is-hard.html https://3fx.ch/typing-is-hard.html
    - sva_ 5y ago
      That's a nice list > Zig > undecidable, since evaluation of recursive functions at compile time is possible, thus requiring the compiler to solve the halting problem. For some reason, I find that amusing.
ebingdom 5y ago
> Straight-up incorrect. Language designers think long and hard about how typings work in their languages. Rob Pike, Ken Thompson, and Russ Cox deliberated generics for like a decade[1] before finally allowing them in Go. I think that kind of proves their point. Parametric polymorphism is one of the most well-understood, least contentious extensions to the lambda calculus. It's formalized by System F and has been implemented in programming languages 40 years ago with great type inference for an important subset (Hindley-Milner). Yet generics was highly controversial in the Go community. And now since none of the standard library was designed with generics in mind, it's full of unsafe patterns that involve essentially dynamic typing (e.g., the `Value` method of `Context`). Despite Rob Pike et al. designing one of the most popular languages today (Go), I consider them more experts in systems rather than programming languages. > I'm not sure exactly what you mean by "proper" -- but "rigid" type systems are extremely cumbersome to use practically. (Typed) λ-calculus is an academic example; Haskell is a real-world example. I find Haskell a joy to use, and I cringe at having to use languages like Java and Go, which are a minefield of error-prone programming patterns (like using products instead of sums to represent "result or error"). Generally speaking, my Haskell code is shorter, less buggy, and more reusable than my Go code, so I'm not sure what you mean by "cumbersome".
- dvt 5y ago
  > I find Haskell a joy to use, and I cringe at having to use languages like Java and Go, which are a minefield of error-prone programming patterns (like using products instead of sums to represent "result or error"). Generally speaking, my Haskell code is shorter, less buggy, and more reusable than my Go code, so I'm not sure what you mean by "cumbersome". I just want you to realize that you are in the extreme minority here, but just from a common-sense POV, if I'm prototyping a project, looking for product-market fit, the last thing I want to care about is that my typeability is recursively enumerable or what-have-you. I just want to build something quickly without much hoopla (hence the massive popularity of very weakly-typed languages like JS and Python). FWIW, I think that generics are a mistake in Go, but I was just trying to counter the point that language designers don't think long and hard about type-theoretic features. I think the main issue with generics, wasn't so much an inept "we don't know how to do this," but rather "is this worth the code complexity?" and "is this worth the added compile times?" -- both of which were main selling points of Go.
rowanG077 5y ago
Go is the poster boy for a language NOT learning anything from decades of PL theory and research.
- thaumasiotes 5y ago
  In my mind, Go is an attempt at keeping the nice things about Java while discarding the worse things.
  - kaba0 5y ago
    Then they have a very strange definition of nice things, when it includes worse error-handling, more verbosity and bad abstractibility.
foobiekr 5y ago
Oh my goodness do I ever agree about any kind of “use parser cleverness to make your cute interior domain specific language” thing as found in Scala and Ruby and a few other contexts. If you want a language, and have legit need, fire up antlr and build a quick compiler. Parser cleverness if the “internal DSl” variety is on par with the C++ windowing libraries that used heavy operator overloading to be clever, the stuff like “window += new Button()” and other nonsense. Just awful and torturous.

by dvt 5y ago

wlib 5y ago

I’m on my phone so I can’t really give this the response that it’s owed, but most of what I want to say is that I don’t think we disagree as much as you think. My mention of languages being the wrong approach to general programming is a key aspect of my position. You’re right that DSL’s are usually not a great idea, but that seems like more of an issue with the “syntax-chasing”. The affordances that a syntax forces upon everyone are why it takes a decade to add generics to Go and why macros are even used to begin with. As we see from the various notations used for equivalent math, we probably we be better off encoding the structure as a flexible semantics graph and then “projecting the syntax” however the programmer wants. Keep in mind that what I write is about possibilities more than what you would be forced to do every project. You wouldn’t expect everyone to import random type systems more than you would expect everyone of write and import their own random crypto system libraries. Some of the most popular languages out there have absolutely zero static checks. Would it be so bad to write a Turing complete static check function? Why do we care so much about decidability that we can’t even consider it in useful exceptions? Also, do you think macros a la lisp would be so bad if they had more powerful type systems backing them up and more flexible editors to understand them?

dvt 5y ago
> Would it be so bad to write a Turing complete static check function? I think most type systems are, in fact, Turing complete (there's a fun proof somewhere that TypeScript is, for example). And most typed languages (Go, C++, Java, TypeScript) have pretty mature static type-checkers, unless I'm misunderstanding your ask.
- creata 5y ago
  "Typing is Hard" is a popular list of languages and the decidability of typechecking in them: https://3fx.ch/typing-is-hard.html https://3fx.ch/typing-is-hard.html
  - sva_ 5y ago
    That's a nice list > Zig > undecidable, since evaluation of recursive functions at compile time is possible, thus requiring the compiler to solve the halting problem. For some reason, I find that amusing.

ebingdom 5y ago

> Straight-up incorrect. Language designers think long and hard about how typings work in their languages. Rob Pike, Ken Thompson, and Russ Cox deliberated generics for like a decade[1] before finally allowing them in Go. I think that kind of proves their point. Parametric polymorphism is one of the most well-understood, least contentious extensions to the lambda calculus. It's formalized by System F and has been implemented in programming languages 40 years ago with great type inference for an important subset (Hindley-Milner). Yet generics was highly controversial in the Go community. And now since none of the standard library was designed with generics in mind, it's full of unsafe patterns that involve essentially dynamic typing (e.g., the `Value` method of `Context`). Despite Rob Pike et al. designing one of the most popular languages today (Go), I consider them more experts in systems rather than programming languages. > I'm not sure exactly what you mean by "proper" -- but "rigid" type systems are extremely cumbersome to use practically. (Typed) λ-calculus is an academic example; Haskell is a real-world example. I find Haskell a joy to use, and I cringe at having to use languages like Java and Go, which are a minefield of error-prone programming patterns (like using products instead of sums to represent "result or error"). Generally speaking, my Haskell code is shorter, less buggy, and more reusable than my Go code, so I'm not sure what you mean by "cumbersome".

dvt 5y ago
> I find Haskell a joy to use, and I cringe at having to use languages like Java and Go, which are a minefield of error-prone programming patterns (like using products instead of sums to represent "result or error"). Generally speaking, my Haskell code is shorter, less buggy, and more reusable than my Go code, so I'm not sure what you mean by "cumbersome". I just want you to realize that you are in the extreme minority here, but just from a common-sense POV, if I'm prototyping a project, looking for product-market fit, the last thing I want to care about is that my typeability is recursively enumerable or what-have-you. I just want to build something quickly without much hoopla (hence the massive popularity of very weakly-typed languages like JS and Python). FWIW, I think that generics are a mistake in Go, but I was just trying to counter the point that language designers don't think long and hard about type-theoretic features. I think the main issue with generics, wasn't so much an inept "we don't know how to do this," but rather "is this worth the code complexity?" and "is this worth the added compile times?" -- both of which were main selling points of Go.

rowanG077 5y ago

Go is the poster boy for a language NOT learning anything from decades of PL theory and research.

thaumasiotes 5y ago
In my mind, Go is an attempt at keeping the nice things about Java while discarding the worse things.
- kaba0 5y ago
  Then they have a very strange definition of nice things, when it includes worse error-handling, more verbosity and bad abstractibility.

foobiekr 5y ago

Oh my goodness do I ever agree about any kind of “use parser cleverness to make your cute interior domain specific language” thing as found in Scala and Ruby and a few other contexts. If you want a language, and have legit need, fire up antlr and build a quick compiler. Parser cleverness if the “internal DSl” variety is on par with the C++ windowing libraries that used heavy operator overloading to be clever, the stuff like “window += new Button()” and other nonsense. Just awful and torturous.