Term#

class Term(*args, **kwargs)[source]#

Abstract base class for terms.

A term is an expression representing a value of a type.

It can be either a Variable, Constant, Application, or Abstraction.

Variable#

class Variable(arg1, type=None, **kwargs)[source]#

Variable.

A variable is an atomic expression representing an arbitrary value of a type.

Parameters:

  • arg1 – Id.

  • type – Type.

  • kwargs – Annotations.

Returns:

A new Variable.

See also

Variables().

Bound variable#

class BoundVariable(arg1, type=None, **kwargs)[source]#

Bound variable.

(Internal: Not intended for direct use.)

Internally, terms use what is called a locally nameless representation. This is a combination of using De Bruijn indices for variables local to the current term (BoundVariable) and names for variables global to the current term (Variable). See C. McBride and J. McKinna, “Functional Pearl: I am not a number–I am a free variable”, Haskell’04, 2004. ACM.

See also

Term.open(), Term.close().

Constant#

class Constant(arg1, type=None, **kwargs)[source]#

Constant.

A constant is an atomic expression representing a particular value of a type.

Parameters:

  • arg1 – Id.

  • type – Type.

  • kwargs – Annotations.

Returns:

A new Constant.

See also

Constants().

Application#

class Application(arg1, arg2, *args, **kwargs)[source]#

Application.

An application is a compound expression representing the application of arg1 to arg2.

Application is left-associative: If more than two arguments are given, the result is left-folded.

Parameters:

  • arg1 – Term.

  • arg2 – Term.

  • args – Remaining Term’s.

  • kwargs – Annotations.

Returns:

A new Application.

Raises:

ValueError – arg1 cannot be applied to arg2.

Abstraction#

class Abstraction(arg1, arg2, *args, _open=True, **kwargs)[source]#

Abstraction.

An abstraction is a compound expression representing the function obtained by abstracting variable arg1 over arg2.

Abstraction is right-associative: If more than two arguments are given, the result is right-folded.

Parameters:

  • arg1 – Variable.

  • arg2 – Variable or Term.

  • args – Remaining Variable’s followed by a Term.

  • _open – Whether to open arg1 in arg2. (Internal: Not intended for direct use.)

  • kwargs – Annotations.

Returns:

A new Abstraction.