"Part of our motivation in maintaining a tight spec and a reliable platform is to hold the Shen community together so that we do not splinter our resources on multiple incompatible forks. We do not want multiple incompatible dialects of Shen, multiple compilers, multiple incompatible libraries. We want $free readable libraries that work for all of us and libraries we can pick up and use without worrying about compatibility. Hence the production of derivative non-conforming programs from our source, whether called Shen, Shin, Shine or Shoo, is barred by the license. To give up on this is to give up on the motivation for Shen."
Whilst avoiding forking prevents splintering it can also be dangerous. OCaml suffers from a similar restriction which has seriously impeded the development and use of new compiler features like staged compilation (http://www.metaocaml.org/), type-safe marshalling (http://www.cl.cam.ac.uk/~pes20/hashcaml/) and delimited continuations (http://groups.google.com/group/fa.caml/browse_thread/thread/...). INRIA rarely accept new features into official distribution and the license prevents anyone else from doing so. Extensions have to be distributed as patches and inevitably bitrot.
Tying the long-term viability of a language (or spec) to a single owner rings alarm bells for me. Clearly they want to avoid another Scheme but I've had bad experiences in both directions.
Tarver would be better off letting go of his urge to tinker with licenses and just run with one of the existing options. The risk posed by suboptimal licensing is negligible compared to the risk of his radical new language not getting used at all, and every time people get distracted by nitpicking license terms -- as they invariably do -- a significant portion of the tiny and precious attention budget for Qi/Shen gets blown through. This is a shame.
However, there doesn't appear to be an object system or a monad library, and the "lazy evaluation" system uses a typical promise/force approach, which every Scheme has had for decades. So Shen may not be well-suited to the kind of fun tricks available in Haskell and (to a certain extent) Scala. Still, it's definitely an interesting language.
The idea is that Shen has a turing-complete type system, so it shouldn't even be possible to create a more powerful type system (given a specific definition of "powerful").
To expand on that idea a little bit: that's a valid definition of 'powerful', but there's another definition of 'powerful' which some people mean when they talk about type systems, and that's "To what degree does this type system prevent errors?" It seems from cursory research that Shen is powerful with respect to the definition, "To what degree can we encode computations in the type system at compile-time?" and Agda and Coq's type systems are powerful with respect to the definition, "How can we limit the class of programs by encoding constraints in the type system such that the resulting programs are provably correct?" Consequently, neither Agda nor Coq are Turing-complete even at the language level, much less the type level, but that accordingly gives them greater power to know information about their programs at compile time.
I think this may be kind of a question of definitions. Agda and Coq at least are more like DSLs for constructing proofs than general-purpose functional programming languages. I'm not familiar with Epigram, but assuming it's similar to the other two in the list, I think you're redefining his terms for him, which is a little bit unfair.
Nobody said anything about "general-purpose functional programming languages", the blurb says "existing functional languages". All of Epigram, Agda and Coq are functional and currently exist. :) More seriously, Coq is designed explicitly to be a proof assistant, but Agda and Epigram are meant to be programming languages.
Considering it's a port/rewrite of Qi, which uses a Turing-complete interpretation of the sequent calculus, yes, it is more powerful than all those languages.
You're right to be suspicious at extraordinary claims, but the tiniest bit of research gets you the extraordinary answers in this case. I'm quite surprised you know of Agda, Coq, and Epigram, but not Qi.
If Turing-completeness is the kind of powerful you're talking about, then Qi's would be more powerful. However, if you're talking about the amount of things the type system can verify, a Turing-complete type system would be subject to the halting problem, and thus is less powerful in that way.
And it looks like Qi's type system is optional. If your only definition of type system power is Turing completeness, then sure, it's powerful, but it can't accomplish the same kinds of verification as Agda, etc.
Relevant: "When we say that a language is expressive, we mean that it is easy to use. When we say that a type system is expressive, we mean that it is not." - Gilad Bracha
Very true, and awesome quote. It's worth noting though that once you're talking about dependently-typed type systems, it's accepted that you're going to be doing a lot of work with the type system. You're going to be using proof tactics to type your programs. It's almost the point at that point.
in this case maybe not so much. If I recall correctly shen has a pretty tiny core that is designed so it can be ported to existing runtimes, so for example a shen/js could just delegate calling libraries to V8 or *monkey, while shen/scheme can use racket's FFI etc
I agree. It's sometimes a pity that even with full unicode support nowadays we still resort to 'ASCII art' to express syntax in programming languages, reducing legibility. This is not so much a problem of US keyboards, because code editors could easily support the extra characters as part of the language support.
You can just configure your editor to figure out when \x y -> x + y is equal to λx y→x+y and replace the symbols as appropriate.
I have Emacs set up to do this for Haskell, so I really have the best of both worlds (mostly): I can type the former expression but it looks like that latter.
I use RFC 1345 digraphs in vim to type unicode characteres. In RFC 1234, λ is l* and → is ->. To type the above, I just input l_*x y -_>x+y where _ means backspace. This is easy to learn, fast to type, and covers most of the useful unicode characters.
A shame, too. At least decent editors make this a tad easier. DrRacket, for example, binds lambda to Ctrl+\. Racket accepts both "lambda" and "λ" as the same thing, so it's up to personal preference.
I'm well aware of how DrRacket works; nonetheless, telling a newbie to type "lambda" will lead to typing, and telling them to type a lambda will lead to griping.
Also, the difficulty of typing lambdas also means that writing blogs about code, or documents, or emails, will require even more pain.
I'm disappointed that it doesn't seem to stick with Lisp syntax, instead adding a large number of infix operators. I'm reminded of the loop macro, but this is more pervasive since you don't have to use loop.
The syntax is important for being able to write sophisticated macros that take advantage of all the language's features and for making things like genetic programming easier.
The infix operations are mostly syntactic sugar - [3 4 5] is the same as (list 3 4 5), [A|B] is (cons A B), and so on. I don't know about '->' for pattern matching and '<-' for backtracking (maybe others), but you can of course replace '->' by conditionals as is usually seen in Lisp programs not employing pattern matching.
It's the non-open license (forks seem not to be allowed) which is a bit more disappointing. I guess it's a reaction to historic Lisp fragmentation but I doubt this will help adoption.
I'm trying to go through the longer book (on Qi, which has been updated for the most part for Shen) but I'm having a difficult time reading it because every page is saved as a JPG! Magnifying the text just makes it more unreadable... is this 1990?
Edit: The book is quite excellent, including a neat history on why imperative languages are the norm. It's just that my eyes are in pain. :(
"Part of our motivation in maintaining a tight spec and a reliable platform is to hold the Shen community together so that we do not splinter our resources on multiple incompatible forks. We do not want multiple incompatible dialects of Shen, multiple compilers, multiple incompatible libraries. We want $free readable libraries that work for all of us and libraries we can pick up and use without worrying about compatibility. Hence the production of derivative non-conforming programs from our source, whether called Shen, Shin, Shine or Shoo, is barred by the license. To give up on this is to give up on the motivation for Shen."
Whilst avoiding forking prevents splintering it can also be dangerous. OCaml suffers from a similar restriction which has seriously impeded the development and use of new compiler features like staged compilation (http://www.metaocaml.org/), type-safe marshalling (http://www.cl.cam.ac.uk/~pes20/hashcaml/) and delimited continuations (http://groups.google.com/group/fa.caml/browse_thread/thread/...). INRIA rarely accept new features into official distribution and the license prevents anyone else from doing so. Extensions have to be distributed as patches and inevitably bitrot.
Tying the long-term viability of a language (or spec) to a single owner rings alarm bells for me. Clearly they want to avoid another Scheme but I've had bad experiences in both directions.