more work on prose, organize the formalizations and init guarded cubical version

failures/transitivity-in-the-limit.tex

+\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{\dyn}{\text{Dyn}}
+\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}}
+\newcommand{\errp}[1]{\mho_{#1}}
+\newcommand{\kerrp}[2]{\mho^{#1}_{#2}}
+\newcommand{\err}{\mho}
+\newcommand{\errlift}{L_\err}
+\newcommand{\ostar}{\circledast}
+
+\newcommand{\ltdynp}[1]{\mathrel{\sqsubseteq_{#1}}}
+\newcommand{\ltdynlift}[1]{\mathrel{\sqsubseteq_{\errlift#1}}}
+\newcommand{\ltprecp}[1]{\mathrel{\sqsubseteq^{\prec}_{\errlift #1}}}
+\newcommand{\ltsuccp}[1]{\mathrel{\sqsubseteq^{\succ}_{#1}}}
+
+\newcommand{\kltp}[2]{\mathrel{\sqsubseteq^{#1}_{#2}}}
+
+\newcommand{\ltgt}[1]{\mathbin{\langle\mspace{-1mu}#1\mspace{-1mu}\rangle}}
+\newcommand{\fmap}{\ltgt{\$}}
+\newcommand{\monto}{\mathrel{\to_{m}}}
+\newcommand{\linto}{\multimap}
+
+\begin{document}
+
+\title{Semantics of Gradual Types in SGDT}
+\author{Max S. New}
+
+\maketitle
+
+\section{Goals}
+
+We want to define a denotational semantics for the core language of
+GTLC and prove graduality.
+
+Here's roughly the structure required
+\begin{verbatim}
+record GTLC(U)
+  type : U
+  tm : type -> U
+  _<ty=_ : PreOrder type
+  _<tm=_ : PreOrder (Sigma A (tm A))
+  impl : (A, M) <tm= (B,N) -> A <ty= B
+
+  dyn : type
+  dynTop : {A} -> A <ty= dyn
+
+  ans : type
+  yes : tm ans
+  no  : tm ans
+
+  arr : type -> type -> type
+  lam : (tm A -> tm B) -> tm (arr A B)
+  app : tm (arr A B) -> tm A -> tm B
+  -- beta, eta
+
+  up : A <ty= B -> tm A -> tm B
+  upR : ...
+
+  dn : A <ty= B -> tm B -> tm A
+  
+\end{verbatim}
+
+\section{Error predomains and domains}
+
+First, we need to define our monad.
+\begin{definition}
+  Define the error-lift type as a solution to the guarded recursive
+  domain equation:
+  \[ \errlift X \cong (X + 1 + \later \errlift X) \]
+
+  We label the three injections as follows:
+  \begin{align*}
+    \eta &: X \to \errlift X\\
+    \err &: \errlift X\\
+    \theta &: \later \errlift X \to \errlift X
+  \end{align*}
+
+  This carries the structure of a strong monad, with $\eta$ as the
+  unit and the join defined by L\"ob induction as follows:
+  \begin{align*}
+    \mu(\eta x) &= x\\
+    \mu(\mho) &= \mho\\
+    \mu(\theta(u)) &= \theta (\mu^\later \ostar u)
+  \end{align*}
+  With map (implying strength) defined as
+  \begin{align*}
+    \errlift f(\eta x) &= f x\\
+    \errlift f(\mho) &= \mho\\
+    \errlift f(\theta(u)) &= \theta ((\errlift f)^\later \ostar u)
+  \end{align*}
+  And the equational laws of a monad can be proven using L\"ob
+  induction.
+\end{definition}
+
+This can be seen as simply a composition of two monads using a
+distributive law: the error monad and the recursive lift monad.
+%
+However, we present them as one combined monad because in gradual
+typing we are interested in a specific ordering relation called the
+\emph{error ordering} where $\err$ is the least element. This is
+\emph{not} the composition of the lift and error monad, which would
+instead have the error as an isolated, maximal element.
+
+We can define this error ordering as a variation on the weak
+simulation relations of prior work:
+\begin{definition}
+  Let $X$ be a type and $\sqsubseteq_X$ a binary relation. We define
+  $\ltdynp{\errlift X} : \errlift X \to \errlift X \to \prop$ as follows:
+  \begin{align*}
+    \err \ltdynlift X d &= \top\\
+    \eta x \ltdynlift X \eta y &= x \ltdynp X y\\
+    \eta x \ltdynlift X \err &= \bot\\
+    \eta x \ltdynlift X \theta t &= \exists{n:\mathbb N}.\exists{y: X}. \theta t = \delta^n (\eta y) \wedge x \ltdynp X y\\
+    \theta s \ltdynlift X \eta y &= \exists{n:\mathbb N}.(\theta s = \delta^n \err)\vee(\exists{y: X}. \theta t = \delta^n (\eta y) \wedge x \ltdynp X y)\\
+    \theta s \ltdynlift X \err &= \exists{n:\mathbb N}.\theta s = \delta^n \err\\
+    \theta s \ltdynlift X \theta t &= \later[l \leftarrow s,r\leftarrow t] s \ltdynlift X t
+  \end{align*}
+\end{definition}
+
+\begin{lemma}
+  When $\ltdynp X$ is reflexive, so is $\ltdynlift X$.
+\end{lemma}
+\begin{proof}
+  By L\"ob induction on the proposition $\forall d: \errlift X. d
+  \ltdynlift X d$. Error and return cases are immediate.  We need to
+  show
+  \[ \theta t \ltdynlift X \theta t = \later[l \leftarrow t,r\leftarrow t] l \ltdynlift X r = \later[l \leftarrow t] l \ltdynlift X l \]
+  The inductive hypothesis $h : \later (\forall d: \errlift X. d \ltdynlift X d)$
+  We can then conclude
+  \[ \text{next}[f \leftarrow h, l \leftarrow t]. h l \]
+\end{proof}
+
+Unfortunately, transitivity is not preserved.
+%
+The problematic case is of the form $\theta s \ltdynlift X \theta t
+\ltdynlift X \eta z$. In this case we know $\theta t = \delta^n (\eta
+y)$ but we cannot conclude that $\theta s$ must eventually terminate!
+In fact this is false in the semantics because it might be that
+$\theta s$ is only related to $\theta t$ because we ran out of fuel,
+and actually $s$ is a diverging computation.
+
+However, this should support transitive reasoning \emph{in the limit},
+i.e., if the equivalence holds for \emph{all} levels of approximation
+then eventually if $\theta t$ terminates, at high enough level of
+approximation it will no longer be related to the diverging
+computation.
+%
+This reasoning \emph{in the limit} is accomplished analytically by
+quantification over all steps.
+%
+Here we accomplish it by using \emph{clocks} and \emph{clock
+quantification}.
+%
+That is rather than a denotation of a syntactic type being a type it
+will be given by a ``clocked'' type:
+
+\begin{definition}
+  A \emph{clocked} type $X$ is an element of $K \to U$.
+
+  We call $\forall k:K. X k$, the \emph{limit} of $X$.
+\end{definition}
+
+Note that, similar to the interval in cubical type theory, $K$ is not
+a type, but only a ``pseudo-type'' that we can quantify over in the
+type $\Pi_{k:K} B$.
+%
+Next, we need a ``clocked'' error ordering associated to every type.
+%
+This will be assumed to be reflexive at each level of approximation,
+but only transitive in the limit.
+
+\begin{definition}
+  A \emph{clocked} preorder on a clocked type $X : K \to U$ is a
+  clocked relation $\kltp {} X : \forall k. X_k \to X_k \to \prop$ satisfying
+  \begin{enumerate}
+  \item Clocked Reflexivity $\forall k. \prod_{x:X_k} x \kltp k X x$
+  \item Transitivity in the limit $\prod_{x,y,z:\forall k. X_k} x \kltp \omega X y \to y \kltp \omega X z \to x \kltp \omega X z$
+  \end{enumerate}
+
+  Where 
+  \[ x \kltp \omega X y = \forall k. x_k \kltp k X y_k \]
+
+  A \emph{monotone function} is a function $f : \forall k. X_0 k \to
+  Y_0 k$ satisfying monotonicity:
+  \[ \forall k.\prod_{x,x':X_0^k} x \kltp k X x' \to f_k x \kltp k Y f_k x' \]
+\end{definition}
+
+For any clocked preorder we can construct the delayed preorder by
+\begin{definition}
+  Define $\later : K \to (K \to U) \to (K \to U)$ by
+  \[ (\later X)^k = \later^k X^k \]
+  and on preorders by:
+  \begin{align*}
+    x \kltp k {\later X} y &= \later^k[l\leftarrow x, r\leftarrow y].~l \kltp k {X} r
+  \end{align*}
+  
+\end{definition}
+
+Then we can define our semantic notions
+\begin{definition}
+  An \emph{error predomain} $X$ consists of
+  \begin{enumerate}
+  \item A clocked type $X_0$
+  \item A clocked preorder $\kltp {} X$ on $X_0$ 
+  \end{enumerate}
+  A morphism of error predomains is a monotone function.
+
+  An \emph{error domain} is an error predomain $X$ with
+  \begin{enumerate}
+  \item A least element $\kerrp {} X : \forall k. X$, i.e., it
+    satisfies $\forall k. \prod_{x:X_k} \kerrp k X \kltp k X x$.
+  \item A monotone ``thunk'' function $\theta_X : \later X \to X$
+  \end{enumerate}
+  A morphism of error domains is a morphism of the underlying error
+  predomains.
+
+  A \emph{linear} morphism of error domains $S : X \multimap Y$ is a
+  morphism of error domains additionally satisfying
+  \begin{enumerate}
+  \item Error preservation $S^k \err^k_X = \err^k_Y$
+  \item Thunk preservation $S^k (\theta^k_X x) = \theta^k_Y (S^k \fmap x)$
+  \end{enumerate}
+\end{definition}
+
+Finally we can return to our original goal of defining the monad for our semantics!
+%
+
+\begin{lemma}
+  next and $\delta$ are monotone
+\end{lemma}
+
+\begin{definition}
+  Let $X$ be an error predomain a binary relation. We define the error
+  domain $\errlift X$ as
+
+  TODO: put the ks in the right spots
+
+  \begin{enumerate}
+  \item $(\errlift X)_0^k = \mu L. X_0^k + 1 + \later^k L$
+  \item Ordering defined by cases:
+    \begin{align*}
+      \err \kltp k {\errlift X} d &= \top\\
+      \eta x \kltp k {\errlift X} \eta y &= x \ltdynp X y\\
+      \eta x \kltp k {\errlift X} \err &= \bot\\
+      \eta x \kltp k {\errlift X} \theta t &= \exists{n:\mathbb N}.\exists{y: X}. \theta t = \delta^n (\eta y) \wedge x \ltdynp X y\\
+      \theta s \kltp k {\errlift X} \eta y &= \exists{n:\mathbb N}.(\theta s = \delta^n \err)\vee(\exists{y: X}. \theta t = \delta^n (\eta y) \wedge x \ltdynp X y)\\
+      \theta s \kltp k {\errlift X} \err &= \exists{n:\mathbb N}.\theta s = \delta^n \err\\
+      \theta s \kltp k {\errlift X} \theta t &= \later[l \leftarrow s,r\leftarrow t] s \kltp k {\errlift X} t
+    \end{align*}
+  \item reflexive: as above
+  \item TODO: transitive in the limit
+  \item TODO: strong monad
+  \end{enumerate}
+\end{definition}
+
+\begin{lemma}
+  $\errlift X$ is the free error domain on $X$, i.e., it is left
+  adjoint to the forgetful functor from the category of error domains
+  and linear maps to the category of predomains.
+\end{lemma}
+
+\begin{lemma}
+  The adjunction is monadic: error domains are precisely algebras of
+  the free error domain. Is this true?
+\end{lemma}
+
+\section{Lazy Semantics}
+
+To define a semantics for lazy gradually typed language, we first need
+to define our \emph{universal} error domain. Unless we add in features
+like pattern matching on the dynamic type, there is some freedom in
+this choice. We present two natural solutions:
+
+The first is a classic-looking dynamic type: the lift of the sum of
+the base type and the function type. A notable difference are the
+guarded recursive uses.
+\[ \dyn_+ \cong \errlift (2 + (\later \dyn_+ \monto \later \dyn_+)) \]
+The second is slightly closer to untyped lambda calculus: we take a
+product rather than a sum, and only need to lift the base type itself.
+\[ \dyn_- \cong \errlift 2 \times (\later \dyn_- \monto \later \dyn_-) \]
+The idea here is that any dynamically typed term can be safely applied
+to any number of arguments and at some point ``projected'' to return a
+boolean, which will actually cause computation to occur as indicated
+by the $\errlift$.
+
+To construct these domains we need to be able to solve recursive
+domain equations \emph{of error domains}. To do this we simply need to
+show that the universe of error predomains is a predomain.
+
+\begin{definition}
+  Define $\theta_{\predom} : \later \predom \to \predom$ as follows
+  \begin{align*}
+    \theta_{\predom}P &= (\later[(X,\ltdynp X) \leftarrow P] X, )
+  \end{align*}
+\end{definition}
+
+
+\end{document}

formalizations/guarded-cubical/ErrorDomains.agda

+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+open import Later
+
+-- | TODO: everything lol

formalizations/guarded-cubical/LICENSE.txt

+Later.agda is subject to the following license:
+
+MIT License
+
+Copyright (c) 2019 Niccolò Veltri and Andrea Vezzosi
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

formalizations/guarded-cubical/Later.agda

+{-# OPTIONS --cubical --rewriting --guarded #-}
+module Later where
+
+-- | This file is from the supplementary material for the paper
+-- | https://doi.org/10.1145/3372885.3373814
+-- | and is originally written by Niccolò Veltri and Andrea Vezzosi
+-- | see the LICENSE.txt for their license.
+
+open import Agda.Builtin.Equality renaming (_≡_ to _≣_)
+open import Agda.Builtin.Equality.Rewrite
+open import Agda.Builtin.Sigma
+
+open import Cubical.Core.Everything
+open import Cubical.Foundations.Everything
+
+module Prims where
+  primitive
+    primLockUniv : Set₁
+
+open Prims renaming (primLockUniv to LockU) public
+
+private
+  variable
+    l : Level
+    A B : Set l
+
+-- We postulate Tick as it is supposed to be an abstract sort.
+postulate
+  Tick : LockU
+
+▹_ : ∀ {l} → Set l → Set l
+▹_ A = (@tick x : Tick) -> A
+
+▸_ : ∀ {l} → ▹ Set l → Set l
+▸ A = (@tick x : Tick) → A x
+
+next : A → ▹ A
+next x _ = x
+
+_⊛_ : ▹ (A → B) → ▹ A → ▹ B
+_⊛_ f x a = f a (x a)
+
+map▹ : (f : A → B) → ▹ A → ▹ B
+map▹ f x α = f (x α)
+
+-- The behaviour of fix is encoded with rewrite rules, following the
+-- definitional equalities of TCTT.
+postulate
+  dfix : ∀ {l} {A : Set l} → (f : ▹ A → A) → I → ▹ A
+  dfix-beta : ∀ {l} {A : Set l} → (f : ▹ A → A) → dfix f i1 ≣ next (f (dfix f i0))
+
+{-# REWRITE dfix-beta #-}
+
+pfix : ∀ {l} {A : Set l} → (f : ▹ A → A) → dfix f i0 ≡ next (f (dfix f i0))
+pfix f i = dfix f i
+
+abstract
+  fix : ∀ {l} {A : Set l} → (f : ▹ A → A) → A
+  fix f = f (pfix f i0)
+
+  fix-eq : ∀ {l} {A : Set l} → (f : ▹ A → A) → fix f ≡ f (next (fix f))
+  fix-eq f = cong f (pfix f)
+
+later-ext : ∀ {A : ▹ Set} → {f g : ▸ A} → (▸ \ a → f a ≡ g a) → f ≡ g
+later-ext eq i a = eq a i
+
+
+
+
+transpLater : ∀ (A : I → ▹ Set) → ▸ (A i0) → ▸ (A i1)
+transpLater A u0 a = transp (\ i → A i a) i0 (u0 a)
+
+hcompLater : ∀ (A : ▹ Set) φ (u : I → Partial φ (▸ A)) → (u0 : ▸ A [ φ ↦ u i0 ]) → ▸ A
+hcompLater A φ u u0 a = hcomp (\ { i (φ = i1) → u i 1=1 a }) (outS u0 a)

formalizations/guarded-cubical/gradual-typing-sgdt.agda-lib

+name: gradual-typing-sgdt
+include: .
+depend: cubical

formalizations/home-rolled/ErrorDomains.agda

+module ErrorDomains where
+
+𝕍 : Set₂
+𝕍 = Set₁
+
+𝕌 : 𝕍
+𝕌 = Set
+
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Data.Product
+
+record Preorder : 𝕍 where
+  field
+    X   : 𝕌
+    _⊑_ : X → X → 𝕌
+    refl : ∀ (x : X) → x ⊑ x
+    trans : ∀ {x y z : X} → x ⊑ y → y ⊑ z → x ⊑ z
+
+infixr 20 _⇨_
+infixr 20 _⇒_
+
+record _⇨_ (X : Preorder) (Y : Preorder) : 𝕌 where
+  module X = Preorder X
+  module Y = Preorder Y
+  field
+    f   : X.X → Y.X
+    mon : ∀ {x y} → X._⊑_ x y → Y._⊑_ (f x) (f y)
+
+app : ∀ {X Y} → (X ⇨ Y) → Preorder.X X → Preorder.X Y
+app = _⇨_.f
+
+_$_ = app
+
+_⇒_ : Preorder → Preorder → Preorder
+X ⇒ Y = record { X = X ⇨ Y
+               ; _⊑_ = λ f g → (x : X.X) → _⇨_.f f x ⊑y _⇨_.f g x
+               ; refl = λ x x₁ → _⇨_.mon x (X.refl x₁)
+               ; trans = λ p1 p2 x → Y.trans (p1 x) (p2 x) }
+  where
+    module X = Preorder X
+    module Y = Preorder Y
+    _⊑y_ = Y._⊑_
+
+_⊨_⊑_ : (X : Preorder) → Preorder.X X → Preorder.X X → Set
+X ⊨ x ⊑ x' = Preorder._⊑_ X x x'
+
+record _⊨_≣_ (X : Preorder) (x y : Preorder.X X) : Set where
+  module X = Preorder X
+  _⊑_ = X._⊑_
+  field
+    to  : x ⊑ y
+    fro : y ⊑ x
+
+record _⇔_ (X : Preorder) (Y : Preorder) : Set where
+  field
+    to  : X ⇨ Y
+    fro : Y ⇨ X
+    eqX : ∀ x → X ⊨ app fro (app to x) ≣ x
+    eqY : ∀ y → Y ⊨ app to (app fro y) ≣ y
+
+record _◃_ (X Y : Preorder) : Set where
+  _⊑y_ = Preorder._⊑_ Y
+  field
+    emb  : X ⇨ Y
+    prj  : Y ⇨ X
+    projection : ∀ y → Y ⊨ app emb (app prj y) ⊑ y
+    retraction : ∀ x → X ⊨ x ≣ app prj (app emb x)
+
+product : Preorder → Preorder → Preorder
+product X Y = record { X = X.X × Y.X
+                     ; _⊑_ = λ p1 p2 → (proj₁ p1 ⊑x proj₁ p2) × (proj₂ p1 ⊑y proj₂ p2)
+                     ; refl = λ x → (X.refl (proj₁ x)) , (Y.refl (proj₂ x))
+                     ; trans = λ leq1 leq2 → (X.trans (proj₁ leq1) (proj₁ leq2)) , Y.trans (proj₂ leq1) (proj₂ leq2)
+                     }
+  where module X = Preorder X
+        _⊑x_ = X._⊑_
+        module Y = Preorder Y
+        _⊑y_ = Y._⊑_
+
+data TransClosure {X : 𝕌}(_R_ : X → X → 𝕌) : X → X → 𝕌 where
+  one  : ∀ {x y} → x R y → TransClosure _R_ x y
+  more : ∀ {x y z} → x R y → TransClosure _R_ y z → TransClosure _R_ x z
+
+transClosureAppend : ∀ {X}{_R_ : X → _}{x y z} → TransClosure _R_ x y → TransClosure _R_ y z → TransClosure _R_ x z
+transClosureAppend (one x) pyz      = more x pyz
+transClosureAppend (more x pxy) pyz = more x (transClosureAppend pxy pyz)
+
+record ReflGraph : 𝕍 where
+  field
+    X : 𝕌
+    _⊑_ : X → X → 𝕌
+    refl : ∀ x → x ⊑ x
+
+_^+ : ReflGraph → Preorder
+G ^+ = record
+  { X = G.X
+  ; _⊑_ = TransClosure G._⊑_
+  ; refl = λ x → one (G.refl x)
+  ; trans = transClosureAppend
+  }
+  where module G = ReflGraph G
+
+-- Let's get some clocks going
+postulate
+  K : 𝕌
+  ▸^  : K → 𝕌 → 𝕌
+  ▸^' : K → 𝕍 → 𝕍
+  next^ : ∀ {A}{k} → A → ▸^ k A
+  gfix^ : ∀ {k : K}{X : 𝕌} → (▸^ k X → X) → X
+  gfix^-unfold : ∀ {k}{X} (f : ▸^ k X → X) → gfix^ f ≡ f (next^ (gfix^ f))
+
+  next^' : ∀ {A}{k} → A → ▸^' k A
+  gfix^' : ∀ {k : K}{X : 𝕍} → (▸^' k X → X) → X
+  gfix^'-unfold : ∀ {k}{X} (f : ▸^' k X → X) → gfix^' f ≡ f (next^' (gfix^' f))
+

gtlc-fake.agda → formalizations/home-rolled/GTLC.agda

+-- | The below is an attempt to describe the semantics of gradually
+-- | typed languages in a HOAS style.
+--
+-- | Warning: this might not make any sense without directed type
+-- | theory!
 
+open import ErrorDomains
 open import Relation.Binary.PropositionalEquality using (_≡_)
 open import Data.Product
 
-postulate
-
-  ▸ : Set → Set
-  K : Set
-
-𝕌 : Set₁
-𝕌 = Set
-
-ℙ : Set₁
-ℙ = Set
-
-record Preorder : Set₁ where
-  field
-    X   : 𝕌
-    _⊑_ : X → X → ℙ
-    refl : ∀ (x : X) → x ⊑ x
-    trans : ∀ {x y z : X} → x ⊑ y → y ⊑ z → x ⊑ z
-
-infixr 20 _⇨_
-infixr 20 _⇒_
-
-record _⇨_ (X : Preorder) (Y : Preorder) : Set where
-  module X = Preorder X
-  module Y = Preorder Y
-  field
-    f   : X.X → Y.X
-    mon : ∀ {x y} → X._⊑_ x y → Y._⊑_ (f x) (f y)
-
-app : ∀ {X Y} → (X ⇨ Y) → Preorder.X X → Preorder.X Y
-app = _⇨_.f
-
-_$_ = app
-
-_⇒_ : Preorder → Preorder → Preorder
-X ⇒ Y = record { X = X ⇨ Y
-               ; _⊑_ = λ f g → (x : X.X) → _⇨_.f f x ⊑y _⇨_.f g x
-               ; refl = λ x x₁ → _⇨_.mon x (X.refl x₁)
-               ; trans = λ p1 p2 x → Y.trans (p1 x) (p2 x) }
-  where
-    module X = Preorder X
-    module Y = Preorder Y
-    _⊑y_ = Y._⊑_
-
-_⊨_⊑_ : (X : Preorder) → Preorder.X X → Preorder.X X → Set
-X ⊨ x ⊑ x' = Preorder._⊑_ X x x'
-
-record _⊨_≣_ (X : Preorder) (x y : Preorder.X X) : Set where
-  module X = Preorder X
-  _⊑_ = X._⊑_
-  field
-    to  : x ⊑ y
-    fro : y ⊑ x
-
-record _⇔_ (X : Preorder) (Y : Preorder) : Set where
-  field
-    to  : X ⇨ Y
-    fro : Y ⇨ X
-    eqX : ∀ x → X ⊨ app fro (app to x) ≣ x
-    eqY : ∀ y → Y ⊨ app to (app fro y) ≣ y
-
-record _◃_ (X Y : Preorder) : Set where
-  _⊑y_ = Preorder._⊑_ Y
-  field
-    emb  : X ⇨ Y
-    prj  : Y ⇨ X
-    projection : ∀ y → Y ⊨ app emb (app prj y) ⊑ y
-    retraction : ∀ x → X ⊨ x ≣ app prj (app emb x)
-
 op : Preorder → Preorder
 op X = record
          { X = X.X
@@ -85,17 +23,6 @@ opF {X}{Y} f = record { f = f.f ; mon = _⇨_.mon f }
         module Y = Preorder Y
         module f = _⇨_ f
 
-product : Preorder → Preorder → Preorder
-product X Y = record { X = X.X × Y.X
-                     ; _⊑_ = λ p1 p2 → (proj₁ p1 ⊑x proj₁ p2) × (proj₂ p1 ⊑y proj₂ p2)
-                     ; refl = λ x → (X.refl (proj₁ x)) , (Y.refl (proj₂ x))
-                     ; trans = λ leq1 leq2 → (X.trans (proj₁ leq1) (proj₁ leq2)) , Y.trans (proj₂ leq1) (proj₂ leq2)
-                     }
-  where module X = Preorder X
-        _⊑x_ = X._⊑_
-        module Y = Preorder Y
-        _⊑y_ = Y._⊑_
-
 record FiberPts {X : Preorder}{Y : Preorder} (f : X ⇨ Y) (y : Preorder.X Y) : Set where
   field
     pt : Preorder.X X

gtlc.tex

 \documentclass{article}
+
 \usepackage{amssymb}
 \usepackage{amsmath}
 \usepackage{amsthm}
@@ -12,11 +13,14 @@
 \newtheorem{definition}{Definition}[section]
 \newtheorem{lemma}{Lemma}[section]
 
+\newcommand{\bool}{2}
 \newcommand{\dyn}{\text{Dyn}}
 \newcommand{\dynv}{\text{Dyn}^+}
 \newcommand{\dync}{\text{Dyn}^-}
 \newcommand{\good}[1]{\text{good}_{#1}}
 \newcommand{\prop}{\mathbb P}
+\newcommand{\smallU}{\mathbb U}
+\newcommand{\bigU}{\mathbb V}
 \newcommand{\with}{\mathrel{\&}}
 \newcommand{\eqv}{\simeq}
 \newcommand{\soln}{\text{Sol}}
@@ -38,7 +42,11 @@
 \newcommand{\ltgt}[1]{\mathbin{\langle\mspace{-1mu}#1\mspace{-1mu}\rangle}}
 \newcommand{\fmap}{\ltgt{\$}}
 \newcommand{\monto}{\mathrel{\to_{m}}}
+\newcommand{\predom}{\text{$\mho$PreDom}}
+\newcommand{\dom}{\text{Dom}}
 \newcommand{\linto}{\multimap}
+\newcommand{\Next}{\text{next}}
+\newcommand{\thinkp}[1]{\theta_{#1}}
 
 \begin{document}
 
@@ -51,49 +59,164 @@
 
 We want to define a denotational semantics for the core language of
 GTLC and prove graduality.
+%
+For lazy gradual typing, based on New and Licata, we need to construct
+a vertically thin cartesian closed pro-arrow equipment with a greatest
+type, least element of each hom set and a weak boolean type.
+
+New and Licata used a denotational semantics based on classical
+analytic domain theory to construct such models. Here we will use
+\emph{synthetic guarded domain theory} to sidestep any side-conditions
+on constructing solutions to domain equations. We work internal to a
+model of multi-clock synthetic guarded domain theory. We use two
+universes $\mathbb U \leq \mathbb V$.
+
+For gradual typing we need to develop a notion of domain that includes
+an \emph{error ordering} with respect to which all constructions in
+the language are monotone and and the errors and gradual type casts
+are characterized by universal properties. We also need to construct
+in each model a \emph{universal} (pre-)domain to interpret the
+``dynamic'' type.
+
+For instance, for a CBN gradual language with functions and booleans a
+suitable domain can be constructed as:
+\[ \dync \cong \errlift \bool \times (\later \dync \monto \later \dync) \]
+where $\errlift$ is an appropriate combination of the error and lift
+monads, $\later$ provides the necessary guarding and $\monto$ is the
+set of \emph{monotone} functions.  A CBV gradual language with
+functions and booleans could instead use
+\[ \dynv \cong \bool + (\later \dynv \monto \errlift(\later\dynv))\]
 
-Here's roughly the structure required
-\begin{verbatim}
-record GTLC(U)
-  type : U
-  tm : type -> U
-  _<ty=_ : PreOrder type
-  _<tm=_ : PreOrder (Sigma A (tm A))
-  impl : (A, M) <tm= (B,N) -> A <ty= B
+\section{Error predomains and domains}
 
-  dyn : type
-  dynTop : {A} -> A <ty= dyn
+We start by defining our notion of predomain and domain and showing
+how to solve recursive domain equations.
+%
+All of the constructions (later, fix, etc) in this section are
+parameterized by an arbitrary clock variable $k : K$, but to avoid
+clutter we leave it implicit.
 
-  ans : type
-  yes : tm ans
-  no  : tm ans
+Our notion of predomain is simply that of a (constructive)
+\emph{preorder}, and our notion of domain is a predomain with a least
+element.
+\begin{definition}
+  An error predomain $X$ consists of
+  \begin{enumerate}
+  \item A type $X_0 : \smallU$
+  \item An order ``relation'' $\ltdynp X : X_0 \to X_0 \to \smallU$
+  \item Satisfying reflexivity, i.e., $x \ltdynp X x$ for every $x$.
+  \item And transitivity, if $x \ltdynp X y$ and $y \ltdynp X z$ then
+    $x \ltdynp X z$.
+  \end{enumerate}
+  We write the universe of predomains as $\predom : \bigU$.
 
-  arr : type -> type -> type
-  lam : (tm A -> tm B) -> tm (arr A B)
-  app : tm (arr A B) -> tm A -> tm B
-  -- beta, eta
+  A monotone function $f : X \to Y$ between error predomains consists
+  of
+  \begin{enumerate}
+  \item A function on the underlying sets $f_0 : X_0 \to Y_0$
+  \item That preserves the ordering: $f_1 : (x \ltdynp X x') \to (f_0x \ltdynp X f_0 x')$
+  \end{enumerate}
 
-  up : A <ty= B -> tm A -> tm B
-  upR : ...
+  We write the type of monotone functions from $X$ to $Y$ as $X \monto Y : \smallU$
+  Furthermore, the type of monotone functions can be extended to a
+  predomain with pointwise ordering. We abusively also write $X \monto
+  Y : \predom$
+\end{definition}
 
-  dn : A <ty= B -> tm B -> tm A
-  
-\end{verbatim}
+Strangely enough for our purposes it is important that the preorder is
+not in a proof-irrelevant universe, but we do not seem to care about
+the equality of ordering proofs. So we seem to have a weird
+intermediate point between proper preorders and categories where there
+might be many different proofs but we impose no ``laws'' on the
+manipulation of these proofs. Michael Arntzenius calls these ``lawless
+categories''.
 
-\section{Error predomains and domains}
+Next, to solve recursive domain equations, we need to prove that the
+universe of error predomains is a domain in the sense of guarded
+domain theory that there is a $\later$-algebra $\theta : \later
+\predom \to \predom$
+
+\begin{definition}
+  Given $X^\later : \later \predom$, define a predomain $\later X^\later$ as
+  follows:
+  \begin{enumerate}
+  \item $(\later X^\later)_0 = \later[X \leftarrow X^\later] X_0$
+  \item $x^\later \ltdynp {\later X^\later} y^\later = \later[X \leftarrow X^\later, x \leftarrow x^\later, y \leftarrow y^\later] x \ltdynp X y$
+  \item Given $x^\later$,
+    \begin{align*}
+      \later[X \leftarrow X^\later, x \leftarrow x^\later, y \leftarrow x^\later] x \ltdynp X y
+      &\equiv \later[X \leftarrow X^\later, x \leftarrow x^\later] x \ltdynp X x
+    \end{align*}
+    Which we can prove as
+    \[ \Next[X \leftarrow X^\later, x \leftarrow x^\later] \text{refl}_X x\]
+    or in applicative style
+    \[ \Next\,\text{refl} \ostar X^\later \ostar x^\later \]
+  \item Given $p_{xy}^\later : x^\later \ltdynp {\later X^\later} y^\later$ and
+    $p_{yz}^\later : y^\later \ltdynp {\later X^\later} z^\later$, we need to show
+    \begin{align*}
+      \later[X \leftarrow X^\later, x \leftarrow x^\later, z \leftarrow z^\later] x \ltdynp X z
+      &\equiv \later[X \leftarrow X^\later, x \leftarrow x^\later,y\leftarrow y^\later, z \leftarrow z^\later] x \ltdynp X z
+    \end{align*}
+    Which we prove as
+    \[ \Next[X \leftarrow X^\later, x \leftarrow x^\later,y\leftarrow y^\later, z \leftarrow z^\later,p_{xy}\leftarrow p_{xy}^\later, p_{yz}\leftarrow p_{yz}^\later] \text{trans}_X p_{xy} p_{yz} \]
+    or in applicative style
+    \[ \Next\,\text{trans} \ostar X^\later \ostar x^\later\ostar y^\later\ostar z^\later \ostar p_{xy}^\later \ostar p_{yz}^\later \]
+  \end{enumerate}
+\end{definition}
+When $X : \predom$, we will write $\later X$ for $\later (\Next\,X)$
+
+We can then define our notion of \emph{error domain} as error
+predomains that have a suitable notion of error and have a
+\emph{monotone} $\later$-algebra.
+\begin{definition}
+  An error domain $X$ is an error predomain with furthermore
+  \begin{enumerate}
+  \item An element $\errp X : X_0$ that is the least element $\errp X \ltdynp X x$
+  \item A monotone function $\thinkp X : \later X \to X$
+  \end{enumerate}
+  We write the universe of error domains as $\dom : \bigU$ and we will
+  (usually?) suppress the obvious coercion $U : \dom \to \predom$
+
+  When $X$ is an error predomain and $Y$ is an error domain, $X \monto
+  Y$ is an error domain with
+  \begin{enumerate}
+  \item $\errp {X \monto Y} = \lambda x. \errp Y$
+  \item $\thinkp {X \monto Y} f = \lambda x. \thinkp Y (f \ostar (\Next\, x)) $
+  \end{enumerate}
+\end{definition}
 
-First, we need to define our monad.
+And finally we can define the error-lift monad, which defines the free
+error domain from an error predomain.
 \begin{definition}
+  Given any predomain $X : \predom$, we define the error lift $\errlift X$ as follows
+
+  \begin{enumerate}
+  \item First, $(\errlift X)_0$ is defined as the solution to the
+    guarded domain equation:
+    \[ (\errlift X)_0 \cong (X_0 + 1 + \later (\errlift X)_0) \]
+
+    We label the three injections as follows:
+    \begin{align*}
+      \eta &: X \to \errlift X\\
+      \err &: \errlift X\\
+      \theta &: \later \errlift X \to \errlift X
+    \end{align*}
+
+  \item We define the order relation, $\ltdynp {\errlift X}$ as the
+    transitive closure of $\wr$, which is defined as:
+
+    \begin{align*}
+      \err \wr r &= 1\\
+      (\eta x) \wr (\eta y) &= x \ltdynp X y\\
+      (\theta s) \wr (\theta t) &= (\Next\; \wr) \ostar s \ostar t\\
+      (\eta x) \wr (\theta t) &= \Sigma_{n:\mathbb N}\Sigma_{y:X_0} (\theta t = \delta^n (\eta y)) \times (x \ltdynp X y)\\
+      (\theta s) \wr (\eta y) &= \Sigma_{n:\mathbb N}\Sigma_{x:X_0} (\theta s = \delta^n (\eta x)) \times (x \ltdynp X y)\\
+    \end{align*}
+  \end{enumerate}
+  
   Define the error-lift type as a solution to the guarded recursive
   domain equation:
-  \[ \errlift X \cong (X + 1 + \later \errlift X) \]
 
-  We label the three injections as follows:
-  \begin{align*}
-    \eta &: X \to \errlift X\\
-    \err &: \errlift X\\
-    \theta &: \later \errlift X \to \errlift X
-  \end{align*}
 
   This carries the structure of a strong monad, with $\eta$ as the
   unit and the join defined by L\"ob induction as follows:
@@ -307,12 +430,12 @@ To construct these domains we need to be able to solve recursive
 domain equations \emph{of error domains}. To do this we simply need to
 show that the universe of error predomains is a predomain.
 
-\begin{definition}
-  Define $\theta_{\predom} : \later \predom \to \predom$ as follows
-  \begin{align*}
-    \theta_{\predom}P &= (\later[(X,\ltdynp X) \leftarrow P] X, )
-  \end{align*}
-\end{definition}
+%% \begin{definition}
+%%   Define $\theta_{\predom} : \later \predom \to \predom$ as follows
+%%   \begin{align*}
+%%     \theta_{\predom}P &= (\later[(X,\ltdynp X) \leftarrow P] X, )
+%%   \end{align*}
+%% \end{definition}
 
 
 \end{document}