dbp / pyret-tc

A type checker for the Pyret programming language

How to use

You must have Pyret installed. See github.com/brownplt/pyret-lang.

Next:

git clone https://github.com/dbp/pyret-tc

And then build it:

raco make tc.arr

(This will take a while - on my desktop, it takes ~40 seconds. On a recent laptop, it should take maybe double that.)

Now run:

raco pyret tc-report.arr /path/to/file.arr

Which will print out a report from type checking, listing any errors detected, and any top level functions that it inferred types for based on tests.

Feedback welcome; though it is definitely still a work in progress (so, "it doesn't catch all type errors" isn't useful feedback. A specific error it missed, on the other hand, is.)

Running tests

If you want to run the type checkers test suite (all the programs in the tests directory), you can run:

raco pyret tc-test.arr

Or to run a specific test:

raco pyret tc-test.arr test/functions1.arr

The tests are normal Pyret programs that have information in special comments that specify what errors and warnings, if any, the program should result in.

If you'd like to run the unit tests built into the type checker, you can run:

raco pyret tc-unit.arr

NOTE: This is a hack - tc-unit.arr is just a symlink to tc.arr, because once you raco make tc.arr, if you try to run it, it will run the compiled version, which doesn't have the unit tests. So instead we run the same file with a different name (by way of a symlink) and it all works. If you are on a platform that doesn't have symlinks, this probably won't work, and you can just removed the compiled directory and then run raco pyret tc.arr.

pyret-tc's Issues

Do reverse desugaring-like operation to figure out when binops were being used

I think it's safe to assume that when _plus is being called, it was not written out by hand. So we can make the error messages be binop aware. An example of a bad error is in: tests/numbers.arr

warning when type is Dyn but type is specified

In let bindings, function return types

don't rely on no-shadowing when finding inferred functions

Shadowing is coming (and also, can be turned on with a commandline flag), meaning these are not invariants that should be used.

Unbound types are being reported twice

See tests/data-poly1.arr for an example.

appTypes should have records

So they can have fields. The fields being in the type env might make sense...

basic understanding of import statements

we won't have types, yet, but at least we can bring in the objects so we aren't getting unbound identifier errors.