4 ms·
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 seque
by bsima 3y ago
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 https://www.youtube.com/watch?v=lMcRBdSdO_U
- bmitc 3y agoThank 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!
- bsima 3y agoDefinitely 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.
- bmitc 3y agoThanks! 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.