11 ms·

I'm of the opinion that there is only one lisp right now with some serious potential to dominate in the future, and that is Racket. Why? For one very simple rea

I'm of the opinion that there is only one lisp right now with some serious potential to dominate in the future, and that is Racket. Why? For one very simple reason: unlike all other lisps, there is serious, ongoing, and lengthy research into correctly bringing a static type-checking process to the language. Clojure's core.typed doesn't count here, as it is full of significant holes that invalidate its entire point -- though, those holes are very possibly getting filled in the coming years as they attempt to refactor core.typed following the Racket model. But the Racket team is doing something with lisp that is true to its core, not just with types, but with many other features as well. Interesting piece of trivia: this website you are reading right now is built on top of Racket.

vertex-four 10y ago
Isn't HN on Arc?
- emidln 10y ago
  Arc runs on mzscheme which turned into Racket. The last official release of Arc requires an older release of mzscheme from before lists were immutable. There is a community-maintained fork called Anarki [1] that runs on modern Racket. [1] - http://arclanguage.github.io/ http://arclanguage.github.io/
emidln 10y ago
What makes the Racket model more correct than the system based in Sequent Calculus [1] provided by Shen? [1] - http://www.shenlanguage.org/learn-shen/types/types_sequent_calculus.html http://www.shenlanguage.org/learn-shen/types/types_sequent_c...
- hellofunk 10y ago
  This is the first I've heard of Shen, so I can't say. However the Racket engineers, particularly Matthias Felleisen, are doing cutting-edge research into types. Typing is not a solved problem, because if it was, there wouldn't be a static vs dynamic type debate that lingers ad nauseum. Racket is in an interesting sweet spot for typing research because it is a traditional lisp with dynamic types, to which gradual typing that works both in typed and untyped land has been introduced and continues to undergo extensive attention.
  - effie 10y ago
    "Typing is not a solved problem, because if it was, there wouldn't be a static vs dynamic type debate that lingers ad nauseum." Could you clarify? Surely even if typing was completely solved, we would still have debates of that kind, because there are benefits to both approaches and there will always be people preferring one or another.
    - hellofunk 10y ago
      > because there are benefits to both approaches and there will always be people preferring one or another And that is exactly my point: people prefer one or the other because it is not a solved problem, there is no universally accepted way.
    - groovy2shoes 10y ago
      The reason typing is not a solved problem is this: there are valid programs which can be expressed in an untyped language that cannot be (directly) expressed in a typed one at the moment. For example: (define (foo p?) (if p? 42 "forty-two")) What is the type of `foo`? It could be `bool -> int` or `bool -> string`, depending on the result of `p?`! In an untyped language, this is a perfectly valid program. In a typed language, this presents a type error, even if `p?` happens to always result in `true` or always result in `false`. The programmer reading the program knows that if `p?` is always `true`, then the type of `foo` is `bool -> int`, and that if `p?` is always `false`, the type is `bool -> string`. However, this program, as-is, is will be rejected as ill-typed. In a language providing sum types, we can work around this by using a type like `(int * string) either`: (define (foo p?) (if p? (left 42) (right "forty-two"))) Where `left` and `right` are type constructors for values of type `('a * 'b) either`. Now, the type of `foo` is `bool -> (int * string) either`. This workaround effectively adds a run-time tag to the `either` values to distinguish the `left` case from the `right` case, which is essentially the way dynamically checked languages operate for values of all types but in a more restricted, specific, and arguably meaningful form. In many (most?) languages with sum types, the language will ensure that the programmer always checks the tag of the `either` values before accessing the underlying "actual" value -- this is the only way to guarantee type safety while ensuring that the program does not barf due to a "type" error at run-time. Now, it could be argued that the typing problem presented above is basically solved by sum types. But it could also be argued that this doesn't really solve the problem, because what we'd really like is a way to specify that the type of `foo` depends on the result of `p?`, which could maybe be written as `p:=bool -> (p ? int : string)`, for example. Perhaps dependent typing could help us come to a true solution for this case, but there are other cases where other solutions will be needed. According to Benjamin C. Pierce in Types and Programming Languages: "Being static, type systems are necessarily also conservative : they can categorically prove the absence of some bad program behaviors, but they cannot prove their presence, and hence they must also sometimes reject programs that actually behave well at run time. ... The tension between conservativity and expressiveness is a fundamental fact of life in the design of type systems. The desire to allow more programs to be typed -- by assigning more accurate types to their parts -- is the main force driving research in the field.[0] In essence, while there is already a vast array of programs we already know how to type, and while it's possible to work around cases that resist typing, type theory is still an active field of research with plenty of open questions yet to be answered. The corollary to this is that there are still valid reasons to prefer untyped languages to typed ones, as my sibling commentor pointed out. The day when typing is solved is the day people can no longer not look like an bozos for preferring untyped languages, but until that day comes, untyped languages remain fundamentally more expressive than typed ones (in the sense that they're fundamentally capable of expressing more programs[1]). --- [0]: Pierce, Benjamin C. Types and Programming Languages. MIT Press, 2002. §1.1, pp. 2,3. [1]: There's also a sense in which typed languages are more expressive than untyped ones, and that's the sense that they are capable of expressing more properties of the program as part of the program itself.
hashkb 10y ago
I believe YC builds their new apps in Rails now.
mordocai 10y ago
It might be good to point out to you that the general industry cares very little about things like this. Racket could have literally the most advanced and robust type system out of all programming languages in existence, and still be used by the same amount of people as today and have a hard time convincing anyone else to use it. What makes a language popular from what I have seen are libraries, frameworks, and community. Edit: Racket has all of the above, so obviously there are other factors as well.
- hellofunk 10y ago
  The tide is turning. Naughty Dog video game company (Uncharted, Crash Bandicoot, Jak and Daxter) uses Racket as its scripting language now.
  - nikofeyn 10y ago
    do you have a source for that? it's not that i don't believe you. it's that i am interested. :) i have seen that one powerpoint from a while back where they used their own scheme dialect to script things. but i thought i had read that when they moved to the ps4 they left that behind and used c++ tooling for the same needs.
    - hellofunk 10y ago
      The scheme they have been using was PLT Scheme, which was renamed Racket.
      - nikofeyn 10y ago
        ahh. i know racket was plt scheme originally. but from my understanding, naughty dog was using their own lisp/scheme and now no longer uses that system. https://en.m.wikipedia.org/wiki/Game_Oriented_Assembly_Lisp https://en.m.wikipedia.org/wiki/Game_Oriented_Assembly_Lisp your comment made it sound like they had returned to using a lisp but had chosen to use racket this time around.

vertex-four 10y ago

Isn't HN on Arc?

emidln 10y ago
Arc runs on mzscheme which turned into Racket. The last official release of Arc requires an older release of mzscheme from before lists were immutable. There is a community-maintained fork called Anarki [1] that runs on modern Racket. [1] - http://arclanguage.github.io/ http://arclanguage.github.io/

emidln 10y ago

What makes the Racket model more correct than the system based in Sequent Calculus [1] provided by Shen? [1] - http://www.shenlanguage.org/learn-shen/types/types_sequent_calculus.html http://www.shenlanguage.org/learn-shen/types/types_sequent_c...

hellofunk 10y ago
This is the first I've heard of Shen, so I can't say. However the Racket engineers, particularly Matthias Felleisen, are doing cutting-edge research into types. Typing is not a solved problem, because if it was, there wouldn't be a static vs dynamic type debate that lingers ad nauseum. Racket is in an interesting sweet spot for typing research because it is a traditional lisp with dynamic types, to which gradual typing that works both in typed and untyped land has been introduced and continues to undergo extensive attention.
- effie 10y ago
  "Typing is not a solved problem, because if it was, there wouldn't be a static vs dynamic type debate that lingers ad nauseum." Could you clarify? Surely even if typing was completely solved, we would still have debates of that kind, because there are benefits to both approaches and there will always be people preferring one or another.
  - hellofunk 10y ago
    > because there are benefits to both approaches and there will always be people preferring one or another And that is exactly my point: people prefer one or the other because it is not a solved problem, there is no universally accepted way.
  - groovy2shoes 10y ago
    The reason typing is not a solved problem is this: there are valid programs which can be expressed in an untyped language that cannot be (directly) expressed in a typed one at the moment. For example: (define (foo p?) (if p? 42 "forty-two")) What is the type of `foo`? It could be `bool -> int` or `bool -> string`, depending on the result of `p?`! In an untyped language, this is a perfectly valid program. In a typed language, this presents a type error, even if `p?` happens to always result in `true` or always result in `false`. The programmer reading the program knows that if `p?` is always `true`, then the type of `foo` is `bool -> int`, and that if `p?` is always `false`, the type is `bool -> string`. However, this program, as-is, is will be rejected as ill-typed. In a language providing sum types, we can work around this by using a type like `(int * string) either`: (define (foo p?) (if p? (left 42) (right "forty-two"))) Where `left` and `right` are type constructors for values of type `('a * 'b) either`. Now, the type of `foo` is `bool -> (int * string) either`. This workaround effectively adds a run-time tag to the `either` values to distinguish the `left` case from the `right` case, which is essentially the way dynamically checked languages operate for values of all types but in a more restricted, specific, and arguably meaningful form. In many (most?) languages with sum types, the language will ensure that the programmer always checks the tag of the `either` values before accessing the underlying "actual" value -- this is the only way to guarantee type safety while ensuring that the program does not barf due to a "type" error at run-time. Now, it could be argued that the typing problem presented above is basically solved by sum types. But it could also be argued that this doesn't really solve the problem, because what we'd really like is a way to specify that the type of `foo` depends on the result of `p?`, which could maybe be written as `p:=bool -> (p ? int : string)`, for example. Perhaps dependent typing could help us come to a true solution for this case, but there are other cases where other solutions will be needed. According to Benjamin C. Pierce in Types and Programming Languages: "Being static, type systems are necessarily also conservative : they can categorically prove the absence of some bad program behaviors, but they cannot prove their presence, and hence they must also sometimes reject programs that actually behave well at run time. ... The tension between conservativity and expressiveness is a fundamental fact of life in the design of type systems. The desire to allow more programs to be typed -- by assigning more accurate types to their parts -- is the main force driving research in the field.[0] In essence, while there is already a vast array of programs we already know how to type, and while it's possible to work around cases that resist typing, type theory is still an active field of research with plenty of open questions yet to be answered. The corollary to this is that there are still valid reasons to prefer untyped languages to typed ones, as my sibling commentor pointed out. The day when typing is solved is the day people can no longer not look like an bozos for preferring untyped languages, but until that day comes, untyped languages remain fundamentally more expressive than typed ones (in the sense that they're fundamentally capable of expressing more programs[1]). --- [0]: Pierce, Benjamin C. Types and Programming Languages. MIT Press, 2002. §1.1, pp. 2,3. [1]: There's also a sense in which typed languages are more expressive than untyped ones, and that's the sense that they are capable of expressing more properties of the program as part of the program itself.

hashkb 10y ago

I believe YC builds their new apps in Rails now.

mordocai 10y ago

It might be good to point out to you that the general industry cares very little about things like this. Racket could have literally the most advanced and robust type system out of all programming languages in existence, and still be used by the same amount of people as today and have a hard time convincing anyone else to use it. What makes a language popular from what I have seen are libraries, frameworks, and community. Edit: Racket has all of the above, so obviously there are other factors as well.

hellofunk 10y ago
The tide is turning. Naughty Dog video game company (Uncharted, Crash Bandicoot, Jak and Daxter) uses Racket as its scripting language now.
- nikofeyn 10y ago
  do you have a source for that? it's not that i don't believe you. it's that i am interested. :) i have seen that one powerpoint from a while back where they used their own scheme dialect to script things. but i thought i had read that when they moved to the ps4 they left that behind and used c++ tooling for the same needs.
  - hellofunk 10y ago
    The scheme they have been using was PLT Scheme, which was renamed Racket.
    - nikofeyn 10y ago
      ahh. i know racket was plt scheme originally. but from my understanding, naughty dog was using their own lisp/scheme and now no longer uses that system. https://en.m.wikipedia.org/wiki/Game_Oriented_Assembly_Lisp https://en.m.wikipedia.org/wiki/Game_Oriented_Assembly_Lisp your comment made it sound like they had returned to using a lisp but had chosen to use racket this time around.