lambda

Let Polymorphism in Mini ML

Topic
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

Simply Typed Lambda Calculus

Topic
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

Lambda Applet

Topic

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.