Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
\documentclass{article}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{tikz-cd}
\usepackage{mathpartir}
\usepackage{stmaryrd}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{nonnum-theorem}{Theorem}[section]
\newtheorem{corollary}{Corollary}[section]
\newtheorem{definition}{Definition}[section]
\newtheorem{lemma}{Lemma}[section]
\newcommand{\dynv}{\text{Dyn}^+}
\newcommand{\dync}{\text{Dyn}^-}
\newcommand{\good}[1]{\text{good}_{#1}}
\newcommand{\prop}{\mathbb P}
\newcommand{\with}{\mathrel{\&}}
\newcommand{\eqv}{\simeq}
\newcommand{\soln}{\text{Sol}}
\newcommand{\police}[1]{\text{police}_{#1}}
\newcommand{\later}{{\blacktriangleright}}
\begin{document}
\title{Gradual Types as Subsets}
\author{Max S. New}
\maketitle
We fix a predomain $\dynv$ with poset structure and a domain $\dync$
with bounded below poset structure as solutions to the domain
equations:
\[ \dynv = 2 + \dync \]
\[ \dync = (\dynv \to \dync) \with L (\dynv_{\mho}) \]
Q: does this actually get us the right order?
Q: what domain-theoretic properties does the order have that matter?
There are several ways to define essentially the same interpretation
of CBV gradually typed lambda calculus with booleans into this
semantics:
\begin{enumerate}
\item Types as ((Co-)Kleisli) co-reflections
\item Types as interior operators
\end{enumerate}
I want to explore one that I previously dismissed as somewhat na\"ive:
value types are (well-behaved) subsets of the universal predomain and
computation types are (well-behaved) quotients of the universal
domain.
\begin{enumerate}
\item A value type $A$ is a \emph{policeable} predicate $\good A :
\dynv \to \prop$
\item A computation type $B$ is a \emph{envelopable} equivalence
relation $\eqv B : \text{Equivalence}(\dynv)$
\end{enumerate}
Let's explain what these mean.
%
First, define $\soln A$ to be the set of ``good'' elements of $\dynv$
according to $A$, i.e., $\{ d : \dynv \,|\, \good A d \}$.
%
$\good A$ is \emph{policeable} when there exists a function $\police A
: \dynv \to (\soln A)_\mho$ satisfying two properties:
\begin{enumerate}
\item (monotonicity) $\forall d \sqsubseteq d'. \police A d \sqsubseteq \police A d'$
\item (retraction) $\forall x \in \soln A. \police A x = \eta x$
\item (projection) $\forall d \in \dynv. \police d \sqsubseteq \eta d$
\end{enumerate}
If $\sqsubseteq$ is a poset and $\eta : A \to A_\mho$ is order-reflecting,
then $\police A$ is uniquely determined by these two properties, for
if there were another such function $(\police A)'$ we would have
\[ \]
\subsection{Synthetic Guarded Domain Theory}
We can solve the domain equation using synthetic guarded domain
theory.
\begin{align*}
\dynv &= \mu (\lambda D^+. 2 + \mu (\lambda D^-. L (1 + D^+) \times (D^+ \to D^-) ))\\
\dync &= \mu (\lambda D^-. L (1 + \later \dynv) \times (\later \dynv \to D^-) )
\end{align*}
unfolding this gives us
\begin{align*}
\dynv &\cong 2 + \dync \\
\dync &= L (1 + \later \dynv) \times (\later \dynv \to \later \dync)\\
&\cong L (1 + \later \dynv) \times \later (\dynv \to \dync)
\end{align*}
\begin{lemma}{Universal Domain}
$\dync$ is a domain with algebra
\[ \theta_\dync = \lambda p: \later \dync. (\pi_1p, ) \]
\end{lemma}
Let's define orderings.
\begin{verbatim}
data _<=_ : Dyn+ -> Dyn+ -> Prop where
bool : forall b : 2. inl b <= inl b
data _<=_ : Dyn- -> Dyn- -> Prop where
err-ord : BinRel a -> BinRel (a + 1)
err-ord _<=_ (inr *) y = T
err-ord _<=_ (inl x) (inl y) = x <= y
err-ord _<=_ _ _ = _|_
laterr-ord< BinRel a -> BinRel (L (a + 1))
laterr-ord< _<=_ (done (inr *)) _ = T
laterr-ord< _<=_ (done (inl *)) _ = T
laterr-ord> BinRel a -> BinRel (L (a + 1))
err : Dyn-
err = mu (\e. ((inl (inl *)), \x. e))
\end{verbatim}
Let's define
\end{document}