Skip to content

solving guide

JohanWiltink edited this page May 3, 2022 · 5 revisions

Lambda Calculus Kata Solving Guide

Syntax

S = \ x y z . x z (y z)
K = \ x _ . x

# comment
random-example' = ( \ arg _unused . arg \ x . x ) \ x . x

Identifiers can be named as in the Syntax Guide ( qv. ).
Indentation signals a continued definition.
Lambda abstraction arguments can be contracted.
Abstractions extend as far right as syntactically possible.
Application is left associative.
Abstractions and applications only need parentheses to override precedence.
Whitespace is required to separate identifiers and to indent lines that continue the current definition, and optional everywhere else.
# starts a comment. ( This may change to # in future, when # without whitespace may become compiler directives. ) \n ends a comment.
#debug toggles strict mode for syntax highlighting. By default, it is set to unstrict. debug should be directly at the start of the comment, and may have trailing other text.

Undefined

() is undefined and must not be evaluated.
Any name starting with _ always has the value undefined and must not be evaluated.
For performance reasons, use undefined names for lambda abstraction arguments that are not used. ( Optimisation is planned but not yet implemented. )

Encodings

Kata should leave you as free as possible to use encodings of your choice. Number encodings will probably be specified ( because the compiler supports certain number encodings ). Other necessary encodings may require you to export constructors ( for input values ) and / or deconstructors ( for output values ).

Boolean constructors are False, True; deconstructor is if.
2-Tuple constructor is Pair; deconstructors are fst, snd.
List constructors are nil, cons; deconstructor is foldr.
Option type constructors are none, some; deconstructor is option.

Exporting these (de)constructors allows you to use any encoding you want, while allowing kata authors to define unambiguous wrappers for testing. The Encodings Reference ( qv. ) has possible encodings ( and specifications of numeral encodings ).
Unless and until a standard library is published, you may want to develop your own reference implementations of ubiquitous encodings, with constructors, deconstructors, and helpers.

Verbosity

LC.configure can be used to set compilation options. purity and numEncoding should be left to whatever the kata set, but verbosity can be adjusted, to generate more debugging output. Options are "Calm", "Concise", "Loquacious", "Verbose" ( in that - alphabetical - order ). Higher levels will generate increasingly detailed progress messages during parsing, as well as increasingly detailed Error messages on any failure.

Clone this wiki locally