Tethys

License Discord Lines of Code

Tethys is a toy functional programming language based on a System F-based core calculus.

This language is mostly for learning about type systems, but I am going to make it into something half-fleshed (as opposed to fully-fleshed). It's not going to be efficient (most likely), but it will be a good learning experience.

Note that this code is very work-in-progress. Contributions are welcome (and encouraged!), but it's likely that as a toy langauge, this will never be in a state that is helpful or efficient to use in production. If you want a language that will (eventually) be robust (enough), see Calypso.

Example

The following example is an implementation of FizzBuzz up to 100. This is also available at support/examples/fizzbuzz.tys. Note that this is currently pseudocode, though it will likely not change much by the time most features are implemented.

def main
 : () -> ()
 = \_.
 each (fizzbuzz 100) println
def fizzbuzz
 : Int -> List[String]
 = \max.
 map (rangeI 1 100) (\n.
 if (divides n 15)
 then "FizzBuzz"
 else if (divides n 3)
 then "Fizz"
 else if (divides n 5)
 then "Buzz"
 # Typeclasses soon(tm)
 else intToString n)

Internals and Motivation

There are two parts of Tethys: the surface language, and the core calculus. The core calculus is the intermediate representation of Tethys which is used for type checking and inference, and for interpretation. The surface language is the higher-level interface that is eventually desugared by the compiler/interpreter to the core calculus.

The reference implementation in Haskell will probably not use any particular "tricks" in terms of interpretation (VM, JIT, AOT compilation to native, etc.), instead just using a simple tree-walk interpreter or similar. (At some point, it may end up compiling to Calypso's SaturnVM.)

This language was created in order to conduct informal research (i.e., not actually discovering anything interesting, probably) on type systems, especially bidirectional typechecking and polymorphism. Tethys is named as such as it is the name of the co-orbital moon to Calypso; as my work on this language is "co-orbital", so to speak, to my work on Calypso.

More information on Calypso (the language, of course) is available at https://calypso-lang.github.io.

This implementation is partially based on an implementation of bidirectional typechecking with unification of higher-rank polymorphism created by Mark Barbone (aka MBones/mb64). A slightly modified version of this implementation is available at support/tychk_nbe.ml. The original is available in this Gist.

Additionally, this implementation is based on an algorithm described by András Kovács in their elaboration zoo. Further inspiration comes from Bálint Kocsis's SFPL. The core algorithm, created for dependent types but made specific to System F, is available in support/typeck.

A list of resources and bibliography used to make this is available in the paper. Note that this list is not necessarily up to date. I'll try to update it as soon as I can, when I use new resources.

"Paper"

The source for the "paper" (really just a typeset informal writeup) is in paper/paper.tex (requires pdftex). At some points there may be a PDF in the repository but there is no guarantee that it is up-to-date with the LaTeX source.

Contribution

I have yet to draft up a CONTRIBUTING.md. If you'd like to contribute and don't know where to start, feel free to open an issue, ping me on Discord or contact me elsewhere. I'll let you know if there's anything I think you can help with, and if so give you some pointers. Contributions are greatly appreciated!

There is a semi-functional VSCode extension / TextMate grammar in support/highlight. It's not perfect, but it works well enough.

Repository Overview

• paper/: Source and occasionally PDF for the "paper" (really just a typeset informal writeup). See this section for a bit more information.
• support/: Support files, including grammars, examples, tests, etc. See its README for a bit more information.

License

This project is licensed under the BSD 3-Clause license: LICENSE or https://spdx.org/licenses/BSD-3-Clause.html.

Contribution

Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, shall be licensed as above, without any additional terms or conditions.