Skip to content

A simple type checker written in hare, which can cope with parametric types.

Notifications You must be signed in to change notification settings

Cramblioni/tyche-hare

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

3 Commits
 
 
 
 
 
 
 
 
 
 
 
 

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

No packages published