I love Shen and highly recommend the Book of Shen and Tarver's other book on Logic and Computation.

The crazy thing about Shen is that its type system is sequent calculus, which means when you define your types, you are literally writing the same language that mathematicians use when they prove things about type theories.

Why would you use it? Because you can leverage a crazy amount of power by writing your own type theories in your programs.

Is it practical in today's corporate world? Probably not, but there is at least one case study in the real world https://www.youtube.com/watch?v=lMcRBdSdO_U

Thank you for the link to the talk! I'll watch it for sure.

If I am interesting in using functional languages (currently F#, Elixir, and Racket) to explore GUI systems, graphics, symbolic math, numerical computing like machine learning and swarm algorithms and automatic differentiation, agent-based modeling, fractals and general chaos theory stuff, etc., is Shen a good match for that type of exploratory, almost from first principles but towards something that is actually usable work?

Is Shen closer to Scheme or Lisp? I typically fall in the Scheme side of things a la Racket.

Thanks for all the information and help!

Definitely usable for those cases. You might have to do some extra work to build the necessary libraries though.

It’s closer to scheme I think, being a lisp-1, even though it’s originally implemented in Common Lisp.

Thanks! And I watched some bits of that talk and got excited about the whole KLambda thing and the ability to use Shen hosted on top of another platform. That seems very interesting to me, especially since Shen has Prolog inside it, and is something I'm going to look into more.

Shen does something unusual in deployment. Their idea is to write a smallish number of intrinsics and data structures in your main language, and then import the shen interpreter on that. This gives you code written in shen, callable from the host language.

This is interesting for sharing code across multi-language projects, e.g. as a JavaScript library and a Java one, where the shen interpreter gets written once per language and now all your library code is callable from any of them.

I think it's a minor misfire that this is an interpreter, as opposed to a compiler from shen to whatever language, but that would be fixable. I'd rather compile the shared definitions to raw c++ code ahead of time than run an interpreter.

Aside from that, the definition is mostly in shen (modulo said primitives) so it has an axiomatic angle to it, and the type checker is a prolog. Compiler and prolog engine both available to user code of course.