7 ms·

Somewhat unrelated to this link, but I really think that it’s interesting how much effort we put into the theory side of languages/types - with almost no one in

by wlib 5y ago

Somewhat unrelated to this link, but I really think that it’s interesting how much effort we put into the theory side of languages/types - with almost no one in industry applying these lessons. The essence of this is just something along the lines of “What if we unified values with types, so we could have more useful type checking?” We have billions of dollars being spent and thousands of smart people working for decades, who don’t even get to use a proper type system - forget about statically-checked polymorphism or dependent typing. It’s not even as if we lost the ball, we’re running in the wrong direction. It’s almost trivial to bolt on gradual typing to a language. It’s also not too hard to retrofit dependent types (just don’t bother with Turing-incompleteness). The whole point of these type systems is to better model systems, so why not go the extensible route of letting anyone hook into the “type checking” phase? Import affine types (that decades old thing that got rust popular); write your own domain-specific checker, even. It’s so frustrating to see how beautiful ideas just die because we feel comfortable the way things are now. Maybe language was the wrong abstraction to begin with. Sorry to derail, but this feels like the only path to truly popularize the lambda cube as a concept.

deleted 5y ago
[deleted]
bjourne 5y ago
There is a huge disconnect between industry and academia. Type systems are very interesting but is not what makes the difference in industry. What actually increases productivity and reduces bugs is an under explored area. I think the answers are just as much about sociology, psychology, and ergonomics as they are about type theory.
ogogmad 5y ago
Type theory has uses outside programming. It can be used to make constructive logic rigorous, which was in fact Martin Lof's original use for it.
- wlib 5y ago
  I’m aware of math being entirely useful outside of programming - my little rant is more about how little programming is inspired by math
  - exdsq 5y ago
    I've used Haskell for 18 months in a professional setting. I prefer C++. Grass is always greener - having endless abstractions to be mathsy becomes a real pain when you're trying to build real products.
- black_knight 5y ago
  While making constructive mathematics rigorous was Martin-Löfs original goal, he was quite early aware of the applications to computer science. See for instance his 1979ish paper «Constructive Mathematics and Computer Programming»[0] [0]: 1982 version: https://raw.githubusercontent.com/michaelt/martin-lof/master/pdfs/Constructive-mathematics-and-computer-programming-1982.pdf https://raw.githubusercontent.com/michaelt/martin-lof/master...
adamnemecek 5y ago
As with all research, the good ideas eventually make it to production.
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
- 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.
tluyben2 5y ago
This is what I have noticed writing a lot of software communicating with systems (old systems) with not very well specified input & output; I first want to write drivel and make it work. I don't want to write/change 1000s of vars/fields while i'm not sure if I even need them etc. Then I want to throw away and refactor with lessons learned and I want to keep doing that, adding types (and sometimes proofs). Maybe with compiler flags which enforces static typing for the 'production version'.
- scotty79 5y ago
  TypeScript is language that allows you to work like that. You may use as many and as few types as you need at any given stage of development. As you start adding types to your working program compiler debugs your program for you finding various corner cases. This motivates you to add more types.
  - tluyben2 5y ago
    Yea, it is indeed how I use typescript, but I do not really like javascript much. Typescript does make it better though. I wish other, nicer languages had this.
shrimpx 5y ago
A core problem is that you don't need super fancy type systems to build robust systems in practice. After a certain threshold, type theory research is exploring what's possible in theory, like pure mathematics, not what would be good for practitioners. But one area of large impact for this pure type theory research seems to be the mechanization of mathematics. It looks probable that in the future, the standard way to do mathematics will be by programming it in a proof development system, aka dependently typed programming language.
- ogogmad 5y ago
  > It looks probable that in the future, the standard way to do mathematics will be by programming it in a proof development system, aka dependently typed programming language. This is a controversial opinion, and not all mathematicians are enthusiastic about it, whether rightly or wrongly. Michael Harris, for instance, is a major sceptic and opponent. It is still a very interesting idea. And it has had some notable successes already.
  - Ericson2314 5y ago
    It's a controversial but good opinion. Mathlib marches on and gets better and better.
  - sva_ 5y ago
    I have been wondering why programming is so much more accessible than mathematics to many, considering programming is in some way also a kind of mathematics. I think some of it may have to do with the fact that in programming, one can get immediate and non-judgmental feedback about the correctness of ones solution. In mathematics, it's usually a lot more difficult to verify a solution if you don't already know the answer, so you're dependent on people for it. So perhaps, interactive theorem provers may make mathematics a lot more accessible. But I hope the art of doing it with pen and paper doesn't get lost on us with it.
- creata 5y ago
  > a proof development system, aka dependently typed programming language. There are proof assistants without dependent types, like Isabelle/HOL.
armchairhacker 5y ago
Most of the less abstract parts of this research (generic and polymorphic types w/ variance, ADT structs/unions, even type functions) are in most modern languages (Scala, TypeScript, C++20, Kotlin, Swift, Go). Rust even has affine types The more abstract parts like dependent types are really complicated and even unintuitive to use. See: issues with Rust’s borrow checker, or Haskell being so confusing. Earlier languages like C and Java are mostly legacy code, they use libraries in legacy code, or they’re for developers familiar with them. Untyped scripting languages are fine for scripts. Honestly idk why developers write big libraries in untyped languages like JavaScript and Python. The main case where advanced formal methods are particularly useful is proving program correctness. And AFAIK this stuff is used by industry, although you don’t hear about it as much. The thing is, most programs either don’t “need” to be proved, or they’re way too big.
- chriswarbo 5y ago
  > The more abstract parts like dependent types are really complicated and even unintuitive to use. I disagree with this: dependent types are way easier than lots of the convoluted schemes that non-dependent languages have come up with. As a simple example, dependently-typed languages don't need parametric polymorphism or generics: we can achieve the same thing by passing types as arguments; e.g. map: (inType: Type) -> (outType: Type) -> (f: inType -> outType) -> (l: List inType) -> List outType map inType outType f l = match l with Nil inType -> Nil outType Cons inType x xs -> Cons outType (f x) (map inType outType f xs) When I program without dependent types, I regularly find myself getting "stuck" inadvertently; knowing that (a) there's no way to make my current approach work in this language, (b) that it would be trivial to make it work if I could pass around types as values, (c) that I need to throw away what I've done and choose a different solution, and (d) the alternative solution I'll end up with will be less correct and less direct than my original approach (e.g. allowing more invalid states)
  - andrewflnr 5y ago
    Is there work on cleanly subsetting dependently typed languages to ones where well-typed-ness can be automatically proven? That's not generally the case, right? I think those concerns are basically why people come up with less-general typing mechanisms.

by wlib 5y ago

deleted 5y ago

[deleted]

bjourne 5y ago

There is a huge disconnect between industry and academia. Type systems are very interesting but is not what makes the difference in industry. What actually increases productivity and reduces bugs is an under explored area. I think the answers are just as much about sociology, psychology, and ergonomics as they are about type theory.

ogogmad 5y ago

Type theory has uses outside programming. It can be used to make constructive logic rigorous, which was in fact Martin Lof's original use for it.

wlib 5y ago
I’m aware of math being entirely useful outside of programming - my little rant is more about how little programming is inspired by math
- exdsq 5y ago
  I've used Haskell for 18 months in a professional setting. I prefer C++. Grass is always greener - having endless abstractions to be mathsy becomes a real pain when you're trying to build real products.
black_knight 5y ago
While making constructive mathematics rigorous was Martin-Löfs original goal, he was quite early aware of the applications to computer science. See for instance his 1979ish paper «Constructive Mathematics and Computer Programming»[0] [0]: 1982 version: https://raw.githubusercontent.com/michaelt/martin-lof/master/pdfs/Constructive-mathematics-and-computer-programming-1982.pdf https://raw.githubusercontent.com/michaelt/martin-lof/master...

adamnemecek 5y ago

As with all research, the good ideas eventually make it to production.

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

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.

tluyben2 5y ago

This is what I have noticed writing a lot of software communicating with systems (old systems) with not very well specified input & output; I first want to write drivel and make it work. I don't want to write/change 1000s of vars/fields while i'm not sure if I even need them etc. Then I want to throw away and refactor with lessons learned and I want to keep doing that, adding types (and sometimes proofs). Maybe with compiler flags which enforces static typing for the 'production version'.

scotty79 5y ago
TypeScript is language that allows you to work like that. You may use as many and as few types as you need at any given stage of development. As you start adding types to your working program compiler debugs your program for you finding various corner cases. This motivates you to add more types.
- tluyben2 5y ago
  Yea, it is indeed how I use typescript, but I do not really like javascript much. Typescript does make it better though. I wish other, nicer languages had this.

shrimpx 5y ago

A core problem is that you don't need super fancy type systems to build robust systems in practice. After a certain threshold, type theory research is exploring what's possible in theory, like pure mathematics, not what would be good for practitioners. But one area of large impact for this pure type theory research seems to be the mechanization of mathematics. It looks probable that in the future, the standard way to do mathematics will be by programming it in a proof development system, aka dependently typed programming language.

ogogmad 5y ago
> It looks probable that in the future, the standard way to do mathematics will be by programming it in a proof development system, aka dependently typed programming language. This is a controversial opinion, and not all mathematicians are enthusiastic about it, whether rightly or wrongly. Michael Harris, for instance, is a major sceptic and opponent. It is still a very interesting idea. And it has had some notable successes already.
- Ericson2314 5y ago
  It's a controversial but good opinion. Mathlib marches on and gets better and better.
- sva_ 5y ago
  I have been wondering why programming is so much more accessible than mathematics to many, considering programming is in some way also a kind of mathematics. I think some of it may have to do with the fact that in programming, one can get immediate and non-judgmental feedback about the correctness of ones solution. In mathematics, it's usually a lot more difficult to verify a solution if you don't already know the answer, so you're dependent on people for it. So perhaps, interactive theorem provers may make mathematics a lot more accessible. But I hope the art of doing it with pen and paper doesn't get lost on us with it.
creata 5y ago
> a proof development system, aka dependently typed programming language. There are proof assistants without dependent types, like Isabelle/HOL.

armchairhacker 5y ago

Most of the less abstract parts of this research (generic and polymorphic types w/ variance, ADT structs/unions, even type functions) are in most modern languages (Scala, TypeScript, C++20, Kotlin, Swift, Go). Rust even has affine types The more abstract parts like dependent types are really complicated and even unintuitive to use. See: issues with Rust’s borrow checker, or Haskell being so confusing. Earlier languages like C and Java are mostly legacy code, they use libraries in legacy code, or they’re for developers familiar with them. Untyped scripting languages are fine for scripts. Honestly idk why developers write big libraries in untyped languages like JavaScript and Python. The main case where advanced formal methods are particularly useful is proving program correctness. And AFAIK this stuff is used by industry, although you don’t hear about it as much. The thing is, most programs either don’t “need” to be proved, or they’re way too big.

chriswarbo 5y ago
> The more abstract parts like dependent types are really complicated and even unintuitive to use. I disagree with this: dependent types are way easier than lots of the convoluted schemes that non-dependent languages have come up with. As a simple example, dependently-typed languages don't need parametric polymorphism or generics: we can achieve the same thing by passing types as arguments; e.g. map: (inType: Type) -> (outType: Type) -> (f: inType -> outType) -> (l: List inType) -> List outType map inType outType f l = match l with Nil inType -> Nil outType Cons inType x xs -> Cons outType (f x) (map inType outType f xs) When I program without dependent types, I regularly find myself getting "stuck" inadvertently; knowing that (a) there's no way to make my current approach work in this language, (b) that it would be trivial to make it work if I could pass around types as values, (c) that I need to throw away what I've done and choose a different solution, and (d) the alternative solution I'll end up with will be less correct and less direct than my original approach (e.g. allowing more invalid states)
- andrewflnr 5y ago
  Is there work on cleanly subsetting dependently typed languages to ones where well-typed-ness can be automatically proven? That's not generally the case, right? I think those concerns are basically why people come up with less-general typing mechanisms.