View on GitHub

tiper

Type Inference Prototyping Engine from Relational specifications of type systems

TIPER aims to automatically generate Type Inference Prototyping Engine from Relational specifications of type systems. Our goal is to build a practical framework called TIPER that automates type system implementations just as parser implementations are automated by parser generators, ever since Yacc was developed in the 70’s. Such a framework will reduce the high-cost of type system implementations supporting type inference so that advancements in type systems research would become much more available to the developers as a cost-effective technology to support in a language implementation. You may take a look at the talk slides on TIPER if you are interested in further details.

In our preliminary case study, we have demonstrated that Logic Programming (LP) is suitable for declarative & executable specifications of polymorphic type systems including advanced features such as type-constructor polymorphism (a.k.a. higher-kinded polymorphism) and kind polymorphism, in addition to type polymorphism in the Hindley–Milner type system (HM). Because our specification is relational, rather than functional, we were able to specify both type checking and type inference without duplication. Being based on LP, our specification is excutable on a machine. Executable specifications reduce the gap between a specification and an implementation. Our specification is not only executable for testing the result of type checking but also serves as a reference implementation for a type inference engine, because the specification can run both ways bidirectionally as a logic program.

Proof-of-Concept Interactive Examples

Here are some examples from our FLOPS 2016 paper made accessible (and also refined, more celaned up than the code in the paper) via online SWI-Prolog environments. You can do simple experiments within these webpages, without installing SWI-Prolog on your local system.

Future Plans

Supportive Partners, Collaborators, and Contributors

Let us know if you should/want to be on this list for your contribution.


[.. ⮥] (back to homepage)