Comment by munchler
2 years ago
> I think the main thing that I find compelling about shen is its type system, especially its sequent calculus system (for defining types in a way that would not be possible for most languages).
That sounds interesting. Can you give an example of a type defined this way that would not be possible in most languages?
One quick example is that the language allows for (nearly) arbitrary computation in the definitions of types, i.e. defining an enumeration/sum type of the employees of a company as:
{datatype Employee
______________________
emp : Employee
}
where the enumeration type contains a case for each employee listed in the text file.
The concept is similar to algebraic datatypes where user defined types are created from sum and product types in combination. However, in Shen the Sequent Calculus based datatypes are definable and constructable using any well formed sequent. Then add on the computational content of the sequent clauses to that and you get a system that is wildly expressive.
Note: this is all of extremely interesting, extremely powerful, and extremely cursed! But I think it is certainly interesting food for thought
Why cursed? Why a neat CSV file can't serve as a part of the source three, while a much more cursed pass with `cpp` to handle `#include`, `#ifdef` and such is seen as okay, even e.g. in the Haskell community?
3 replies →
That’s pretty cool. Any other examples? Actor framework equivalent ?
check out https://shenlanguage.org/learn.html, especially
"Coding a Lisp Interpreter in Shen by Mark Tarver", "Shen Tutorial: Sequent Calculus by Neal Alexander", and " Defining Types in Shen by Chris Double" - these all illustrate what is going on in different ways.