Skip to content

authoring reference

Jump to bottom
JohanWiltink edited this page May 3, 2022 · 7 revisions

Lambda Calculus Kata Authoring Reference

LC

import {assert,config,LC,getSolution} from "./lc-test.js" imports 6 things:

  • chai.assert as assert
  • chai.config as config
  • LC = { compile, configure, fromInt, toInt, Primitive }
  • getSolution, getPreloaded and getSolutionWithPreloaded

getSolution and friends

getSolution() returns the user Solution code, getPreloaded returns the author Preloaded code, getSolutionWithPreloaded() returns a safe version of Preloaded and Solution code, concatenated.

compile

LC.compile(getSolution()) ( or a variant ) returns a JavaScript Object with all top level definitions from the compiled Lambda Calculus source code, which can be destructured.

const solution = LC.compile(getSolution());
const { "is-empty": isEmpty } = solution;

Destructuring can be performed multiple times to avoid overly long lines, and keys can be renamed to comply with JavaScript identifier name restrictions.

Note that definitions can be overwritten; for multiply defined names only the last definitions will be exported, but other definitions always use the definition of a name at the time of their own definition.

Because solvers can also overwrite Preloaded definitions, do not rely on solver exports from LC.compile(getSolutionWithPreloaded()); always ( ALWAYS! ) get those exports directly from LC.compile(getPreloaded()), or define them as LC-encoded JS values in Testing.

configure

Default configuration is

{ verbosity: "Calm"                  //  Calm | Concise | Loquacious | Verbose
, purity: "PureLC"                   //  Let | LetRec | PureLC
, numEncoding: "None"                //  None | Church | Scott | BinaryScott
, enforceBinaryScottInvariant: true  //  Boolean
}

LC.configure is called with a JavaScript Object with the desired new setting(s), eg. configure({ purity: "LetRec" }). Unnamed settings are unchanged.

Currently, solvers can only change the configuration for Example testing, by editing the test suite directly. A syntax extension with compiler pragmas to allow solvers access to configuration is being considered; there will then also be configuration options to forbid particular configuration changes by pragma ( you probably don't want solvers to change numEncoding ).

verbosity controls the amount of debug and error information displayed. It is recommended to set verbosity to at least Concise for Submit testing.

purity controls both if defined names can be used in later definitions ( in PureLC, they cannot; in Let and LetRec, they can ), and if self-recursion is allowed in definitions ( only in LetRec ). In PureLC, solvers will have to apply lambda abstractions to define names for their own use. Below LetRec, solvers will have to implement recursion themselves explicitly.

numEncoding controls what number encoding is transparently used by the compiler. This may also be used in assert.equal but will not be recognised by assert.deepEqual. In general, authors will have to encode and decode values other than numbers ( booleans, arrays, tuples ) explicitly. There are currently no plans to support any values other than numbers in the compiler syntax.

enforceBinaryScottInvariant controls if toInt checks BinaryScott numbers for zero-padding in violation of the invariant that the MSB, if any, is a 1. This is ON by default. Note that solutions can use padded numbers internally; the check occurs only when a number is tested, ie. exported to JavaScript. No other number encodings with invariants have been defined ( yet ), so no checking is done for them.

fromInt, toInt

fromInt is called with a JavaScript Number and returns a Lambda Calculus expression for the number, in the active encoding ( configure().numEncoding ), compiled to a JavaScript Function.

toInt is called with a JavaScript Function equivalent to a Lambda Calculus expression, and returns a JavaScript Number for the expression, decoded according to the active encoding.

These functions are used by the compiler itself for transparently compiling JavaScript Numbers in Lambda Calculus source code, but they can be called directly from testing code.

Invoking configure({ numEncoding: { fromInt() {}, toInt() {} } }); allows an author to specify a custom number encoding. This encoding will then also be used by the compiler.

Primitive

JavaScript Numbers ( not BigInts ) that are ( in testing ) passed to compiled LC functions will automatically be converted to LC values according to the numEncoding in effect. This behaviour can be disabled by wrapping the Number in Primitive, eg. ifThenElse (boolean) ((LC.Primitive(1)) ((LC.Primitive(0)) will return a JS Number; without the wrapper, it would return a numEncoded LC value.

assert

assert is standard chai.assert extended with assert.numEql.

assert.numEql(actual,expected,message) will automatically decode ( according to the active numEncoding ) actual to a Javacript Number for comparison to expected and failure messaging, obviating any need for explicit decoding.

assert.equal, .strictEqual, .deepEqual, with explicit decoding, are still to be used for comparing values of other types.

what is in what language, what syntax, what encoding?

Kata author Preloaded code and solver Solution code are Strings in Lambda Calculus syntax. Separately compiling Preloaded code means its definitions are inaccessible to Solution code and is probably abuse of the Preloaded mechanism; this code should be in Testing, possibly precompiled. Explicitly importing Preloaded definitions into Solution code ( with a compiler pragma ) is under consideration as an extension of the current syntax.

LC.compile compiles Lambda Calculus code to JavaScript Functions. There is a one-to-one correspondence between Lambda Calculus syntax and JavaScript syntax, and everything that comes out of compile is JavaScript, and is a callable Function. It can be applied with native JavaScript Functions, with compiled Lambda Calculus terms ( thus JavaScript Functions ), or with other JavaScript values, which will pass uncompiled. Thus, everything that happens in testing happens in JavaScript.

The only way to arrive at JavaScript values from compiled Lambda Calculus code is passing its compiled form a JavaScript value in testing; there is no way to embed JavaScript values in Lambda Calculus code - not even passing it Numbers, which will be transparently encoded ( or generate an EvalError, when numEncoding = None ).

Note that there are no Strings in Lambda Calculus syntax, though you can pass and manipulate Strings in testing ( ie. in JavaScript ).

Also note that all passed Numbers will be transparently encoded, which will generate a RangeError for negative numbers in most numEncodings. Numbers wrapped in Primitive ( qv. ) will be passed unchanged.

Leave solvers free to use encodings

numEncoding is designed to set a particular numeral encoding for the kata, and provide support for testing with that. Other encodings however should be as free for solvers as possible. Use constructors and deconstructors in wrappers for testing, and allow solvers to export their own (de)constructors for datatypes other than numbers.

For booleans, ask for False, True : Boolean and if : Boolean -> z -> z -> z ( \ if (boolean) (true) (false) . result ).
For 2-tuples, ask for Pair : x -> y -> Pair x y and fst : Pair x y -> x, snd : Pair x y -> y.
For lists, ask for nil : List x, cons : x -> List x -> List x and foldr : (x -> z -> z) -> z -> List x -> z.
For streams, ask for cons : x -> Stream x -> Stream x and head : Stream x -> x, tail : Stream x -> Stream x.
For option types, ask for none : Option x, some : x -> Option x and option : z -> (x -> z) -> Option x -> z.

E.g.

const { foldr } = solution;
const toArray = xs => foldr ( x => xs => [x,...xs] ) ( [] ) (xs) ;

xs is an LC value here; toArray(xs) is then a JS array that can be tested ( don't forget the elements are encoded as well! ).

Refer to the Encodings Reference for naming conventions.

Clone this wiki locally