Domain-specific type systems in the church and curry formalism

Currently there are two main methods for constructing type systems for lambda calculus: following the Church approach and following the Curry approach. In systems based on the Church approach, terms represent annotated versions of untyped terms. Each term has a type, which is usually unique (up to an equivalence relation) and is derived from the term annotation. In the typed lambda calculus à la Curry, each term has a set of possible types. This set can be empty, singleton, or consist of several (possibly infinitely many) elements. Aim of article to present a method for constructing type systems with different approaches, highlight their advantages and disadvantages, and to determine the possibility of their application for constructing a domain-oriented type system when constructing practical applicative systems.

A method for constructing type systems based on different approaches is presented, and recommendations for their application in constructing a domain-oriented type system are given. The results of the work can be used in the selection or construction of an tooling system to support practical applicative systems.