# lambda

## Let Polymorphism in Mini ML

###### 9/2/21

## Let polymorphism

We would like to have polymorphism in certain circumstances. For example, we would like to have the same identity function λx:x that could be used on Booleans and Integers, without having to have two separate identity functions, one of type B->B and the other of type I->I .

The usual way to do this, in this setting, is via a 'let' construction. Most functional programming languages have an expression form similar to

## Polymorphism, Annotation, and Decidable Type Inference

###### 7/8/21

[In this section, we will sometimes use annotated abstractions, and sometimes use unannotated abstractions. This is just to be flexible in discussing their respective merits.]

There certainly is an unusual feature possessed by the annotated STLC that we have thus far. Consider two abstractions with annotations

λx:I.x

and

λx:B.x

## Simply Typed Lambda Calculus

###### 8/23/21

## Types and Values

Types are collections or sets of values. For our purposes, to produce an illustrative example, we can get by with just two *basic* Types, one with a finite number of values, and the other with an infinite number of values.

The Type Boolean, or Bool, or just 'B' is a type with the two values: True, and False.

The Type Integer, or Int, or just 'I', is a type with the values 0,1,2,3... etc

## The Lambda Reduction Widget

###### 1/25/2020

Example

#### Alpha conversion (Rewrite of bound variables):-

Any abstraction λ<variable1>.<expr> can be converted to λ<variable2>.<expr>/.<variable1> -><variable2> provided the substitution <expr> /. <variable1> -> <variable2> is sound.

## Lambda Applet

Example

2013

#### Alpha conversion (Rewrite of bound variables):-

Any abstraction λ<variable1>.<expr> can be converted to λ<variable2>.<expr>/.<variable1> -><variable2> provided the substitution <expr> /. <variable1> -> <variable2> is sound.