Polymorphism - Programming Languages, Computer Science & Engineering Video Lecture - Computer Science Engineering (CSE)

welcome to lecture 33 so I'll just
briefly recapitulate what we did about
Mon Amour phys 'm and then go on to
polymorphism today all right so we
defined the language of this simply
typed lambda calculus where there was a
where there is a there is a notion of
some base types and the construction of
the construction of higher types from
the base types and these base types
which for simplicity I took to be
integer and boolean are really what
might be called type constants this they
are really even if and you say something
when you give something the name integer
it's in the in the domain of types it's
a constant now the significance of that
will become evident slightly later but
it's important to remember that they are
type constants okay so you can construct
complex types using the simple language
that we gave for constructing higher
types from these type constants so
essentially what it means is that all
your types will be of the form let's say
if in ten Bullard your base types then
you will have types of this form int
arrow int int arrow bool maybe you could
have you could have for example higher
types like int arrow int arrow bool
arrow
bully and so on I mean what I mean is
all your type expressions are going to
be of this form all your type
expressions will have the names of the
base types always occurring in it I mean
this there's nothing else is nothing
else to it okay so and then we give type
inferencing system for for this which
from which you can prove that you can
prove that every Combinator therefore
that every or every lambda expression in
this simply typed lambda calculus
actually has a unique type based on the
type expression based on these inference
rules yeah so given that a variable has
a certain type which a variable could
have a higher type also remember that we
are treating functions and variable
functions and values all as equal
objects so for example this X could be
of type int arrow int which denotes that
it is a function from integers to
integers and you could infer therefore
the types of all the lambda abstractions
all the lambda expressions in the
language which are typable and if they
are not typable then of course it
doesn't belong to the simply typed
lambda calculus and the beta reduction
is of course modified to take typing
into account so that only if you have a
lambda abstraction which is title which
is typable as something arrows something
and as let's say sigma arrow tau and you
have an operand which is of type Sigma
assuming that these types can be
inferred and therefore they have well
type terms then you can perform a beta
reduction and get a value of type talk
right so one of the things was that so
we looked at some examples dealing with
the identity functions and so what what
we notice that at this point is that
every every Combinator
are useful function because of because
of the type inferencing system because
every Combinator has a unique type which
is built up from the base types
therefore for what used to be type list
Combinator's which could be applied
anywhere in the in the untyped lambda
calculus for each one of them you have
several copies depending on the type of
application right so even a simple
integer as a simple identity function
then therefore has an incarnation for
integers has an incarnation for billions
has an incarnation for all functions
from integers to boolean's so for every
tau that you can think about there is a
separate identity function I tau okay
and they all and this is because of the
unique typing feature of this in simply
typed lambda calculus right so for each
type tau the combinators see any the the
the analog of the Combinator see in the
untyped lambda calculus when you move it
into the simply typed lambda calculus
for each type tau you will get a
Combinator C tau which respects that
typing okay so and of course we asked
this question whether we were actually
being too harsh by using a simple typing
scheme and one thing of course is that
these simple typing schemes were what
were used in some of the older
programming languages like Pascal and
modular and so on and so forth and of
course there are some questions I mean
we we actually went through the
computations of twice applied to itself
and so on and we found that some of them
could actually be given a meaning so not
all self application really is
meaningless and secondly the the point
is that these if you take any Combinator
C is really too tedious to have so many
different copies of it for each you have
accommodator C tau
for each possible trial the combinator
could be some complex program right so
it's really too tedious to have
something like this what we would like
when we think of an identity function
what we actually are implying really is
that it's a higher-order function which
given a function of any type tau returns
you the same function actually but
returns you a result of the type tau so
the other the identity function
regardless of their type for which it is
meant actually is is one really higher
order function which could be
parametrized on the time so we can talk
about I the identity Combinator I being
parametrized on a type tau and I tau
would therefore and the result should be
I tau which is appropriate Combinator
for values of type tau by values I also
include functions right so so and in
fact such such a generalized what I
might call a parameterised typing so
what we should be able to do is we
should be able to take this identity
call a general identity function i and
parameterize it on the substant right
and that is that is what follow morphism
is about then we have an identity
function which actually takes a type
itself as a parameter and then
specializes to that time right so we and
as we saw there are lots of lots of
functions which are which we use in all
our ML programming and so on which
really are of there the head and tail
function is the constant the map
function they are all in that sense
polymorphic I mean in the sense that
they the actual function is not very
crucially dependent
the underlying base type from which your
data type is constructed I mean this the
function remains more or less unchanged
except for the type for all possible
kinds of arguments that you might get or
at least for a class of possible
arguments for example I mean you can't
apply cons on an integer cons for
between two integers but there is a
class of arguments namely integers and
into integer lists billions and boolean
lists may be integer integer to integer
functions and lists of integer to
integer functions and so on for there is
a class of objects for which cons is
going to have essentially the same
representation and our intuitive meaning
of cons is just that given some given
some argument of type tau and given
another argument of a type list of
elements of type tau you should be able
to perform a cons and the implementation
or the meaning should not significantly
vary with it with variations in the
underlying type tau right so so so the
mono morphism actually has this real
problem that you cannot adequately
parameters so we generalize monomorphic
types so that they give us this general
flexibility and that means that in
addition to these type constants which
are the base types we also allow for
type variables okay so and that's that's
intuitively when how we look at the
let's say even a simple function like
the identity function right so what what
we are saying by a general identity
function is that for any type T and for
any value or function X which is of type
T the identity combinated I T when
applied to X
is summer beta equivalent actually it
should be the reduce in many steps may
be 2x itself okay now what we can do is
if you look at the lambda abstraction as
we have looked at it I told you the
analog of the lambda abstraction with
sex the lambda abstraction also has its
analog with universally quantified
objects okay so and this is essentially
a universal quantification so if you
look at the lambda if you look at a
lambda term of the let's let's look at
the identity Combinator what we are
essentially saying by this bound
variable X is that we are saying that
for any X they return back the value of
x in the case of sex what we were saying
is if you had a predicate here let's say
P dependent on X we're saying for any X
such that the predicate P of X is true
so the set notation the lambda
abstraction and universal quantification
are all very very similar and we will
use this fact so if you were to actually
read whatever we have been saying now a
good way to read it is as if it is a
universally quantified object for each
type T and for any value or function X
of type T I T of X should be beta equal
to X so what we did is that we stopped
here in our lambda calculus you know
simply typed lambda calculus we stopped
with this abstraction we just translated
this abstraction into the Combinator I T
right but if we go beyond this
abstraction also into this abstraction
okay then what you get is a general
Combinator I
okay so four you can read this is for
any P and for any X of type T return X
okay and I'm just and since the I mean
the universal quantification in
predicate logic is really like lambda
abstraction I'm just using the universal
quantifier here so this identity of the
generalized identity Combinator that we
are really looking for is really has a
type which is given by a universally
quantified type variable the moment
you've got so now they here here you've
got a case where there is a variable
which is bound by this universal
quantifier right so this is like a again
I mean this is like a local declaration
this this this is this is like a
predicate if you like so but this local
declaration clearly specifies that for
any type so the identity Combinator is
has a type such that for any type T it
has the functionality functionality T
arrow T where I don't really care what
value you give this T okay if you're
generalizing from monomorphic types then
what you can say is that this variable T
maybe may take any value from the
monomorphic types defined by this by the
language of types right so for example
so this T could be a value like int it
could be bull
it could be int arrow bool it could be
int arrow int arrow bool and and so on
and so forth any of the types that we
have so far defined in our simple type
structure could be a value for T and the
identity approximately and that and that
identity Combinator
will will
appropriately take this velocity okay so
now what we are looking at is I mean we
we started out with variables and
constants way back in the in the in the
Paleolithic period where constants and
variables really took values from an
underlying domain of values we took then
we got functions unnamed functions which
are also variables we generalized func
we generalize the notion of variables to
functions on type functions where the
functions could take values from well
function spaces an underlying domain
which was function spaces now we are
going further and we are taking their
domains themselves types are really
those domains and those domains are
fixed so far and now we are generalizing
them we are saying you take a variable
over which takes values which are the
naming of particular domains right so
the domain int arrow int could be a
particular value of this variable T okay
and this universal this is like a
universal quantification okay so if this
lambda abstraction is like a universal
quantification then lambda then lambda
application or a beta redex
is like Universal instantiation so I
mean you studied this quantifier
elimination and introduction rules so
lambda abstraction
the quantifier introduction and beta
reduction is quantifier elimination or
Universal instantiation so you can
instantiate the T here by any particular
type constant that you like or any type
expression which is built up only from
type constants so T could so you can
talk of type variables which actually
take values and those values are type
expressions built up from type constants
and that is what polymorphism is about
right so this is what is known as a
parametric polymorphism and this is the
Perim this is the polymorphism that is
present in MA yeah so so let's let's
look at the function for example twice
so the reason twice is meaningful then
is really that it is a function of this
form if you look at the definition of
twice I can say that for any type T for
any function f of type T arrow T and for
any value or function X of type T twice
f twice applied to F applied to X should
be beta equal to F applied to F applied
to X right so this is this is this is
the basic fact we know about twice and
now go back upwards and do the
abstraction so what do you get you get F
applied to F applied to X you perform
the abstraction on
X to be of type T then you perform the
abstraction on F to be of type T arrow T
and so far it's really like the simply
typed lambda calculus and then actually
we haven't yet another abstraction a
universal quantification over the type T
and so this essentially says for every
type T and for every function f which
has a type TR of T and for any argument
X which has a type T return the result F
applied to F applied to X and so what is
the type of twice I will I mean the
problem the point now is that now we
have two kinds of beta reductions and if
you know if Universal instantiation if
lambda expressions are really like
universally quantified predicates then
beta reduction is like Universal
instantiation okay then
inst and Universal instantiation is like
beta reduction which means when you
universally quantify on types and
instantiate those types you get a form
of beta reduction also four types in
addition to the beta reduction that you
already have for the lambda expressions
so it's so as you can see things can get
a little hairy at this point I mean okay
so we have variables we have type
variables we have constants if you are
applying the lambda calculus on to some
domain and you will also have type type
constants and then you can have
instantiation of those variables
instantiation of those values
instantiation of value variables
instantiations of type variables by
typing spreche ins by expressions of the
application and you will be inferring
types you'll be inferring so types and
values also look essentially the same
you're going to have a beta reduction
for type expression
for quantified type expressions which
which is like another lambda expression
only this lambda is abstraction is on
types and it's not on values and of
course values are the same as functions
whatever may be the order right but
types are different but still types also
follow essentially the same discipline
of quantification beta of application
beta reduction Universal generalization
Universal instantiation quantifier
elimination quantifier introduction and
everything this is this is the and so ok
and so so what is the type of twice so I
just assume that you already know the
inference rules you can get the
inference rules by analogy so we can
actually by structural induction on the
inference rules which are predictable
now you can actually infer the type of
wire in this fashion so given that f is
of type T arrow T and X is of type T if
F applied to X will be of type T F
applied to F applied to X will be of
type t2 because of this F is of type T
arrow T and F X is of type T therefore F
applied to F X will be of type T then
when you perform the abstraction over X
I am doing this bottom-up of course but
but that's always easier to understand
for the human being that's not
necessarily how the machine will do it
how your compiler will do it note that
all this has to be done by the compiler
so it will do it by a structural
induction you can assume for practical
purposes it will be doing it by a
recursive descent parsing method as part
of the parsing process type
determination is part of the power
parsing before the code generation you
do the type determination in order to
decide whether code has to be generated
at all and so you'll do it in a
recursive descent parsing fashion and
come up so then this abstraction gives
you this type then the abstraction over
F gives you this type and the
abstraction over T
it gives you this time right so
essentially what we are saying is that
functions like twice which are actually
meaningful they are meaningful even
under self-application because when
twice is applied to twice the operator
twice has a type
since twice as polymorphic it's type is
universally quantified we can always
choose a type for the operand twice and
generalize it so that the operator twice
has a higher type than the operand twice
and that's in fact what normally happens
in mathematics when you apply one
function to another when you apply a
function to another
the OP the operator always has a higher
type than the operand
now since twice is polymorphic this
twice when you apply twice to itself
this is the operator twice and this is
the operand twice the operator twice is
of a much higher type than the operon
twice so you assign if you assign if you
assign to twice this the operand twice a
type tau and that type tau would be an
expression of this form universally
quantified a universally quantified type
expression of this form then so if this
has a type tau where tau is let's say
sum for all Sigma such that I have I
have missed out a T here this should be
T at T here T arrow T goes to T arrow T
right for all so for all Sigma if if
this twice has the type for all Sigma
Sigma R sigma arrow Sigma arrow Sigma
then this twice has a type
so the result of applying this twice to
this twice should give you an element of
type town right so then this twice has a
type which is really given by tau R tau
R of tau where tau on application
treated in general it has a type when
you look at this twice in I mean that
Tower or tau arrow tau or tau has to
come out as a particular case of this
Sigma biased by a suitable nope
substitution process I leave that as an
exercise to you but essentially
polymorphism means that an expression is
polymorphic if it can actually have
different types depending on the context
in which it is applied right so the
truth so the application of twice -
twice
is meaningful provided the operator
twice as a higher type which is
compatible with the author n twice which
is compatible with the twice of the
operand a particular case of this is
something that you can you can see in
any standard book on polymorphism or
programming languages ok so what we'll
do is let's formalize these notions so
we have the language of what I might
call poly types ok so now the language
of poly types as opposed to the language
of mono types which is what we did in
this simply typed lambda calculus is
firstly you assume an infinite
collection of type variables and a
collection of type constants and these
type constants are usually are the
usually consist of the base types which
you're going to start off with so let's
say integer and boolean and then firstly
you build we build up the mono types
in the same fashion that we did for the
simply typed lambda calculus so if B is
the base type then B is also a mono type
and if tau 1 and tau 2 are mono types
then tau 1 arrow tau 2 is a mono type in
addition you allow type variables also
to be regarded as one attacks so type
variables actually are going to denote
particular instances of monotypes
right then we build our poly types like
this anymore o type is also a poly type
and anymore any poly type quantified
over a free type variable the notion of
free and bound variables is as before
over type expressions if if pi is some
type then any variable that occurs in it
any type variable that occurs in pi is a
free type variable and you can quantify
overtype variables and then that
variable becomes bound ok so so this is
how we construct poly types you know so
this is the kind of when I mean there is
a mean if you just extend this argument
further we could also construct super
poly types by a similar grammar given
that pi is a poly type you could define
a collection of an infinite collection
of super type variables a collection of
poly types over poly types and then
super poly tile is being defined in a
similar fashion
yeah and so in this the pipe hierarchy
actually can go to ad infinitum upwards
the lowest part of the type hierarchy
are the mono types
yep
right and below the monotypes of course
our values and functions right so but
let's let's limit ourselves to just this
the type hierarchy at two levels so
there are just type variables and type
variables can vary can take values only
from mono types and mono types are
whatever was were defined in the simply
typed lambda calculus right so and then
you can construct a poly type by
quantifying over the monotypes
quantifying over the type variables
right so now so the polymorphic lambda
calculus is defined in this fashion so
we have the usual syntax of the simply
typed lambda calculus remember that this
is a mono type remember that the simply
typed lambda calculus was very nice in
the sense that it gave you everything
that was that could be statically typed
determinable it it could type check
statically but the only problem was that
the simply typed lambda calculus could
not account for generalized Combinator's
like i or twice which are polymorphic i
is of course very very general twice is
not so general i mean twice can will
type check only for certain classes of
arguments argument types i mean for
example you can't give twice a value
from the base type it won't type check
for example you can't apply twice on an
integer
twice can be applied only to another
function which means it should have a
type of the form some t1 arrow t2 i mean
it could only apply to another object
which has a type t1 arrow t2 it cannot
apply it to a to a base to adjust a base
type
has to apply to a function right so but
that is essentially like the way we
write sets right let's take this X such
that X is even and then it satisfies
some other property I mean you can you
can take subtypes of the nut I mean you
can take subsets of the natural scent
right generalized set definitions right
this is still quite general right so so
the so functions like twice are
polymorphic in the sense that they do
not range over the entire type hierarchy
where is the the the Combinator I
actually ranges over the entire type
hierarchy you can give it a value a
function a type variable anything and
the identity Combinator will work it
will just give you back whatever you
asked whatever you gave it but the twice
requires an argument which has a type of
a certain form that it should be
explicitly a function form it cannot be
a value form not only that it should
explicitly be a function form it should
it cannot be a function form of type t1
arrow t2 where t1 and t2 are completely
different it has to have a type t1 arrow
T 1 so all for all instantiation of t1
such that the types such that you have
functions from t1 arrow T 1 the twice
can be applied that is the type of twice
right so that that's that's what is
obvious from its from the definition of
the function abstraction in twice right
so so now what we have is in addition to
the mono types we have the type
abstraction
on lambda abstractions on on lambda
terms right so this is the standard is
the type of abstraction which I pointed
out and this is actually an application
of a mano type of a of a lambda P of
presumably a lambda term which takes a
type as a parameter so if this lambda
term were the Combinator I was a
polymorphic Combinator I you could give
it any monotype as an argument and it is
specialized to that particular I towel
okay in the case of I of course this now
could be anything anything in the
monotypes in the case of twice this now
would have to be of the form Sigma arrow
Sigma where Sigma arrow Sigma is
constructed constructible from the base
types through the monotype context-free
grammar right so so this is actually a
type applicant is actually an
application of a lambda term to a mono
type so as to specialize that Combinator
for that particular time yeah and then
well for completeness since this
was all this was there in Ravi Satie's
book I decided to add this construct
also so here is a let expression where
so but these are all mono wherever I
have written tau it's a mono type
wherever I that means it's it's a it's a
restricted part of the type grammar that
we have word I mean it's there also how
is the monotype means that it comes from
the language of simply typed of the
simply typed lambda calculus with of the
the language of type types in the simply
typed lambda calculus but with with the
added construction that you could have
variables instead of actual
expressions buildup of type constants
okay but now we can take a poly type
okay so you if X is a supposed to be a
poly type then this is this whole let
construct is a lambda application in
which all free occurrences of X in this
will be replaced by this and it should
type J okay so we look at it we look at
this construct a little more carefully
later but essentially the most important
additions are really that are really
this the new type application in the
type of structure this type application
means that there is a beta reduction for
types okay and this is the construction
of more complex functions which are
polymorphic from the poly types
themselves yeah so this is really this
is actually a form of lambda lambda
application as you can as you will be
able to see all right when we when I
give the rules it should become clear
but for the moment let go of this or
rather let's keep this because I'm going
to give an example which illustrates
this okay so it's a very nice example
again drawn from Ravi satus book so
let's take twice
so I have this expression which is
really let twice which is defined in
this fashion okay
choices of type this it's polymorphic as
you can see because it has a universal
quantifier over type variables so it's
not a mono type so consider the
polymorphic function twice whose
definition is given by this okay
in the expression twice int successor
the successor is the standard successor
function written in the lambda calculus
we are assuming applying it on integers
let's say so for any X the successor of
X is as defined by piano arithmetic
right so now what we are saying here is
apply first tries on two integers that
means particular as twice to integer
functions that means functions from
integers to integers so what you get
when you apply twice to integers is a
new function which is particularly to
all functions of the type of the
monotype integer to integer apply that
function onto successor okay the result
of which has to be applying successor
twice on to whatever is the argument and
if you applies and the result of so the
result of this application is to
particular as twice to the type int
arrow int and having particular eyes
twice to int arrow int you apply it now
to successor which is which is a
function from int arrow int so it's
perfectly understandable right so it's
type compatible
okay since successor is he's a function
is since successor is lambda X X prime
where X prime is going to be int and
therefore this lambda abstraction gives
successor the type int arrow int so this
twice applied to int gives you a
function twice subscript int arrow int
which applied to this function successor
which is of type int arrow int so
therefore it's applicable I'm sorry
twice applied to int gives me a function
int arrow int arrow int arrow int which
applied to a function successor which is
of type int arrow int gives me a result
which is a function of type int arrow
int which given the argument 0 gives me
a value in int so essentially we do the
value 2 which seems a hell of a big mess
to get into just in order to get the
value 2
but in principle it's it's a powerful
operation so I've just I just showed how
the beta reduction works for particular
izing so the beta reduction for types
for polymorphic types is to really
particular eyes that function for a
particular for a certain type right or
instantiate the universal quantifier in
their type to a particular so this twice
applied to int is actually what I have
written in if you if I follow the
notation that I used before it's
actually twice particular eyes to int so
it's really I would have given the
subscript int arrow int arrow
int arrogant right
so it this this twice works only for
works only on functions of the forum int
arrow int of course there is a
possibility that I could have applied
twice on a type variable too
and I could have put that variable may
have maybe quantified somewhere later
okay if I can have nested quantifiers
right for all s for all T and so on and
so forth then that variable might get
its value might get its type value
because of the instant she ation of a
quantifier they'll exists somewhere in
the outer scope right and then so then
for if so and if I look at this
restricted sub term then it would be
twice with the subscript T arrow T arrow
T arrow T where T should get its value
instantiated somehow later right so now
we can actually and since beta reduction
is so the so now you understand why beta
reduction is really important
checking whether membership in a set is
really a form of beta reduction applying
functions is really a form of beta
reduction Universal instantiation is
really a form of beta reduction and
constructing sets by abstraction is
really a form of lambda abstraction
constructing quantified predicates is
really a form of lambda abstraction
constructing types is really a form of
lambda abstraction so applying types and
instantiating them is also a form of
beta reduction so so beta reduction in
computation is really the most
fundamental concept which which is
probably evolved over the last 40 years
almost anything that is constructed by
constructive anything that is
computationally relevant has beta
reduction up
in some form or the other parameter
passing in procedures is a form of beta
reduction whether the parameters are
passed by value or by reference or by
name they are all forms of beta
reduction and now types are also forms
of beta reduction so there generates
that you have in C++ and ADA are really
some very restricted form of beta
reduction applied only to some base
types and AHA so far in in terms of
implemented programming languages the
highest form of the most sophisticated
type system that is so far come up is
the ML polymorphism which is completely
statically determinate where types are
completely polymorphic types are
statically determinate means they are
determinable at translation time without
going into executions yeah so that's one
of the reasons for studying ml because
it's it's a functional a it's not just
that it's a functional language but also
that it has a very sophisticated type
system the most sophisticated type
system in existence in an implemented
programming languages is an ml so the
type inferencing rules now actually by
now you want to you would have got a
flavor of the type inferencing rules
that you should have and these are
essentially it so given a variable so
again given a type context gamma or a
type environment gamma the type of a
variable X is whatever this X is free
right so if so whatever if the context
does not contain X then it does not type
check as simple as that and you throw
out that program but so whatever the
context in give for X is the type of X
and this is the usual application of
functions if L is of type Sigma arrow
tau which are by the way Sigma and tau
are monotypes
this is this is the monomorphic
application
M is of type Sigma which is again a
monotype then L applied to M is of type
tau if with the assumption that X is of
type Sigma add it to the context you can
infer that L is of type tau then the
lambda abstraction X Sigma L has the
type Sigma R or tau where again all
these Sigma's and Tau's are monotypes
right okay
so that is as so these the the type
inferencing rules here are really like
the time entrancing rules is the simply
typed lambda calculus there is no
difference but what we require now are
type inferencing for the polymorphic
lambda calculus right so here here goes
so if it is determinable that L has that
L has the polymorphic type for all T pi
where pi could itself be another
polymorphic type because you could have
quantifiers you could have a sequence of
quantifiers right in nested quantifiers
so pi could be a polymorphic type then
given tau a monotype you cannot apply L
to another polymorphic type but you can
apply it to a mono type that is applying
L to a mono type means particular izing
L to a certain type applying L to a
polymorphic type does not exist in our
language so far okay but I mean as I
said there's no reason to build up the
type hierarchy I mean you have
quantifiers over polymorphic type
variables to I mean then you would have
a particular reason there is actually a
reason for doing that but that's because
it's not many of those things are when
you go from two types higher than this
it
that lots of problems about of
undecidability cropper so this is about
the limit that we are currently we have
currently reached so given that Tao is a
mono type your particular izing the
polymorphic lambda expression L so that
an incarnation of it for the type tau is
created by this application and if an
Inc and so that means what this
universal quantifier for odd T has to be
instantiated has to be eliminated by
instantiating P with the value tau and
that's what this substitution does so it
takes PI and for all free occurrences of
T in pi it replaces those free
occurrences by the monotype tau okay so
this is the case this is clearly a case
of universal instantiation it's also a
form of beta reduction for the types
yeah so this is a type application or
instantiation where Phi is a poly type
and tau is the monitor right and then of
course and this so this is like
Universal instantiation so there should
be a corresponding universal
generalization or quantifier
introduction rule and that is what this
does given that in the context gamma you
can show that L is of type a poly type
PI then this abstraction over the types
over the free variables T over the free
type variables T in PI gives you a
polymorphic lambda expression which has
a type for all T PI this is type
abstraction where it is very similar to
the lambda abstraction
yeah the only thing of course is that
whenever we are talking about free
variables whether it's type variables or
value variables and I know whenever
whenever we are talking about binding
them we should ensure that there is no
capture of free variables because of
your because of the binding you're
creating because of the introduction of
this quantifier you are creating a you
you're binding this variable T and as a
result no T in pi which actually so they
should have there should not be any T in
the context gamma okay already defined
because that T if that T occurred in PI
then that he would get captured by this
quantifier okay so the usual confusion
of free variables bound variables alpha
conversion with quantifiers and so on I
mean I mean of course alpha conversion
also exists anywhere where there is
anywhere where there is binding or
declaration there is alpha conversion
right and so you have to do alpha
conversions over bound variables to
ensure that there are no free variable
captures right so T should not be free
in gamma that means T should not already
have been declared in gamma and then the
last rule is just really a form of typed
lambda application for the polymorphic
case if L is of type PI 1 which is a
polymorphic type and with the assumption
that X is of type PI 1 if you can infer
that M is of type PI 2 then this let
expression this whole let expression
really has the type of M because M is
really the expression and the meaning of
any let expression is the body of the
expression which is which in this case
is M right so it has a type right so let
expressions really are like applications
because what you can it's the semantics
of a let expression is equivalent to
substituting all free occurrences of X
in M by L yep
so it's really a form so now you can
look at you can go back and try to
determine what the type of this right
and by now I mean so you really reach
the highest levels that types can reach
in a decidable fashion