From b6325554a2df61de4b6312c108bdf6b02065ce03 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Wed, 25 Apr 2018 08:12:11 -0400
Subject: [PATCH] correct impl of function upcast I think
---
gcbpv.tex | 16 ++++++++++------
1 file changed, 10 insertions(+), 6 deletions(-)
diff --git a/gcbpv.tex b/gcbpv.tex
index bb8a398..f014685 100644
--- a/gcbpv.tex
+++ b/gcbpv.tex
@@ -579,6 +579,7 @@ We implement the appropriate casts and their adjoints as follows
\[ \upcast {U \u M} {U \dync} x = \u \roll \thunk [ \pi_{\u M} \mapsto \force x; \pi_{\u M'} \mapsto \err ] \]
\begin{figure}
+ \begin{mathpar}
\inferrule
{A \vtype \and \u B \ctype}
{A \to \u B \ctype}
@@ -604,22 +605,25 @@ We implement the appropriate casts and their adjoints as follows
{\Phi \pipe \Psi \vdash M_1 \ltdyn M_2 : A_1 \to \u B_1 \ltdyn A_2 \to \u B_2 \and
\Phi \vdash v_1 \ltdyn v_2 : A_1 \ltdyn A_2}
{\Phi \pipe \Psi \vdash M_1(v_1) \ltdyn M_2(v_2) : \u B_1 \ltdyn \u B_2}
+ \end{mathpar}
\caption{Function Type}
\end{figure}
\begin{figure}
+ \begin{mathpar}
\inferrule
{}
- {\dncast {A_1 \to \u B_1}{A_2 \to \u B_2} \bullet \equidyn \lambda x:A_1. \dncast {\u B_1}{\u B_2} (\bullet(\upcast {A_1} {A_2}))}
+ {\dncast {A_1 \to \u B_1}{A_2 \to \u B_2} \bullet \equidyn \lambda x:A_1. \dncast {\u B_1}{\u B_2} (\bullet(\upcast {A_1} {A_2} x))}
\inferrule
{}
- {\upcast {U({A_1 \to \u B_1})}{U({A_2 \to \u B_2})} (f : U(A_1 \to \u B_1)) \equidyn
- \thunk \lambda x_2 : A_2. \force \upcast{U \u B_1}{U \u B_2}(\thunk ((\force f)))
+ {\upcast {U({A_1 \to \u B_1})}{U({A_2 \to \u B_2})} (f : U(A_1 \to \u B_1)) \equidyn\\
+ \thunk \lambda x_2 : A_2.
+ \lett x_1 = \dncast{\u F A_1}{\u F A_2}\ret x_2;
+ (\force \upcast{U \u B_1}{U \u B_2}(\thunk ((\force f)(x_1))))
}
-
-
-
+
+ \end{mathpar}
\caption{Function Contract Theorem, Proof}
\end{figure}
--
GitLab