-
Notifications
You must be signed in to change notification settings - Fork 0
Cramblioni/tyche-hare
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
# Tyche (𐑑𐑱𐑗𐑳) Overly simple typechecker written in Hare. ## Tyche's views Tyche is a simple typechecker based on programming langauges like C and Hare. Tyche isn't a proper type checker as it is based on layout typing. The type system used by Tyche can be described as simple and intuitive, though not depthfull. Ideally, concrete types in Tyche refer to how a piece of data is layed out in memory. This includes functions, each function type refers to a specific function. ## Current progress Tyche can currently check single expressions and cannot be integrated with any programming system yet. Function types are implemented as product types. ## More explained ### types and schemes The idea with function types is that they're unique per function. Where a language like C would deem function `fizz` and `buzz` to have the same type of `void (*)(int)`, Tyche would deem them both to have seperate types. Future implementations will give each function type a prototype in order to do useful typechecking. The Typechecker has two layers, concrete types and type schemes. Type schemes are Tyche's way of working with types and capture all of the "during typecheck" behaviour Tyche has. Schemes also store type variables, which are handled with substitutions. Tyche uses an occures check to prevent a variable being substituted with a scheme that contains that type variable. This means Tyche cannot be used for type systems that allow recursive types (It cannot mock a mockingbird). Tyche uses unification to generate substitutions. ### The Opaque API The idea behind how you interface with Tyche is by having type rules that make simple queries to tyche and then assertions to tyche. Tyche Does not need to know the specifics of your system's structure, just the types. This aspect is what led to the justification of the opaque api (named after Hare's `*opaque` type). Various structures in Tyche don't care what they're holding, they just hold it. So, Tyche holds pointers to what you manage. Tyche will use these as identifiers and some API endpoints will return them. A quick note, this isn't a webdev style endpoint, "endpoint" is used to refer to the ABI method calls that will be called via API methods. The API shouldn't be seen as trivial, but as a partial implementation. There are a few methods Tyche expects, and these must be implemented. ## Plans/TODO - [ ] Implement opaque API - [ ] Type Pool - [ ] Type Context - [ ] Implement schemes
About
A simple type checker written in hare, which can cope with parametric types.
Resources
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published