Shen – A Sufficiently Advanced Lisp [video] | Hacker News Reader

Shen – A Sufficiently Advanced Lisp [video]

youtube.com

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)

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.

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.

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.

After searching for the official specification (a term used formally in the license), the only thing I could find is the web page for the documentation that is called the official shen standard doc, http://www.shenlanguage.org/learn-shen/shendoc.htm, so I suppose the official specification is the content of this page. As I don't have the book of Shen I can't tell if there is further documentation about the "specification of the language".

The author in the license page claims that he is not going to make a fork illegal by changing the standard in such a way as to make the fork retrospectively illegal.

There was one author who made a close source port of Shen in java but then there were big problems. Perhaps he could give a lot of information of what kind of problems are you to encounter when you try to develop a close source product using Shen. The last think I can remember was that he bought the book of Shen for her 16 years old daughter and he was emotionally very interested in Shen but then all went down. [By the way, I apologize for not putting the 's i the third person )). in my other posts.

here is the link https://groups.google.com/forum/#!topic/qilang/yL2Eps2cnwY

The issue here was not that the port was closed; but that people helped to build it and gave their time for free on the assumption it was going to be free and readable. My post

https://groups.google.com/forum/?hl=en#!topic/qilang/PJyM6xC...

opened this topic. The rest is history.

I have a clear policy of not contributing my time to closed (for money) software unless I am being paid as a consultant. I do not have any objection as such to closed source software.

Mark

Hello Mark. Could you give a link to the "specification of Shen", that is, is there a battery of test that for a fork of Shen certifies that the fork is a conforming with the specification fork?, is the "official standard documentation web page of Shen the text of the specification alluded in the license?

Thanks for you work in Shen.

The license was introduced before Shen was issued in September 2011 (the license came out in June) and for a year or so the only specification was Shendoc (now Shendoc 16). The understanding was that Shen was specified in that document and what was not covered by Shendoc was covered by 'Functional Programming in Qi'. Later a hurriedly introduced text 'The Book of Shen (first edition)' (TBoS) was produced to fill a gap (2012) and this year (January 2014) a more thorough 2nd edition of TBoS (> 400 pages) was published which fixes the language standard very thoroughly. This is currently the canonical standard. You can find a link to that book on the Shen home page.

http://www.fast-print.net/bookshop/1506/the-book-of-shen-sec...

Shen is now very stable and has been for nearly two years. At my suggestion, I posited that it might be better to move the standard to a computable series of tests and this was floated to the 2011 committee that is responsible jointly for all the ports.

http://shenlanguage.org/2011committee.html

Such a change requires the unanimous consent of all the people involved and it seems we have this and a reworded simplified license.

The only obstacle is the work needed to put this test suite together. I've suggested that this suite might be assembled in Github, though for legal reasons the final version must be put in a publicly accessible but tamper-proof place.

Since the type-integrity given out by the system is not better than the strength of the kernel, we take kernel work very seriously. There is already a suite of 126 tests that I run every Shen port through and 2011 members echo these tests. But this informal test suite needs to be amped up to several hundred tests to approach what I consider to be an adequate test suite. It is very boring but important work. So far I have begun assembling all the programs in TBoS into this suite.

These license issues really only affect people who are deeply involved in kernel work and as far as application programmers are concerned, I doubt that it affects them much at all. As far as graphics, concurrency, FFI etc. and add-ons are concerned there are no restrictions. Likewise none on closed source work.

I'll also add that I'll be asking for volunteer contributions on the Shen news group to help assemble this test suite. So people who want to expedite us here can do so.

If you want to see the tests that are currently used; they are in the source code download.

http://www.shenlanguage.org/Download/download.html

See Test Programs/Readme.shen

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-sec...

[2] 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)

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/

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

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."

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.

>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)-

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.

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...

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.

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.

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

"Maybe you want to launch missiles. It's a lisp, not Haskell"

Reply on news.ycombinator.com