[package] [Java implementation] [Execution output]


Lists


/**
 * Church's "a[i]" syntax is syntactic sugar for, and equivalent to, both "get(a, i)" and "a.get(i)".
 * Each of these three forms may appear both in an expression or on the left hand side of a function definition.
 * <p>
 * For the purposes of allowing more general applicability of the get method and its associated syntactic forms,
 * we define "get(a, i)", as follows:
 *
 * @param   a the collection
 * @param   i the index of the element to be returned
 * @return  the i'th element of the collection
 *
 * Here 'collection' is a more general concept than that encapsulated by the "get" method defined in java.util.List --
 * which provides an abstraction over all types of List. The extra generality here allows the same syntax, and indeed
 * the same generic function, to be applied to Lists, native Java arrays -- or any other type for which an
 * implementation is available in the current compilation context.
 * <p>
 * The type of the collection, given below as 'C<T>', is typically referred to as 'higher-kinded' by the functional
 * programming community. The signature says that we don't know the type of collection: it might be a
 * java.util.List<T> or Array<T> (which would be written as T[] in Java) or something else. In general,
 * each of its elements will be of type T, and the result of the "get" method must also therefore be of type T.
 * <p>
 * Higher-kinded types are supported internally by Church's type system, but are not permitted as valid Java
 * generics, and so must undergo a transformation before being emitted as Java source code.
 * The transformation process results in legal, statically-typed Java sources that don't have higher-kinded types.
 * <p>
 * In the case of the "get" method, there is no legal Java syntax for the generic type "C<T>", nor is there
 * a way to refer to the functor that produces Java array types. To avoid these two problems, Church's type system
 * instantiates the higher-kinded type (e.g. java.awt.Button[]) and outputs source code for the instantiation,
 * rather than the abstraction, which a Java compiler can then type-check w.r.t. the Java Language Specification
 * in the usual way.
 */
abstract <C, T> T: (C<T>: a)[int: i];