Church

Church is a very small statically-typed language that is designed to run on: the Java Virtual Machine, in browsers and natively. It is supported by a compiler that performs source-to-source translation into languages that have direct support on the host platform. It currently only runs on the Java VM, where it translates Church sources to type-safe Java source code. Church's static type system is sound which allows Church programs to be directly translated into efficient native languages like C.

Examples

There is a directory of example code here. The examples reference the Church run-time library, whose sources are here. The corresponding translations to Java source code are available from the "[Java implementation]" link at the top of each HTML rendering of the Church sources.

Specific examples:

ComplexIntegerTest and it's associated Java translation show how polymorphism works in Church
LinkedList: shows a Church abstract data type; its Java translation shows how abstract types are mapped to the visitor pattern
SetExample: shows how equals and hashCode methods are captured during set construction
ChainedCalls: shows how native Java classes are referenced with some different forms for calling Java methods
Derivative: and the other files in this package show how primitive pattern matching can be used to perform symbolic computations

The same examples can be downloaded and run locally from the corresponding church-examples project on GitHub. The project has a README.txt file in its root directory which has instructions on how to edit, compile and run the Church sources in the project.

Downloading the SDK

SDK: download.

Influences

Church's primary influences are from:

Java: for general language conventions
Haskell: for its type system
LISP/Scheme: for the smaller-is-better approach to language design
Groovy: for its ability to augment third-party classes with new methods
Python: for its prioritization of syntactic terseness

What's new?

By way of orientation, here are the key differences between Church and:

Overview

Licensing

The compiler and related libraries are free and will use the permissive Apache 2.0 Open Source Software License

Syntax

core syntax is broadly that which is common to: C, Java and JavaScript

just two additional programming constructs: class and abstract

grammar is 'shallow' rather than 'nested'; so as to be suitable for use as a scripting language or worksheet (R.E.P.L.)
no syntax for creating or referring to null pointers
automatic currying of function calls when required

Type system

formally: static, nominative, safe, sound, strong
no sub-typing
no support for manual coercion from one type to another
uses type-inference to obviate almost all type declarations

Polymorphism

not object-oriented

provided by abstract data types and generic functions

Execution model

fast / efficient as it uses the data structures and operations of the host platform directly

eager evaluation

effected by compilation to type-safe source code
opt-in support for imperative programming:

assignment
operations with side-effects
loops (to appear)

Libraries

has a small cross-platform library (independent of java.lang.Object)

provides access to Java libraries through direct import statements of standard Java classes

Polymorphism in Church

Church's form of polymorphism is based on generic functions, rather than inheritance. Even though this difference seems very fundamental (and it is), Church programs look and work much like Java programs. This is because Church uses similar syntax to Java and uses generic functions to mimic Java's method calling paradigm.

Church unifies the principle of calling a dynamic method with that of making a call to a generic function with an extra parameter. The first translation the Church compiler makes is purely syntactic, along the following lines:

a.foo(b, c) => foo(a, b, c)

[Kotlin also blurs the distinction between these two syntactic forms.] If the function foo is generic, Church's generic function resolution system will then act at each call-site that references foo, to statically construct an appropriate version of the foo method... [it's easier to understand this by looking at the some of the sample sources: e.g.: ComplexIntegerTest.chuch and its associated ComplexIntegerTest.java translation to Java source code].

Dispatching works on the type of the arguments, not on their run-time class. As Church does not support sub-typing, the need for a formal distinction between type and class is much reduced, though arguably not entirely obviated. In all cases, Church's type system guarantees that there are no cases in which a typing error will occur at run-time.