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.