Skip to content

Latest commit

 

History

History
80 lines (68 loc) · 5.51 KB

index.md

File metadata and controls

80 lines (68 loc) · 5.51 KB

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.

  • [Simply-Typed Lambda Calculus (STLC)
  • Hindley--Milner type system (HM):
  • HM + type-constructor polymorphism + kind polymorphism:
  • HM + tycon poly + kind poly + (non-nested) pattern matching + Mendler-style recursion over algebraic data types:
  • HM + tycon poly + row poly (for extensible records)

Future Plans

  • Error handling and parser integration.
  • Support more features
    • term indices (as in Nax)
    • first class polymorphism and modules
    • Generalized Algebraic Data Type(GADT)s
    • qualified types such as type classes
    • null-handling (as in Kotlin)
    • measures of unit
    • ... (and maybe more including OO-related features) ...
  • Research/case-study on alternative LP semantics including S-resolution, which may be better suited for type checking/inference.
  • Implementation based on an embedded DSL for LP such as micro-Kanren. (This will lift the dependency on SWI-Prolog and make TIPER possible directly target many other languages where Kanren has already been implemented.)
  • Plug-ins for IDEs and scriptable editors, which are do neccesarily depend on a specific compiler/interpreter implementation. This will be possible at a stage when we produce a mature (easy-to-use & portalbe) version of TIPER.

Papers and Talks related to TIPER

Supportive Partners, Collaborators, and Contributors

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

[.. ⮥] (back to homepage)