6 ms·

Shen – A Sufficiently Advanced Lisp [video]

lkrubner 12y ago
This interests me a great deal: "Qi makes use of the logical notation of sequent calculus to define types. This type notation, under Qi's interpretation, is actually a Turing complete language in its own right. This notation allows Qi to assign extensible type systems to Common Lisp libraries and is thought of as an extremely powerful feature of the language." http://en.wikipedia.org/wiki/Qi_(programming_language) http://en.wikipedia.org/wiki/Qi_(programming_language) What also interests me is that, unlike Java or Scala, adding types is optional, so the types can be layered in. I prefer that style, because when I face a new problem that I have never faced before, I feel that adding type information suggests I know something that I don't actually know. I prefer to add types to a function, once I've come to understand what role a function should play in regards to the problem I'm trying to solve. In that way, the type information also communicates what I have learned about the problem I am trying to solve, versus the areas of my problem that I am still ignorant about, and whose code I can leave untyped while I figure things out. I am also intrigued by what fogus has written: "Qi (and its successor Shen) really push the limits of what we might call a Fluchtpunkt Lisp. I suspect it requires a categorization of its own. A few years ago I was looking for a Lisp to dive into and my searching uncovered two extremely interesting options: Clojure and Qi. I eventually went with Clojure, but in the intervening time I’ve managed to spend quality time with Qi and I love what I’ve seen so far. Qi’s confluence of features, including an optional type system (actually, its type system might be more accurately classified as “skinnable”), pattern matching,3 and an embedded logic engine based on Prolog, make it a very compelling choice indeed." http://blog.fogus.me/2011/05/03/the-german-school-of-lisp-2/ http://blog.fogus.me/2011/05/03/the-german-school-of-lisp-2/ Just recently, here on Hacker News, we had posted an example of a step-by-step explanation of adding types to a working Shen app: http://www.shenlanguage.org/library/shenpaper.pdf http://www.shenlanguage.org/library/shenpaper.pdf Someone in the comments on Hacker News highlighted this comment, by the original author of the untyped app: "No, I didn't think about writing typed version of this program. You know, I'm not "disciplined" kind of person so type discipline is (for now) pretty foreign to me. :) I have the strange feeling that types hampers programmer's creativity." Mark Taver responded with his own thoughts, which I thought were interesting: "The underlined sentence is a compact summary of the reluctance that programmers often feel in migrating to statically typed languages – that they are losing something, a degree of freedom that the writer identifies as hampering creativity. Is this true? I will argue, to a degree – yes. A type checker for a functional language is in essence, an inference engine; that is to say, it is the machine embodiment of some formal system of proof. What we know, and have known since Godel's incompleteness proof [9] [11], is that the human ability to recognise truth transcends our ability to capture it formally. In computing terms our ability to recognise something as correct predates and can transcend our attempt to formalise the logic of our program. Type checkers are not smarter than human programmers, they are simply faster and more reliable, and our willingness to be subjugated to them arises from a motivation to ensure our programs work. That said, not all type checkers are equal. The more rudimentary and limited our formal system, the more we may have to compromise on our natural coding impulses. A powerful type system and inference engine can mitigate the constraints placed on what Racketnoob terms our creativity. At the same time a sophisticated system makes more demands of the programmer in terms of understanding."
- tel 12y ago
  Taver's comment is particularly illustrative. His invocation of Gödel's Incompleteness is particularly interesting. Gödel suggests that any fixed formal system must be true for all compatible models and thus, supposing we built the formal system to capture properties of some model we care about, is going to be overly restrictive to capture what we really want. Fortunately, typed programming languages (taken as the formal proof systems they are) are extensible. Indeed, that's half of what programming is: adding new types (formally or in documentation alone) to help us capture the reasoning for why our program should work. So, programmers need not fear Gödel so much. Instead, if you embrace the type system then it will help to calculate (up to the current limitations of the logic you've designed and your willingness to wait) the consequences of the logic you've currently designed. And, should the type checker help you to determine that your current system does not capture the behavior you're interested in... Well, you just introduce a new type and your formal system grows.
- moonchrome 12y ago
  >Qi’s confluence of features, including an optional type system (actually, its type system might be more accurately classified as “skinnable”), pattern matching,3 and an embedded logic engine based on Prolog, make it a very compelling choice indeed. Note that the post is from 2011, in the meantime Clojure got core.typed (optional type checker), core.match (pattern matching), core.logic (logic engine)-
  - MTarver 12y ago
    Not really the same. That's rather like saying because I have a chassis and some wheels and an engine piled in the garage, I have a car. They have to be connected together in the right way to make Shen. Shen is available under Clojure and has been for about 2 years. I'll also add that IMO there is a difference between having these features in a library and having them in the language standard. Common Lisp for instance, has had pattern-matching in various forms, but if you look at the code contributions on comp.lang.lisp these extensions are not often used.
- AnimalMuppet 12y ago
  The problem is, sometimes I know what I'm doing more than the type system does. But sometimes I only think I know more than it does, and actually it knows more than I do. This makes it very difficult to make the typed-vs-untyped choice "correctly". No matter what you choose, sometimes it's the wrong choice. What's the answer? Maybe gradual type systems? I dream of an IDE where I have a setting for "type rigidity". I'd start with it "off", and just write the code. Then I'd set it to "warn", and see what it complained about. For code to be production, I'd set it to "error". But for that to work, I'd need some way of telling the compliler "I really know more than you do about that type error you think you're seeing, so trust me on this one". (In effect, this winds up functioning something like C/C++ casts.) The problem comes when it's right and I'm wrong, but I tell it to trust me anyway...
segmondy 12y ago
I like what Shen has to offer, but it runs on top of other languages hence there's a huge performance hit. There's nothing revolutionary about it, it's just a lisp with pattern matching, lazy evaluation, prolog system, type checking etc. Having looked at it, it doesn't give much of an edge over say Prolog, I'm yet to see anything that it offer's that Prolog doesn't.
- levosmetalo 12y ago
  "Maybe you want to launch missiles. It's a lisp, not Haskell"
- doall 12y ago
  Shen's powerful T* type system using sequent calculus which is turing complete is revolutionary. Also, Shen's approach doesn't have a huge performance hit. See benchmarks for Qi implemented in SBCL. http://www.lambdassociates.org/studies/study10.htm http://www.lambdassociates.org/studies/study10.htm
- MTarver 12y ago
  I'll let others judge the originality of Shen. I would say that the performance of Shen is very much a function of the platform and the person who did the port. The Merlin compiler in Qi II would, as doall points out, outpace the output of a Lisp programmer. I've yet to put all that technology into Shen. Also, credit to the 2011 Shen committee members who ported Shen to so many platforms, the versatility of being being able to traffic Shen code across languages is what made Aditya's work and talk possible.
akavel 12y ago
From what I remember, it has some weird license. I can never remember what exactly is weird about it (or that of Qi, a related project), but on a quick reading now, I think at least this: "6. [...] In particular it is not permitted to make derived copies of this software which do not conform to the Shen standard or appear under a different title." (i.e. kinda "no forking" clause, IIUC)
- hga 12y ago
  The license text itself is sufficiently complicated and multiply redundant it's hard to tell what it's trying to say. By multiply redundant I mean it tries to say the same thing 3 or more times. The author/creator is incapable of seeing the problems this presents (let alone the terms of the license he's trying to get across); no matter how interested I might be in the language, this has turned out to be a show stopper. And, yeah, there's a no forking clause, subjectively judged; he's also has no interest in a test suite, he says there are already enough implementations of the language.
- totalzeroone 12y ago
  I seem to remember that the author only require that the forked Shen satisfies a number of published tests, that is to guarantee that the forked program function like the original Shen in the basis case. A forked program could extended the original one with new capabilities, libraries and ideas. I think that the author of Shen believe that free sofware should not be free as in beer, now he earn some money selling the Shen book. Only my two cents.
  - jcrubino 12y ago
    Shen and Qi are written by an academic. More likely than trying to sell the book is the that author is trying to ensure that the core theories that got put into the languages stay in the language with out alterations to the core principles... what exactly those are I never delved into enough for comment but the documents and history point to a very principled author and language being created.
    - 12y ago
michaelsbradley 12y ago
I wish Dr. Tarver would make his Book of Shen[1] available via Google Play[2] (or similar). I rarely purchase paper books these days (especially technical books), but am very happy to pay for well-written books and read them on my iPad. [1] http://www.fast-print.net/bookshop/1506/the-book-of-shen-second-edition http://www.fast-print.net/bookshop/1506/the-book-of-shen-sec... [2] https://play.google.com/books/publish/ https://play.google.com/books/publish/

This interests me a great deal: "Qi makes use of the logical notation of sequent calculus to define types. This type notation, under Qi's interpretation, is actually a Turing complete language in its own right. This notation allows Qi to assign extensible type systems to Common Lisp libraries and is thought of as an extremely powerful feature of the language." http://en.wikipedia.org/wiki/Qi_(programming_language) http://en.wikipedia.org/wiki/Qi_(programming_language) What also interests me is that, unlike Java or Scala, adding types is optional, so the types can be layered in. I prefer that style, because when I face a new problem that I have never faced before, I feel that adding type information suggests I know something that I don't actually know. I prefer to add types to a function, once I've come to understand what role a function should play in regards to the problem I'm trying to solve. In that way, the type information also communicates what I have learned about the problem I am trying to solve, versus the areas of my problem that I am still ignorant about, and whose code I can leave untyped while I figure things out. I am also intrigued by what fogus has written: "Qi (and its successor Shen) really push the limits of what we might call a Fluchtpunkt Lisp. I suspect it requires a categorization of its own. A few years ago I was looking for a Lisp to dive into and my searching uncovered two extremely interesting options: Clojure and Qi. I eventually went with Clojure, but in the intervening time I’ve managed to spend quality time with Qi and I love what I’ve seen so far. Qi’s confluence of features, including an optional type system (actually, its type system might be more accurately classified as “skinnable”), pattern matching,3 and an embedded logic engine based on Prolog, make it a very compelling choice indeed." http://blog.fogus.me/2011/05/03/the-german-school-of-lisp-2/ http://blog.fogus.me/2011/05/03/the-german-school-of-lisp-2/ Just recently, here on Hacker News, we had posted an example of a step-by-step explanation of adding types to a working Shen app: http://www.shenlanguage.org/library/shenpaper.pdf http://www.shenlanguage.org/library/shenpaper.pdf Someone in the comments on Hacker News highlighted this comment, by the original author of the untyped app: "No, I didn't think about writing typed version of this program. You know, I'm not "disciplined" kind of person so type discipline is (for now) pretty foreign to me. :) I have the strange feeling that types hampers programmer's creativity." Mark Taver responded with his own thoughts, which I thought were interesting: "The underlined sentence is a compact summary of the reluctance that programmers often feel in migrating to statically typed languages – that they are losing something, a degree of freedom that the writer identifies as hampering creativity. Is this true? I will argue, to a degree – yes. A type checker for a functional language is in essence, an inference engine; that is to say, it is the machine embodiment of some formal system of proof. What we know, and have known since Godel's incompleteness proof [9] [11], is that the human ability to recognise truth transcends our ability to capture it formally. In computing terms our ability to recognise something as correct predates and can transcend our attempt to formalise the logic of our program. Type checkers are not smarter than human programmers, they are simply faster and more reliable, and our willingness to be subjugated to them arises from a motivation to ensure our programs work. That said, not all type checkers are equal. The more rudimentary and limited our formal system, the more we may have to compromise on our natural coding impulses. A powerful type system and inference engine can mitigate the constraints placed on what Racketnoob terms our creativity. At the same time a sophisticated system makes more demands of the programmer in terms of understanding."

tel 12y ago
Taver's comment is particularly illustrative. His invocation of Gödel's Incompleteness is particularly interesting. Gödel suggests that any fixed formal system must be true for all compatible models and thus, supposing we built the formal system to capture properties of some model we care about, is going to be overly restrictive to capture what we really want. Fortunately, typed programming languages (taken as the formal proof systems they are) are extensible. Indeed, that's half of what programming is: adding new types (formally or in documentation alone) to help us capture the reasoning for why our program should work. So, programmers need not fear Gödel so much. Instead, if you embrace the type system then it will help to calculate (up to the current limitations of the logic you've designed and your willingness to wait) the consequences of the logic you've currently designed. And, should the type checker help you to determine that your current system does not capture the behavior you're interested in... Well, you just introduce a new type and your formal system grows.
moonchrome 12y ago
>Qi’s confluence of features, including an optional type system (actually, its type system might be more accurately classified as “skinnable”), pattern matching,3 and an embedded logic engine based on Prolog, make it a very compelling choice indeed. Note that the post is from 2011, in the meantime Clojure got core.typed (optional type checker), core.match (pattern matching), core.logic (logic engine)-
- MTarver 12y ago
  Not really the same. That's rather like saying because I have a chassis and some wheels and an engine piled in the garage, I have a car. They have to be connected together in the right way to make Shen. Shen is available under Clojure and has been for about 2 years. I'll also add that IMO there is a difference between having these features in a library and having them in the language standard. Common Lisp for instance, has had pattern-matching in various forms, but if you look at the code contributions on comp.lang.lisp these extensions are not often used.
AnimalMuppet 12y ago
The problem is, sometimes I know what I'm doing more than the type system does. But sometimes I only think I know more than it does, and actually it knows more than I do. This makes it very difficult to make the typed-vs-untyped choice "correctly". No matter what you choose, sometimes it's the wrong choice. What's the answer? Maybe gradual type systems? I dream of an IDE where I have a setting for "type rigidity". I'd start with it "off", and just write the code. Then I'd set it to "warn", and see what it complained about. For code to be production, I'd set it to "error". But for that to work, I'd need some way of telling the compliler "I really know more than you do about that type error you think you're seeing, so trust me on this one". (In effect, this winds up functioning something like C/C++ casts.) The problem comes when it's right and I'm wrong, but I tell it to trust me anyway...

segmondy 12y ago

I like what Shen has to offer, but it runs on top of other languages hence there's a huge performance hit. There's nothing revolutionary about it, it's just a lisp with pattern matching, lazy evaluation, prolog system, type checking etc. Having looked at it, it doesn't give much of an edge over say Prolog, I'm yet to see anything that it offer's that Prolog doesn't.

levosmetalo 12y ago
"Maybe you want to launch missiles. It's a lisp, not Haskell"
doall 12y ago
Shen's powerful T* type system using sequent calculus which is turing complete is revolutionary. Also, Shen's approach doesn't have a huge performance hit. See benchmarks for Qi implemented in SBCL. http://www.lambdassociates.org/studies/study10.htm http://www.lambdassociates.org/studies/study10.htm
MTarver 12y ago
I'll let others judge the originality of Shen. I would say that the performance of Shen is very much a function of the platform and the person who did the port. The Merlin compiler in Qi II would, as doall points out, outpace the output of a Lisp programmer. I've yet to put all that technology into Shen. Also, credit to the 2011 Shen committee members who ported Shen to so many platforms, the versatility of being being able to traffic Shen code across languages is what made Aditya's work and talk possible.

akavel 12y ago

From what I remember, it has some weird license. I can never remember what exactly is weird about it (or that of Qi, a related project), but on a quick reading now, I think at least this: "6. [...] In particular it is not permitted to make derived copies of this software which do not conform to the Shen standard or appear under a different title." (i.e. kinda "no forking" clause, IIUC)

hga 12y ago
The license text itself is sufficiently complicated and multiply redundant it's hard to tell what it's trying to say. By multiply redundant I mean it tries to say the same thing 3 or more times. The author/creator is incapable of seeing the problems this presents (let alone the terms of the license he's trying to get across); no matter how interested I might be in the language, this has turned out to be a show stopper. And, yeah, there's a no forking clause, subjectively judged; he's also has no interest in a test suite, he says there are already enough implementations of the language.
totalzeroone 12y ago
I seem to remember that the author only require that the forked Shen satisfies a number of published tests, that is to guarantee that the forked program function like the original Shen in the basis case. A forked program could extended the original one with new capabilities, libraries and ideas. I think that the author of Shen believe that free sofware should not be free as in beer, now he earn some money selling the Shen book. Only my two cents.
- jcrubino 12y ago
  Shen and Qi are written by an academic. More likely than trying to sell the book is the that author is trying to ensure that the core theories that got put into the languages stay in the language with out alterations to the core principles... what exactly those are I never delved into enough for comment but the documents and history point to a very principled author and language being created.
  - 12y ago

michaelsbradley 12y ago

I wish Dr. Tarver would make his Book of Shen[1] available via Google Play[2] (or similar). I rarely purchase paper books these days (especially technical books), but am very happy to pay for well-written books and read them on my iPad. [1] http://www.fast-print.net/bookshop/1506/the-book-of-shen-second-edition http://www.fast-print.net/bookshop/1506/the-book-of-shen-sec... [2] https://play.google.com/books/publish/ https://play.google.com/books/publish/