search

quangis / transforge

Describe processes as type transformations, with inference that supports subtypes and parametric polymorphism. Create and query corresponding transformation graphs.
GNU General Public License v3.0
2 stars 0 forks source link

Formal properties of type inference system & connection to other systems #83

Open nsbgn opened 2 years ago

nsbgn commented 2 years ago

The type system for this library was developed to accommodate the needs of the CCT algebra. Due to this, I did not develop it as a formal system first, but rather as an ad-hoc improvement to/replacement for existing machinery for the algebra.

It is clear now that the CCT algebra has non-trivial needs --- complex typeclass constraints --- that would benefit from the formal rigor and community effort behind dedicated inference systems like Agda, Coq, or Isabelle.

On the other hand, as far as I can see, ours is a stand-alone and easy-to-use type inference system within the Python ecosystem, and so it is better suited to our needs than anything else, especially since inter-process communication to the aforementioned seems less than ideal (https://blog.janestreet.com/using-python-and-ocaml-in-the-same-jupyter-notebook/ looks possible though).

However, this DIY approach means that we don't have any proofs on its computational properties. Also, even though it was inspired by Traytel et al 2011, it is by no means the same, so establishing a connection to it and other extensions to HM would be a good idea.

For Coq: https://softwarefoundations.cis.upenn.edu/current/lf-current/toc.html, https://www.cs.umd.edu/~rrand/cufp_2015/

nsbgn commented 1 year ago

There is a Python interface to Isabelle. Also one for Lean, and some more for Coq. Of these, I think Lean looks nice. There's some support for subtyping in community libraries.