{ "cells": [ { "cell_type": "markdown", "metadata": {}, "source": [ "# A short introduction to the typed lambda calculus in the Lambda Notebook\n", "\n", "### Notebook author: Kyle Rawlins\n", "\n", "This notebook introduces the typed lambda calculus in the context of the Lambda Notebook. It presupposes some knowledge of how similar formalisms are used in compositional semantics. It also isn't intended to generally introduce the lambda notebook's metalanguage.\n", "\n", "_Note_: Run all on this notebook will be blocked by a purposefully generated exception in the middle." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "In formal semantics, compositionality is typically modeled by the interaction of (potentially higher order) functions, and this interaction is guided by syntactic structure. Functions are typically characterized using a typed lambda calculus. An untyped lambda calculus uses representations like \"$\\lambda x \\: \\alpha $\" to characterize a function that given some $x$, returns $\\alpha$. A typed lambda calculus uses a system of types to place constraints on both $x$ and $\\alpha$, effectively describing the domain and range of the function explicitly. (Often, types are actually defined in terms of sets, but here I will not do that, as the lambda notebook takes them as primitives.)\n", "\n", "### Types\n", "\n", "The two core types in (extensional) formal semantics are $e$ (for entities), and $t$, for truth-values. A functional type is always a pair of types, with the left member specifying the domain, and the right member specifying the range. An inductive definition of (simple) types therefore often takes this form:\n", "\n", " 1. **Atomic types:** $e$ and $t$ are types.\n", " 2. **Functional types:** If $\\alpha $ and $\\beta $ are types, then so is $\\langle \\alpha, \\beta \\rangle $.\n", " 3. **Closure:** Nothing else is a type.\n", " \n", "Rule 2 is recursive. So, the type $\\langle e, t \\rangle$ characterizes functions whose domain is the set of entities, and whose range is the set of truth-values. $\\langle \\langle e, t \\rangle, t \\rangle$ is the type of a function whose input is a (higher order) function of type $\\langle e, t \\rangle$, and whose output is type $t$ (this is of course the type of a generalized quantifier). In the Lambda Notebook, types are written in a similar way, and $e$ and $t$ are built in. The following shows how to construct these three types using the built-in `tp` (for type parser) function, which parses strings into Type objects." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "from IPython.display import display\n", "display(tp(\"e\"),\n", " tp(\"\"),\n", " tp(\"<,t>\"))" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "tp(\"<,t>\").left" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "All expressions in the Lambda Notebook metalanguage are typed, including variables and constants, and this is written using a \"`_`\" followed by the type. The following simply defines a variable over functions $f$ that has the type of a generalized quantifier." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "%%lamb\n", "f = f_<,t>" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "f.type" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "See the [neo-Davidsonian fragment](/notebooks/fragments/Neo-davidsonian%20event%20semantics.ipynb) and the [intensional semantics](/notebooks/fragments/von%20Fintel%20and%20Heim%20beginning.ipynb) fragments for examples of adding further types." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Typed lambda expressions\n", "\n", "There are various notational systems/conventions for a typed lambda calculus, but one common notation (or notational shortcut) often seen in formal semantics is to write expressions such as:\n", " * $\\lambda x_e . Cat(x)$\n", " \n", "In Heim and Kratzer, for example, this is really an abbreviation for something like the following, which is basically a two-place $\\lambda$ expression allowing for rich constraints on $x$:\n", " * $\\lambda x : x \\in D_e . Cat(x)$\n", " \n", "Currently the lambda notebook uses _only_ the abbreviated form, i.e. allows only type-based constraints, not the two-place $\\lambda$ expression. Therefore, a lambda expression in the notebook consists of a variable, a type constraint, and a body. These expressions both describe a function that, given some $x$ of type $e$, returns true just in case $x$ is a cat. Notice that, implicitly, the thing to the right of the period is a truth-value, and the predicate $Cat$ can be thought of as having a type as well (though this last part isn't typical; it is often thought of as being a first-order predicate logic constant).\n", "\n", "In the lambda notebook, this function can be described in the meta-language using the form \"`lambda var_type : body`\", where the variable name (lowercase) is separated from the type by an underscore. Here's an example:\n", " * `lambda x_e : Cat(x)`\n", " \n", "This example is illustrated below in practice. The second line of the next cell defines a variable `cat` that is a function of type $\\langle e, t \\rangle $. This variable is exported into the python environment, and is a subclass of `lamb.meta.TypedExpression` (In this case, `lamb.meta.LFun`, the class for lambda expressions.)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "%%lamb\n", "cat = lambda x_e : Cat(x)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "ltx_print(cat, cat.type, \"This object's class is: \" + str(cat.__class__))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Notice the info message warning us effectively that we didn't specify a type for the constant `Cat`. There are some very simple built-in heuristics for what type you might mean, and it first guesses $t$ for a constant (and $e$ for a variable); it realizes this is wrong and upgrades the type for the constant to be a property type. We could also explicitly specify all the types for all terms:" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "%%lamb\n", "cat = lambda x_e : Cat_(x_e)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Type mismatches\n", "\n", "If you do something wrong, a `TypeMismatch` (module: `types`) exception will be raised. Note that type checking happens on construction of any `TypedExpression`, and is not deferred until application." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "%lamb p_t = p_t\n", "%lamb y_e = y_e\n", "cat(y) # this one works, because the types match" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "cat(y).reduce_all() # a handy function" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Here's an example of a type mismatch that you can uncomment if you want; a preformatted example of what happens when this sort of exception is thrown in python is shown below the cell. An exception produces a 'stack trace' showing exactly where execution was when the exception happened, which is often more verbose than you need: for `TypeMismatch` the crucial problem is usable visible from the end of the stack trace. " ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "# cat(p)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ " ---------------------------------------------------------------------------\n", " TypeMismatch Traceback (most recent call last)\n", " in ()\n", " ----> 1 cat(p)\n", "\n", " /Users/advil/repos/lambda-notebook/lamb/meta.py in __call__(self, *args)\n", " 1160 \n", " 1161 #print(\"globals: \", globals())\n", " -> 1162 return TypedExpr.factory(self, *args)\n", " 1163 \n", " 1164 \n", "\n", " /Users/advil/repos/lambda-notebook/lamb/meta.py in factory(cls, assignment, *args)\n", " 821 else:\n", " 822 logger.warning(\"Unable to coerce guessed type %s for '%s' to match argument '%s' (type %s)\" % (operator.type, repr(operator), repr(arg), arg.type))\n", " --> 823 result = ApplicationExpr(operator, arg, assignment=assignment)\n", " 824 if result.let:\n", " 825 result = derived(result.compact_type_vars(), result, \"Let substitution\")\n", "\n", " /Users/advil/repos/lambda-notebook/lamb/meta.py in __init__(self, fun, arg, defer, assignment, type_check)\n", " 1271 tc_result = self.fa_type_inference(fun, arg, assignment)\n", " 1272 if tc_result is None:\n", " -> 1273 raise TypeMismatch(fun, arg, \"Function argument combination (unification failed)\")\n", " 1274 fun, arg, out_type, history = tc_result\n", " 1275 op = \"Apply\"\n", "\n", " TypeMismatch: Type mismatch: '(λ x_e: Cat_(x_e))'/ and 'p_t'/t conflict (mode: Function argument combination (unification failed))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "It is often convenient to wrap something that might produce a TypeMismatch directly in a `try: ... except: ...` block. Here is one way of doing this:" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "result = None\n", "try:\n", " result = cat(p)\n", "except types.TypeMismatch as e:\n", " result = e\n", "result" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Complex function expressions\n", "\n", "Lambda expressions can be treated just as any expression in the lambda notebook metalanguage, with parenthesis used for grouping (see other documentation for details). For example, we can write very complicated expressions made up of functions:" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "reload_lamb()" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "%%lamb\n", "id = ((lambda f_<,> : lambda g_ : lambda x_e : (f(g))(x))(lambda h_ : h))(lambda i_e : i)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "The full semantics of lambda expressions (i.e. function argument combination and type checking) are supported. In some cases (mainly semantic composition) reduction is done automatically but for variable definitions like this you have control. The easiest way to do the reduction is typically the `reduce_all` function:" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "id.reduce_all()" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "If you want to see how this happened, you can peek at the derivation with varying levels of detail:" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "id.reduce_all().derivation" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "id.reduce_all().derivation.trace()" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Variable collisions and alpha conversion\n", "\n", "Variable renaming of bound variables (alpha conversion) will occur as needed." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "%%lamb\n", "collision = lambda x_e : (lambda f_ : lambda x_e : f(x))(lambda y_e : y <=> x) # use '<=>' for equality" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "$x$ is of course bound to the higher lambda term in the argument, and we wouldn't want it to become bound to the lower variable on function application (substitution for $f$ in the scope of the lwoer binder), so one of them has to be renamed:" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "collision.reduce_all()" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "That's pretty much what there is to the lambda calculus in this context. To summarize:\n", "\n", " * Notation for types, using angle brackets and commas. (Several other types are available by default, including tuples and sets, so the full type grammar is a bit more complicated.)\n", " * Notation for lambda expressions, of the form \"`lambda var_type : body`\". \n", " * `%%lamb` environments for defining functions in the metalanguage." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Inspecting meta-language objects\n", "\n", "Finally, if you want to inspect an existing object to see how you would write it in the meta-language, `repr` is guaranteed to produce parsable output with the same result. (If it doesn't, this is a bug, please report it!) The form may be slightly normalized relative to how it was constructed." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "repr(collision)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "te(repr(collision))" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "repr(te(repr(collision))) == repr(collision) # normalization should be idempotent, too" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [] } ], "metadata": { "kernelspec": { "display_name": "Lambda Notebook (Python 3)", "language": "python", "name": "lambda-notebook" }, "language_info": { "codemirror_mode": { "name": "ipython", "version": 3 }, "file_extension": ".py", "mimetype": "text/x-python", "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", "version": "3.6.6" } }, "nbformat": 4, "nbformat_minor": 2 }