Issues and Inklings

This page is intended to be common property, a collection point for issues which Epigram might benefit from addressing and inklings as to how we might address them.

Datatypes

  • Locally defined datatypes
  • Coinductive datatypes
  • Mutual datatypes (including mixed induction and coinduction)
  • Induction-recursion
  • Mutual telescopes of datatypes

But it’s not just a question of which datatypes we’re allowed, there’s also room for improvement in the generation of datatypes.

  • Datatypes in a universe
  • Refinements of datatypes
  • Datatypes generated for reflection, defunctionalisation, collection of unfinished cases
  • Refactorings of datatypes

Computations

Life’s no fun without a little impurity here and there. Haskell’s monads are all jolly well, but there’s so much more waiting to be found. We get to think it out again. I’d like to see a situation where more syntax is spent on establishing which effects are locally available and less on plumbing effects through expressions. Half an idea: work with respect to a local ‘notion of computation’; spend syntax on shifting aspects of computation between explicit types and the ambient notion; retain the ordinary syntax of expressions but allow locally sanctioned effects. Turn ‘do’ back into ‘let’!

Leave a Reply