Defining Types in Shen

DRANK

The Shen programming language has an extensible type system. Types are defined using sequent calculus and the system is powerful enough to create a variety of exotic types but it can be difficult when first starting with Shen to know how to use that power. In this post I hope to go through some basic examples of defining types in Shen without needing to know too much sequent calculus details.For an overview of Shen there is Shen in 15 minutes and the Shen OS Kernel Manual. An interactive JavaScript REPL exists to try examples in the browser or pick on one of the existing Shen language ports. For these examples I'm using my Wasp Lisp port of Shen.Shen is optionally typed. The type checker can be turned off and on. By default it is off and this can be seen in the Shen prompt by the presence of a '-' character:(0-) ...shen code... Turning type checking on is done by using (tc +). The '-' in the prompt changes to a '+' to show type checking is active. It can be turned off again with (tc -…