Existential types
-- hiding
F_{ \E }
%t ::= ... | \E %a <= %t_1. %t_2
e ::= ... | pack[ %a = %s in %t ]. e
Type assignment
\ffrac{
%G |- %s' <= %s
\hspace{1cm}
%G |- e : %t
}{
pack[ %a = %s' in %t ].e \e \E %a <= %s. %t
}
Refinement
\ffrac{
%G |- %s <= %s'
\hspace{1cm}
%G |- %t' <= %t
}{
%G |- \E %a <= %s' . %t' <= \E %a <= %s. %t
}
slide
:
The existential type calculus
