Bounded polymorphism
-- abstraction
F_{ <= }
%t ::= Top | %a | %r | %t_1 -> %t_2 | \A %a <= %t_1. %t_2
e ::= x | %l x:%t.e | e_1 e_2 | %L %a <= %t.e | e [ %t ]
Type assignment
\ffrac{
%G, %a <= %s |- e : %t
}{
%G |- %L %a <= %s. e \e \A %a <= %s . %t
}
\ffrac{
%G, e : \A %a <= %s . %t
\hspace{1cm}
%G |- %s' <= %s
}{
%G |- e [ %s' ] \e %t [ %a := %s' ]
}
Refinement
\ffrac{
%G |- %s <= %s'
\hspace{1cm}
%G |- %t' <= %t
}{
%G |- \A %a <= %s'.%t' <= \A %a <= %s.%t
}
slide
:
The bounded type calculus
