Tillmann Rendel

Release

1

We should release this (without any stability or correctness or other guarantees). - [ ] write release announcement - [x] check if compiles with current haskell platform

- When a source file has line pragmas, the code snippets in error messages are taken from the wrong file. - If a line pragma changes the current line number...

Support postulates.

10

Postulates would be convenient for rapid prototyping.

Implement abstract exports

4

Maybe it would be nice to export some identifiers abstractly, that is, export their name and their type but not their value. Example usage: ``` module Natural; Natural : *...

Print binders using multiple arguments

1

Support the syntax from #15 in the pretty printer. We already have the various chains in `PTS.Pretty`.

Specify PTS instances with external DSL

5

Users should be able to specify PTS instances without having to recompile any Haskell code. The hard part is to invent a syntax to express infinite instances.

The `PTS.Transform.transform` function should support transformation of lists of statements, not just terms.

The `PTS.Transform.transform` should provide a command-line interface for transforming files, not just stdin. Benefit: More uniform interface, easier to call from scripts in some situations, better error messages.

Support non-ASCII characters?

1

Jenkins reported: ``` Changes: [Tillmann Rendel] Add examples about Church numerals (see #21). [...] + dist/build/tests/tests --hide-successes --maximum-generated-tests=10000 --jxml=junit-log.xml tests: examples/ChurchNumbers.lpts: hGetContents: invalid argument (invalid byte sequence) Build step 'Execute...

Test whether we detect errors

1

Our tests focus on detecting well-typedness. We should also test for detecting ill-typedness. Was mentioned in the discussion of #21. Maybe some variant of the `assert` statement could be introduced...