lection08.tex

\section{Лекция 8}

\subsection{Экзистенциальные типы}
	 1) $\dfrac{\Gamma\vdash\phi[\alpha:=\theta]}{\Gamma\vdash\exists\alpha.\phi}$\\ \\
	 2) $\dfrac{\Gamma\vdash\exists\alpha.\phi\qquad\Gamma,\phi\vdash\psi}{\Gamma\vdash\psi}$
	 
	  Экзистенциальные типы это способ инкапсуляции данных. Предположим, что у нас есть стек с хранилищем типа $\alpha$, у которого определены следующие операции:\\\\
	 \textbf{empty}: $\alpha$\\
	 \textbf{push}: $\alpha\&\nu\rightarrow\alpha$\\
	 \textbf{pop}: $\alpha\rightarrow\alpha\&\nu$\\
	 
	 Тогда очевидно, что тип stack$\equiv\alpha\&(\alpha\&\nu\rightarrow\alpha)\&(\alpha\rightarrow\alpha\&\nu)$.
	 Но что если мы реализовали хранилище как-то по-особенному, не меняя типов операций. Мы хотим скрыть данные о реализации, в частности о типе $\alpha$. Вместо деталей просто скажем, что существует интерфейс, удовлетворяющий такому типу:\\$\exists\alpha.\alpha\&(\alpha\&\nu\rightarrow\alpha)\&(\alpha\rightarrow\alpha\&\nu)$
	 
\subsection{Абстрактные типы}	 
	 Предположим, что мы захотим создать стек, в котором лежат целые числа. Рассмотрим, как тогда будет выглядеть тип созданного стека: \\
	 \textbf{stack}$\equiv\forall\nu.\exists\alpha.\alpha\&(\alpha\&\nu\rightarrow\alpha)\&(\alpha\rightarrow\alpha\&\nu)$\\
 	По аналогии с правилом удаления квантора существования, можно определить правила вывода для выражений абстрактных типов: \\

	
 	$\dfrac{\Gamma \vdash M : \varphi[\alpha := \theta]}{\Gamma\vdash (\text{pack } M, \theta \text{ to } \exists \alpha . \varphi) : \exists \alpha.\varphi}\\ \\ \\
	$ Это правило вывода позволяет скрыть реализацию стека, так как если $\alpha$ --- это тип стека, то $\alpha[\nu := \theta]$ --- его конкретная реализация, например ArrayStack, LinkedListStack и подобные \\ \\
 	 $
 	\dfrac{\Gamma \vdash M : \exists \alpha . \varphi\qquad\Gamma, x : \varphi \vdash N : \psi}{\Gamma \vdash \text{abstype } \alpha \text{ with } x:\varphi \text{ in } M \text{ is } N:\psi}
	(\alpha \notin FV(\Gamma, \psi))$
	\\ \\
	Это правило вывода соответствует виртуальному вызову стека какой-то реализации, например: 
	\begin{verbatim}
		foo(Stack s) {
			...
		}
	\end{verbatim}
	Поскольку выводимые формулы выглядят слишком громоздко, перепишем их, вспомнив, что: \\
	$\exists\alpha.\sigma\equiv\forall\beta.(\forall\alpha.\sigma\rightarrow\beta)\rightarrow\beta$\\\\
	Тогда: \\
	$	\text{\textbf{pack} } M, \theta \text{ \textbf{to} } \exists \alpha . \varphi =
		\Lambda \beta . \lambda x^{\forall \alpha . \varphi \to \beta} . x \theta M \\
		\text{\textbf{abstype} } \alpha \text{ \textbf{with} } x:\varphi \text{ \textbf{in} } M \text{ \textbf{is} } N:\psi =
		M \psi (\Lambda \alpha . \lambda x ^ \varphi . N)
	$