← Back to context

Comment by throwaway17_17

2 years ago

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

  if (element? emp read-file “employee_list.txt”)

______________________

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.

7 comments

throwaway17_17

Reply
JoelMcCracken  2 years ago

Note: this is all of extremely interesting, extremely powerful, and extremely cursed! But I think it is certainly interesting food for thought

  • nine_k  2 years ago

    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?

    • JoelMcCracken  2 years ago

      Well, first off, I don't think those things in haskell are good, really. They are/were necessary because of various _other_ issues, but they are not "good" features. And e.g. template haskell doing arbitrary IO at compile time is famously a cause of a variety of unintended problems (e.g. can't cache correctly if you never know what things a TH-module depends upon, very hard to cross compile if you can't be sure the arbitarary TH logic isn't depending upon the compilation host architecture to make some decision for compilation target, etc)

      Specifically though for Shen, what causes me pause is how frequently this kind of "call an arbitrary term-level function in the type system" is done; it is quite frequent, and thus all my mental alarm bells sound. Debugging issues that arise in things like this can be quite challenging.

      Sharp/dangerous tools are often necessary, but what I find unfortunate is that you need to use those sharp tools constantly, when a safer tool could do just as well!

      2 replies →