(version: 1.1.2)

24 Roadmap

With Cedille 1.1, we have a version of Cedille that provides familiar higher level concepts for datatypes like datatype declarations, constructors, and pattern-matching (histomorphic) recursion. Cedille 1.1 elaborates these down to Cedille Core, a pure type theory without primitive datatypesl This accomplishes a major goal in the roadmap of Cedille 1.0. Future directions are somewhat up in the air at present. One avenue likely to be developed in 2019 is automatic subtyping, which will make certain examples with datatype notations more succinct. The following items are still on the agenda:

• Second-order matching and term inference incorporated into spine-local type inference
• Rebase Cedille on sequent calculus to enable deriving types like existentials as dual to universals, and support constructive control operators

We also plan to continue incorporating high-level syntax for advanced datatype features into Cedille, although exactly which might be up next is currently not determined.