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
|
$\beta$ laws:
\vspace{-1cm}
\begin{gather*}
\prodmatch{\vpair{\mV}{\mV'}}{\mx}{\mA}{\my}{\mA'}\mM
=
\substituteDouble\mM{\mV}{\mx}{\mV'}{\my}
\\
\plusmatch{\inject{\indx
i}\mV\!}{\mx_1\!}{\!\mA_1}{\mM_1}{\mx_2\!}{\!\mA_2}{\mM_2}
\!=
\substitute{\mM_i}{\mV\!}{\mx_i}
\\
\force{\parent{\thunk\mM}}
=
\mM
\qquad
\sbind{\parent{\return\mV}}\mx\mA\mM
=
\substitute\mM\mV\mx
\\
\apply{\indx i}{\cpair{\mM_1}{\mM_2}} = \mM_i
\qquad
\apply{\mV}{\abst\mx\mA\mM} = \substitute\mM\mV\mx
\end{gather*}
$\eta$ laws:
\vspace{-1cm}
\begin{gather*}
\mV = \unitval
\\
\substitute\mM\mV\mz
=
\prodmatch\mV{\mx}{\mA}{\my}{\mA'}{\substitute\mM{\vpair\mx\my}{\mz}}
\quad
\fresh{\mx$, $\my}\mM
\\
\mM
=
\zeromatch\mV\mB
\\
\substitute\mM\mV\mz
=
\plusmatch*\mV{\mx}{\mA\hphantom{'}}{\substitute\mM{\inject[]1\mx}\mz}{\my}{\mA'}{\substitute\mM{\inject[]2\my}\mz}
\quad
\fresh{\mx$, $\my}\mM
\\
\mV = \thunk{\parent{\force \mV}}
\qquad
\mM = \sbind\mM\mx\mA{\return\mx}
\\
\mM
=
\cpair{\apply{\indx 1}\mM}{\apply{\indx 2}\mM}
\qquad
\mN = \abst\mx\mA{\apply \mx\mN} \qquad \fresh\mx\mN
\end{gather*}
Sequencing:
\begin{gather*}
\sbind\mM{\mx\!}{\!\mA}{\parent{\sbind\mN{\my\!}{\!\mA'\!}{\mN'}}}
\!=\!
\sbind{\parent{\sbind\mM{\mx\!}{\!\mA}\mN}\!}{\my\!}{\!\mA'\!}{\mN'}
\quad\!\!\!
\fresh\mx{\mN'}
\\
\sbind\mM\mx\mA{\cpair{\mN_1}{\mN_2}}
=
\cpair*{\sbind\mM\mx\mA{\mN_1}}
{\sbind\mM\mx\mA{\mN_2}}
\\
\sbind\mM\mx\mA{\abst\my{\mA'}\mN}
=
\abst\my{\mA'}{\parent{\sbind\mM\mx\mA\mN}}
\quad\fresh\my\mM
\end{gather*}
Effects:
\vspace{-1.1cm}
\begin{gather*}
\mop_{\mV}^{\mB}{\abst{\mx\!}{\!\sArity}{\parent{\sbind\mM{\my\!}{\!\mA'}\mN}}}
=
\sbind{\parent{\!\mop_{\mV}^{\sF{\mA'}}\!{\abst{\mx\!}{\!\sArity}\mM}\!}\!\!}{\my\!}{\!\mA'\!\!}\mN
\ \,
\fresh\mx\mN
\\
\mop_{\mV}^{\mB_1\cprod\mB_2}{\abst\mx\sArity{\cpair*{\mM_1}{\mM_2}}}
=
\cpair*{\mop_{\mV}^{\mB_1}\abst\mx\sArity{\mM_1}}
{\mop_{\mV}^{\mB_2}\abst\mx\sArity{\mM_2}}
\\
\mop_{\mV}^{\funtype{\mA'}{\mB}}\abst\mx\sArity{\abst\my{\mA'}\mM }
=
\abst\my{\mA'}{\mop_{\mV}^{\mB}\abst\mx\sArity\mM}
\quad \mx\neq\my
\end{gather*}
% Recursion: $\quad \sfix\mx\mB\mM = \substitute\mM{\thunk{\sfix\mx\mB\mM}}\mx$
Coercion:
\vspace{-1.05cm}
\begin{gather*}
\coerce[\e_2\subset\e_3]{\parent{\coerce\mM}}
=
\coerce[\e_1\subset\e_3]\mM
\\
\coerce{\parent{\return[\e_1]\mM}} = \return[\e_2]\mM
\\
\coerce[\e\subset\e']{\parent{\sbind{\mM\!}{\mx\!}{\!\mA}\mN}}
=
\sbind{\parent{\coerce[\e\subset\e']\mM}\!}{\mx\!}{\!\mA}{\coerce[\e\subset\e']\mN}
\\
\coerce {\parent{{\mop_{\mV}^{\sF[\e_1]{\mA'}}\abst\mx\sArity\mM}}}
=
\mop_{\mV}^{\sF[\e_2]{\mA'}}\abst\mx\sArity{\coerce\mM}
\end{gather*}
|