1. 39

  2. 5

    I wonder if the author has heard of Shen

    1. 12

      Given its dubious licensing history and bizarre current licensing statement, I’d advise them to avoid even reading any of the Shen sources, just in case.

      1. 3

        It’s currently BSD licensed, so even if future versions change licenses, the current version is permanently free.

        Mark Tarver in his ivory tower never really “got” FOSS culture, but his initial license was free-ish even if it was weird. I’m glad he was talked into BSD.

        1. 13

          It’s currently BSD licensed, so even if future versions change licenses, the current version is permanently free.

          The current licensing statement is a BSD license coupled with an explicit non-grant of permission to distribute under the GPL. Since the BSD license includes permission to distribute under the GPL the statement is incoherent and as such I wouldn’t want to rely on it - who knows what a court might say?

          1. 7

            Ugh, really? It seems he still doesn’t get it.

        2. 1

          Mark Tarver actually makes a reasonable case against the GPL here. I’m not sure if Tarver is necessarily correct, but his ideas at least aren’t “bizarre” or “dubious”.

        3. 1

          Is Shen ready for usage? I couldn’t even find out how to install it.

          1. 6

            It’s certainly ready for tinkering.

            tl;dr of the layers:

            • Shen is an optionally-typed lisp with a built-in prolog DSL.
            • Shen is compiled to Horn clause logic (similar to prolog) and this is where type-checking proofs are executed.
            • The Horn clause logic is compiled-to/implemented-in a very minimal lisp called “k-lambda”.
            • K-lambda is extraordinarily minimal and not meant to be written by hand. If you implement k-lambda, you get the rest of Shen “for free”.
            • The canonical k-lambda implementation is Mark Tarver’s Common Lisp one, but the community has written many others: Java, Python, Ruby, etc.
            1. 1

              You basically just answered my question about a clean-slate implementation. As in, such a minimal LISP using things like Prolog should be really easy to code for a LISP developer. Based on hga’s comments, I’d say just create a new one that’s full BSD or especially GPL.

              1. 3

                Easy enough conceptually. The stack is a cool innovation which deserves to be mimicked, but the greater part of Mark’s work with Shen is with the type checker, based on something called Sequent Calculus which I do not understand in the slightest. Reading Shen’s history, the story of Shen is really a story of the sequent calculus-powered type checker.

                You can find more detail in The Book of Shen. Here is the pdf table of contents. The type checker is discussed in chapters 24 and 25.

                1. [Comment removed by author]

                  1. 3

                    Yeah. I think language implementations need to be non- or weak-copyleft because rightly or wrongly corporations are scared of the GPL and unwilling to contribute to GPLed projects. Of course that leaves open the question of who stands to make any money from implementing languages, and how.

                    1. 3

                      We can also consider a LGPL with static linking allowed. They contribute any changes to library itself back to it but are otherwise isolated from the problems. Heard MPL does that but I haven’t read it carefully. Might get the companies used to that.

                      1. [Comment removed by author]

                        1. 2

                          I haven’t met a viral copyleft license that wasn’t complicated.

                          Not a lawyer, but my understanding of the MPL is that it is source-file-based, whereas GPL and LGPL focus on compiled binaries and linking. I have no idea how the GPL applies to interpreted languages such as Javascript, but MPL continues to make sense in that context.

              2. 5

                At the top of the page there’s a download link to several flavors. http://shenlanguage.org/download_form.html

                Apparently downloading it is complicated because it has so many possible implementations.

              3. 1

                I wonder if Shen finally checks pattern matching exhaustiveness during type checking.

                1. 4

                  The Shen type system is designed to be open, not closed (which is necessary for exhaustive checks). But can write your own algebraic type system on top of Shen which does pattern matching exhaustive checks, see this thread

                  1. 3

                    There are three problems with your linked thread:

                    • The original question in it has nothing to do with exhaustive case analysis. (It’s about providing multiple implementations of the same abstract operation.)
                    • The answer defers the details of how to embed Hindley-Milner into Shen to The Book of Shen, which unfortunately isn’t freely available.
                    • In any case, my question wasn’t about Hindley-Milner. A language with no type inference can also have guaranteed-exhaustive case analyses. (Recall that global type inference is one of the defining features of Hindley-Milner.)

                    My use case is as follows: I’m writing a library of data structures and algorithms, together with (manual) proofs of correctness of their implementations. I have the following design constraints:

                    • Unreachable control flow paths are forbidden. Inexhaustive pattern matching, raise ThisWontHappen, calling partial functions (List.hd, List.tl), returning dummy values and deliberately looping forever in a routine supposed to terminate are all symptoms of this problem. Enforcing this policy requires a strict division of labor between the type checker and myself: the type checker ensures the exhaustiveness of my case analyses, and I prove that each case has been dealt with correctly.

                    • Unrelated concerns must be dealt with separately. For example, in a search tree implementation, there are two unrelated concerns: how to prevent trees from becoming too unbalanced, and how to ensure that the in-order traversal of any tree produces a monotonic sequence. The former depends on the internal representation of trees, but the latter only depends on the ability to perform step-by-step binary search and insert/update/delete an element at the current position. Thus, the latter must be implemented once and only once, in a manner agnostic to the details of the internal representation of trees.

                    • Finally, economy of effort. Ceteris paribus, simpler programs and proofs are preferable to complex ones. Also, the aforementioned division of labor must be tailored to exploit the strengths and avoid running into the weaknesses of each party. Computers are much better than humans at exhaustive enumeration, but humans are better than computers at equational reasoning (computers can get stuck exploring an infinite space of applicable rewriting rules, where human insight would let you pick the right one).

                    These constraints have pretty much forced me to pick between Standard ML and OCaml. (But note that Hindley-Milner type inference was not a factor in the decision!) I ultimately picked Standard ML because its treatment of equality and recursive values is less wonky.