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.
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)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.
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.
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.
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.
This project is licensed under the BSD 3-Clause license: LICENSE or https://spdx.org/licenses/BSD-3-Clause.html.
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.