From e0a9bc191aef922dbc019ff08c4a3125ce3ac749 Mon Sep 17 00:00:00 2001
From: Alan Jeffrey <403333+asajeffrey@users.noreply.github.com>
Date: Fri, 11 Feb 2022 19:03:26 -0600
Subject: [PATCH] Prototype: added syntax for optional type annotations (#358)

---
 prototyping/Examples/OpSem.agda             |  8 +--
 prototyping/Examples/Run.agda               |  9 +--
 prototyping/Examples/Syntax.agda            | 18 +++---
 prototyping/Interpreter.agda                |  2 +-
 prototyping/Luau/Heap.agda                  | 31 ++++++-----
 prototyping/Luau/OpSem.agda                 | 32 +++++------
 prototyping/Luau/Run.agda                   | 10 ++--
 prototyping/Luau/RuntimeError.agda          | 10 ++--
 prototyping/Luau/RuntimeError/ToString.agda |  7 ++-
 prototyping/Luau/Substitution.agda          | 16 +++---
 prototyping/Luau/Syntax.agda                | 62 +++++++++++++++------
 prototyping/Luau/Syntax/FromJSON.agda       | 20 +++----
 prototyping/Luau/Syntax/ToString.agda       | 37 +++++++-----
 prototyping/Luau/Value.agda                 |  4 +-
 prototyping/PrettyPrinter.agda              |  2 +-
 prototyping/Properties/Step.agda            | 26 ++++-----
 16 files changed, 165 insertions(+), 129 deletions(-)

diff --git a/prototyping/Examples/OpSem.agda b/prototyping/Examples/OpSem.agda
index 4043869..ec8bce7 100644
--- a/prototyping/Examples/OpSem.agda
+++ b/prototyping/Examples/OpSem.agda
@@ -1,11 +1,9 @@
 module Examples.OpSem where
 
 open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; subst)
-open import Luau.Syntax using (var; nil; local_←_; _∙_; done; return)
-open import Luau.Heap using (emp)
+open import Luau.Syntax using (Block; var; nil; local_←_; _∙_; done; return; block_is_end)
+open import Luau.Heap using (∅)
 
-x = var "x"
-
-ex1 : emp ⊢ (local "x" ← nil ∙ return x ∙ done) ⟶ᴮ (return nil ∙ done) ⊣ emp
+ex1 : ∅ ⊢ (local (var "x") ← nil ∙ return (var "x") ∙ done) ⟶ᴮ (return nil ∙ done) ⊣ ∅
 ex1 = subst
 
diff --git a/prototyping/Examples/Run.agda b/prototyping/Examples/Run.agda
index bfa7983..88ca39b 100644
--- a/prototyping/Examples/Run.agda
+++ b/prototyping/Examples/Run.agda
@@ -3,16 +3,13 @@
 module Examples.Run where
 
 open import Agda.Builtin.Equality using (_≡_; refl)
-open import Luau.Syntax using (nil; var; _$_; function_⟨_⟩_end; return; _∙_; done)
+open import Luau.Syntax using (nil; var; _$_; function_is_end; return; _∙_; done; _⟨_⟩)
 open import Luau.Value using (nil)
 open import Luau.Run using (run; return)
-open import Luau.Heap using (emp; lookup-next; next-emp; lookup-next-emp)
+open import Luau.Heap using (lookup-next; next-emp; lookup-next-emp)
 
 import Agda.Builtin.Equality.Rewrite
 {-# REWRITE lookup-next next-emp lookup-next-emp #-}
 
-x = var "x"
-id = var "id"
-
-ex1 : (run (function "id" ⟨ "x" ⟩ return x ∙ done end ∙ return (id $ nil) ∙ done) ≡ return nil _)
+ex1 : (run (function "id" ⟨ var "x" ⟩ is return (var "x") ∙ done end ∙ return (var "id" $ nil) ∙ done) ≡ return nil _)
 ex1 = refl
diff --git a/prototyping/Examples/Syntax.agda b/prototyping/Examples/Syntax.agda
index 8af9bca..4ffcf4c 100644
--- a/prototyping/Examples/Syntax.agda
+++ b/prototyping/Examples/Syntax.agda
@@ -2,21 +2,21 @@ module Examples.Syntax where
 
 open import Agda.Builtin.Equality using (_≡_; refl)
 open import FFI.Data.String using (_++_)
-open import Luau.Syntax using (var; _$_; return; nil; function_⟨_⟩_end; done; _∙_)
+open import Luau.Syntax using (var; _$_; return; nil; function_is_end; local_←_; done; _∙_; _⟨_⟩)
 open import Luau.Syntax.ToString using (exprToString; blockToString)
 
-f = var "f"
-x = var "x"
-
-ex1 : exprToString(f $ x) ≡
-  "f(x)"
+ex1 : exprToString(function "" ⟨ var "x" ⟩ is return (var "f" $ var "x") ∙ done end) ≡
+  "function(x)\n" ++
+  "  return f(x)\n" ++
+  "end"
 ex1 = refl
 
-ex2 : blockToString(return nil ∙ done) ≡
-  "return nil"
+ex2 : blockToString(local var "x" ← nil ∙ return (var "x") ∙ done) ≡
+  "local x = nil\n" ++
+  "return x"
 ex2 = refl
 
-ex3 : blockToString(function "f" ⟨ "x" ⟩ return x ∙ done end ∙ return f ∙ done) ≡
+ex3 : blockToString(function "f" ⟨ var "x" ⟩ is return (var "x") ∙ done end ∙ return (var "f") ∙ done) ≡
   "local function f(x)\n" ++
   "  return x\n" ++
   "end\n" ++
diff --git a/prototyping/Interpreter.agda b/prototyping/Interpreter.agda
index 9184235..3ec5b8d 100644
--- a/prototyping/Interpreter.agda
+++ b/prototyping/Interpreter.agda
@@ -18,7 +18,7 @@ open import Luau.Run using (run; return; done; error)
 open import Luau.RuntimeError.ToString using (errToStringᴮ)
 open import Luau.Value.ToString using (valueToString)
 
-runBlock : Block → IO ⊤
+runBlock : ∀ {a} → Block a → IO ⊤
 runBlock block with run block
 runBlock block | return V D = putStrLn (valueToString V)
 runBlock block | done D = putStrLn "nil"
diff --git a/prototyping/Luau/Heap.agda b/prototyping/Luau/Heap.agda
index 1a0416e..12f8dab 100644
--- a/prototyping/Luau/Heap.agda
+++ b/prototyping/Luau/Heap.agda
@@ -5,39 +5,40 @@ open import FFI.Data.Maybe using (Maybe; just)
 open import FFI.Data.Vector using (Vector; length; snoc; empty)
 open import Luau.Addr using (Addr)
 open import Luau.Var using (Var)
-open import Luau.Syntax using (Block; Expr; nil; addr; function⟨_⟩_end)
+open import Luau.Syntax using (Block; Expr; Annotated; FunDec; nil; addr; function_is_end)
 
-data HeapValue : Set where
-  function_⟨_⟩_end : Var → Var → Block → HeapValue
+data HeapValue (a : Annotated) : Set where
+  function_is_end : FunDec a → Block a → HeapValue a
 
-Heap = Vector HeapValue
+Heap : Annotated → Set
+Heap a = Vector (HeapValue a)
 
-data _≡_⊕_↦_ : Heap → Heap → Addr → HeapValue → Set where
+data _≡_⊕_↦_ {a} : Heap a → Heap a → Addr → HeapValue a → Set where
 
   defn : ∀ {H val} →
 
     -----------------------------------
     (snoc H val) ≡ H ⊕ (length H) ↦ val
 
-lookup : Heap → Addr → Maybe HeapValue
-lookup = FFI.Data.Vector.lookup
+_[_] : ∀ {a} → Heap a → Addr → Maybe (HeapValue a)
+_[_] = FFI.Data.Vector.lookup
 
-emp : Heap
-emp = empty
+∅ : ∀ {a} → Heap a
+∅ = empty
 
-data AllocResult (H : Heap) (V : HeapValue) : Set where
-  ok : ∀ a H′ → (H′ ≡ H ⊕ a ↦ V) → AllocResult H V
+data AllocResult a (H : Heap a) (V : HeapValue a) : Set where
+  ok : ∀ b H′ → (H′ ≡ H ⊕ b ↦ V) → AllocResult a H V
 
-alloc : ∀ H V → AllocResult H V
+alloc : ∀ {a} H V → AllocResult a H V
 alloc H V = ok (length H) (snoc H V) defn
 
-next : Heap → Addr
+next : ∀ {a} → Heap a → Addr
 next = length
 
-allocated : Heap → HeapValue → Heap
+allocated : ∀ {a} → Heap a → HeapValue a → Heap a
 allocated = snoc
 
--- next-emp : (length empty ≡ 0)
+-- next-emp : (length ∅ ≡ 0)
 next-emp = FFI.Data.Vector.length-empty
 
 -- lookup-next : ∀ V H → (lookup (allocated H V) (next H) ≡ just V)
diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda
index dcd474b..878b8bd 100644
--- a/prototyping/Luau/OpSem.agda
+++ b/prototyping/Luau/OpSem.agda
@@ -2,13 +2,13 @@ module Luau.OpSem where
 
 open import Agda.Builtin.Equality using (_≡_)
 open import FFI.Data.Maybe using (just)
-open import Luau.Heap using (Heap; _≡_⊕_↦_; lookup; function_⟨_⟩_end)
+open import Luau.Heap using (Heap; _≡_⊕_↦_; _[_]; function_is_end)
 open import Luau.Substitution using (_[_/_]ᴮ)
-open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function⟨_⟩_end; _$_; block_is_end; local_←_; _∙_; done; function_⟨_⟩_end; return)
+open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; fun; arg)
 open import Luau.Value using (addr; val)
 
-data _⊢_⟶ᴮ_⊣_ : Heap → Block → Block → Heap → Set
-data _⊢_⟶ᴱ_⊣_ : Heap → Expr → Expr → Heap → Set
+data _⊢_⟶ᴮ_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set
+data _⊢_⟶ᴱ_⊣_ {a} : Heap a → Expr a → Expr a → Heap a → Set
 
 data _⊢_⟶ᴱ_⊣_  where
 
@@ -17,11 +17,11 @@ data _⊢_⟶ᴱ_⊣_  where
     -------------------
     H ⊢ nil ⟶ᴱ nil ⊣ H
 
-  function : ∀ {H H′ a x B} →
+  function : ∀ {H H′ a F B} →
 
-    H′ ≡ H ⊕ a ↦ (function "anon" ⟨ x ⟩ B end) →
+    H′ ≡ H ⊕ a ↦ (function F is B end) →
     -------------------------------------------
-    H ⊢ (function⟨ x ⟩ B end) ⟶ᴱ (addr a) ⊣ H′
+    H ⊢ (function F is B end) ⟶ᴱ (addr a) ⊣ H′
 
   app : ∀ {H H′ M M′ N} →
   
@@ -29,11 +29,11 @@ data _⊢_⟶ᴱ_⊣_  where
     -----------------------------
     H ⊢ (M $ N) ⟶ᴱ (M′ $ N) ⊣ H′
 
-  beta : ∀ {H M a f x B} →
+  beta : ∀ {H M a F B} →
   
-    (lookup H a) ≡ just(function f ⟨ x ⟩ B end) →
+    H [ a ] ≡ just(function F is B end) →
     -----------------------------------------------------
-    H ⊢ (addr a $ M) ⟶ᴱ (block f is local x ← M ∙ B end) ⊣ H
+    H ⊢ (addr a $ M) ⟶ᴱ (block (fun F) is local (arg F) ← M ∙ B end) ⊣ H
 
   block : ∀ {H H′ B B′ b} →
  
@@ -61,14 +61,14 @@ data _⊢_⟶ᴮ_⊣_  where
 
   subst : ∀ {H x v B} →
   
-    -------------------------------------------------
-    H ⊢ (local x ← val v ∙ B) ⟶ᴮ (B [ v / x ]ᴮ) ⊣ H
+    ------------------------------------------------------
+    H ⊢ (local x ← val v ∙ B) ⟶ᴮ (B [ v / name x ]ᴮ) ⊣ H
 
-  function : ∀ {H H′ a f x B C} →
+  function : ∀ {H H′ a F B C} →
   
-    H′ ≡ H ⊕ a ↦ (function f ⟨ x ⟩ C end) →
+    H′ ≡ H ⊕ a ↦ (function F is C end) →
     --------------------------------------------------------------
-    H ⊢ (function f ⟨ x ⟩ C end ∙ B) ⟶ᴮ (B [ addr a / f ]ᴮ) ⊣ H′
+    H ⊢ (function F is C end ∙ B) ⟶ᴮ (B [ addr a / fun F ]ᴮ) ⊣ H′
 
   return : ∀ {H H′ M M′ B} →
   
@@ -76,7 +76,7 @@ data _⊢_⟶ᴮ_⊣_  where
     --------------------------------------------
     H ⊢ (return M ∙ B) ⟶ᴮ (return M′ ∙ B) ⊣ H′
 
-data _⊢_⟶*_⊣_ : Heap → Block → Block → Heap → Set where
+data _⊢_⟶*_⊣_ {a} : Heap a → Block a → Block a → Heap a → Set where
 
   refl : ∀ {H B} →
 
diff --git a/prototyping/Luau/Run.agda b/prototyping/Luau/Run.agda
index 29709ce..d84f75d 100644
--- a/prototyping/Luau/Run.agda
+++ b/prototyping/Luau/Run.agda
@@ -1,20 +1,20 @@
 module Luau.Run where
 
 open import Agda.Builtin.Equality using (_≡_; refl)
-open import Luau.Heap using (Heap; emp)
+open import Luau.Heap using (Heap; ∅)
 open import Luau.Syntax using (Block; return; _∙_; done)
 open import Luau.OpSem using (_⊢_⟶*_⊣_; refl; step)
 open import Luau.Value using (val)
 open import Properties.Step using (stepᴮ; step; return; done; error)
 open import Luau.RuntimeError using (RuntimeErrorᴮ)
 
-data RunResult (H : Heap) (B : Block) : Set where
+data RunResult {a} (H : Heap a) (B : Block a) : Set where
   return : ∀ V {B′ H′} → (H ⊢ B ⟶* (return (val V) ∙ B′) ⊣ H′) → RunResult H B
   done : ∀ {H′} → (H ⊢ B ⟶* done ⊣ H′) → RunResult H B
   error : ∀ {B′ H′} → (RuntimeErrorᴮ H′ B′) → (H ⊢ B ⟶* B′ ⊣ H′) → RunResult H B
 
 {-# TERMINATING #-}
-run′ : ∀ H B → RunResult H B
+run′ : ∀ {a} H B → RunResult {a} H B
 run′ H B with stepᴮ H B
 run′ H B | step H′ B′ D with run′ H′ B′
 run′ H B | step H′ B′ D | return V D′  = return V (step D D′)
@@ -24,5 +24,5 @@ run′ H _ | return V refl = return V refl
 run′ H _ | done refl = done refl
 run′ H B | error E = error E refl
 
-run : ∀ B → RunResult emp B
-run = run′ emp
+run : ∀ {a} B → RunResult {a} ∅ B
+run = run′ ∅
diff --git a/prototyping/Luau/RuntimeError.agda b/prototyping/Luau/RuntimeError.agda
index 86e7cf2..e514dc9 100644
--- a/prototyping/Luau/RuntimeError.agda
+++ b/prototyping/Luau/RuntimeError.agda
@@ -1,17 +1,17 @@
 module Luau.RuntimeError where
 
 open import Agda.Builtin.Equality using (_≡_)
-open import Luau.Heap using (Heap; lookup)
+open import Luau.Heap using (Heap; _[_])
 open import FFI.Data.Maybe using (just; nothing)
-open import Luau.Syntax using (Block; Expr; nil; var; addr; function⟨_⟩_end; block_is_end; _$_; local_←_; function_⟨_⟩_end; return; done; _∙_)
+open import Luau.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_)
 
-data RuntimeErrorᴮ (H : Heap) : Block → Set
-data RuntimeErrorᴱ (H : Heap) : Expr → Set
+data RuntimeErrorᴮ {a} (H : Heap a) : Block a → Set
+data RuntimeErrorᴱ {a} (H : Heap a) : Expr a → Set
 
 data RuntimeErrorᴱ H where
   NilIsNotAFunction : ∀ {M} → RuntimeErrorᴱ H (nil $ M)
   UnboundVariable : ∀ x → RuntimeErrorᴱ H (var x)
-  SEGV : ∀ a → (lookup H a ≡ nothing) → RuntimeErrorᴱ H (addr a)
+  SEGV : ∀ a → (H [ a ] ≡ nothing) → RuntimeErrorᴱ H (addr a)
   app : ∀ {M N} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (M $ N)
   block : ∀ b {B} → RuntimeErrorᴮ H B → RuntimeErrorᴱ H (block b is B end)
 
diff --git a/prototyping/Luau/RuntimeError/ToString.agda b/prototyping/Luau/RuntimeError/ToString.agda
index f11756f..e828715 100644
--- a/prototyping/Luau/RuntimeError/ToString.agda
+++ b/prototyping/Luau/RuntimeError/ToString.agda
@@ -4,9 +4,10 @@ open import FFI.Data.String using (String; _++_)
 open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; NilIsNotAFunction; UnboundVariable; SEGV; app; block)
 open import Luau.Addr.ToString using (addrToString)
 open import Luau.Var.ToString using (varToString)
+open import Luau.Syntax using (name)
 
-errToStringᴱ : ∀ {H B} → RuntimeErrorᴱ H B → String
-errToStringᴮ : ∀ {H B} → RuntimeErrorᴮ H B → String
+errToStringᴱ : ∀ {a H B} → RuntimeErrorᴱ {a} H B → String
+errToStringᴮ : ∀ {a H B} → RuntimeErrorᴮ {a} H B → String
 
 errToStringᴱ NilIsNotAFunction = "nil is not a function"
 errToStringᴱ (UnboundVariable x) = "variable " ++ varToString x ++ " is unbound"
@@ -14,5 +15,5 @@ errToStringᴱ (SEGV a x) = "address " ++ addrToString a ++ " is unallocated"
 errToStringᴱ (app E) = errToStringᴱ E
 errToStringᴱ (block b E) = errToStringᴮ E ++ "\n  in call of function " ++ varToString b
 
-errToStringᴮ (local x E) = errToStringᴱ E ++ "\n  in definition of " ++ varToString x 
+errToStringᴮ (local x E) = errToStringᴱ E ++ "\n  in definition of " ++ varToString (name x) 
 errToStringᴮ (return E) = errToStringᴱ E ++ "\n  in return statement"
diff --git a/prototyping/Luau/Substitution.agda b/prototyping/Luau/Substitution.agda
index 1a36117..b956aea 100644
--- a/prototyping/Luau/Substitution.agda
+++ b/prototyping/Luau/Substitution.agda
@@ -1,24 +1,24 @@
 module Luau.Substitution where
 
-open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function⟨_⟩_end; _$_; block_is_end; local_←_; _∙_; done; function_⟨_⟩_end; return)
+open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; _⟨_⟩ ; name; fun; arg)
 open import Luau.Value using (Value; val)
 open import Luau.Var using (Var; _≡ⱽ_)
 open import Properties.Dec using (Dec; yes; no)
 
-_[_/_]ᴱ : Expr → Value → Var → Expr
-_[_/_]ᴮ : Block → Value → Var → Block
-var_[_/_]ᴱwhenever_ : ∀ {P} → Var → Value → Var → (Dec P) → Expr
-_[_/_]ᴮunless_ : ∀ {P} → Block → Value → Var → (Dec P) → Block
+_[_/_]ᴱ : ∀ {a} → Expr a → Value → Var → Expr a
+_[_/_]ᴮ : ∀ {a} → Block a → Value → Var → Block a
+var_[_/_]ᴱwhenever_ : ∀ {a P} → Var → Value → Var → (Dec P) → Expr a
+_[_/_]ᴮunless_ : ∀ {a P} → Block a → Value → Var → (Dec P) → Block a
 
 nil [ v / x ]ᴱ = nil
 var y [ v / x ]ᴱ = var y [ v / x ]ᴱwhenever (x ≡ⱽ y)
 addr a [ v / x ]ᴱ = addr a
 (M $ N) [ v / x ]ᴱ = (M [ v / x ]ᴱ) $ (N [ v / x ]ᴱ)
-function⟨ y ⟩ C end [ v / x ]ᴱ = function⟨ y ⟩ C [ v / x ]ᴮunless (x ≡ⱽ y) end
+function F is C end [ v / x ]ᴱ = function F is C [ v / x ]ᴮunless (x ≡ⱽ name(arg F)) end
 block b is C end [ v / x ]ᴱ = block b is C [ v / x ]ᴮ end
 
-(function f ⟨ y ⟩ C end ∙ B) [ v / x ]ᴮ = function f ⟨ y ⟩ (C [ v / x ]ᴮunless (x ≡ⱽ y)) end ∙ (B [ v / x ]ᴮunless (x ≡ⱽ f))
-(local y ← M ∙ B) [ v / x ]ᴮ = local y ← (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮunless (x ≡ⱽ y))
+(function F is C end ∙ B) [ v / x ]ᴮ = function F is (C [ v / x ]ᴮunless (x ≡ⱽ name(arg F))) end ∙ (B [ v / x ]ᴮunless (x ≡ⱽ fun F))
+(local y ← M ∙ B) [ v / x ]ᴮ = local y ← (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮunless (x ≡ⱽ name y))
 (return M ∙ B) [ v / x ]ᴮ = return (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮ)
 done [ v / x ]ᴮ = done
 
diff --git a/prototyping/Luau/Syntax.agda b/prototyping/Luau/Syntax.agda
index 3fe05bc..04970b6 100644
--- a/prototyping/Luau/Syntax.agda
+++ b/prototyping/Luau/Syntax.agda
@@ -1,27 +1,55 @@
 module Luau.Syntax where
 
+open import Agda.Builtin.Equality using (_≡_)
+open import Properties.Dec using (⊥)
 open import Luau.Var using (Var)
 open import Luau.Addr using (Addr)
+open import Luau.Type using (Type)
 
 infixr 5 _∙_
 
-data Block : Set
-data Stat : Set
-data Expr : Set
+data Annotated : Set where
+  maybe : Annotated
+  yes : Annotated
 
-data Block where
-  _∙_ : Stat → Block → Block
-  done : Block
+data VarDec : Annotated → Set where
+  var : Var → VarDec maybe
+  var_∈_ : ∀ {a} → Var → Type → VarDec a
 
-data Stat where
-  function_⟨_⟩_end : Var → Var → Block → Stat
-  local_←_ : Var → Expr → Stat
-  return : Expr → Stat
+name : ∀ {a} → VarDec a → Var
+name (var x) = x
+name (var x ∈ T) = x
+
+data FunDec : Annotated → Set where
+  _⟨_⟩∈_ : ∀ {a} → Var → VarDec a → Type → FunDec a
+  _⟨_⟩ : Var → VarDec maybe → FunDec maybe
+
+fun : ∀ {a} → FunDec a → Var
+fun (f ⟨ x ⟩∈ T) = f
+fun (f ⟨ x ⟩) = f
+
+arg : ∀ {a} → FunDec a → VarDec a
+arg (f ⟨ x ⟩∈ T) = x
+arg (f ⟨ x ⟩) = x
+
+data Block (a : Annotated) : Set
+data Stat (a : Annotated) : Set
+data Expr (a : Annotated) : Set
+
+data Block a where
+  _∙_ : Stat a → Block a → Block a
+  done : Block a
+
+data Stat a where
+  function_is_end : FunDec a → Block a → Stat a
+  local_←_ : VarDec a → Expr a → Stat a
+  return : Expr a → Stat a
+
+data Expr a where
+  nil : Expr a
+  var : Var → Expr a
+  addr : Addr → Expr a
+  _$_ : Expr a → Expr a → Expr a
+  function_is_end : FunDec a → Block a → Expr a
+  block_is_end : Var → Block a → Expr a
 
-data Expr where
-  nil : Expr
-  var : Var → Expr
-  addr : Addr → Expr
-  _$_ : Expr → Expr → Expr
-  function⟨_⟩_end : Var → Block → Expr
-  block_is_end : Var → Block → Expr
diff --git a/prototyping/Luau/Syntax/FromJSON.agda b/prototyping/Luau/Syntax/FromJSON.agda
index 0a4164f..b081d15 100644
--- a/prototyping/Luau/Syntax/FromJSON.agda
+++ b/prototyping/Luau/Syntax/FromJSON.agda
@@ -1,6 +1,6 @@
 module Luau.Syntax.FromJSON where
 
-open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; function⟨_⟩_end; local_←_; function_⟨_⟩_end; return; done; _∙_)
+open import Luau.Syntax using (Block; Stat ; Expr; nil; _$_; var; function_is_end; _⟨_⟩; local_←_; return; done; _∙_; maybe)
 
 open import Agda.Builtin.List using (List; _∷_; [])
 
@@ -31,12 +31,12 @@ lookupIn (key ∷ keys) obj with lookup (fromString key) obj
 lookupIn (key ∷ keys) obj | nothing = lookupIn keys obj
 lookupIn (key ∷ keys) obj | just value = (key , value)
 
-exprFromJSON : Value → Either String Expr
-exprFromObject : Object → Either String Expr
-statFromJSON : Value → Either String Stat
-statFromObject : Object → Either String Stat
-blockFromJSON : Value → Either String Block
-blockFromArray : Array → Either String Block
+exprFromJSON : Value → Either String (Expr maybe)
+exprFromObject : Object → Either String (Expr maybe)
+statFromJSON : Value → Either String (Stat maybe)
+statFromObject : Object → Either String (Stat maybe)
+blockFromJSON : Value → Either String (Block maybe)
+blockFromArray : Array → Either String (Block maybe)
 
 exprFromJSON (object obj) = exprFromObject obj
 exprFromJSON val = Left "AstExpr not an object"
@@ -55,7 +55,7 @@ exprFromObject obj | just (string "AstExprCall") | _ | nothing  = Left ("AstExpr
 exprFromObject obj | just (string "AstExprConstantNil") = Right nil
 exprFromObject obj | just (string "AstExprFunction") with lookup args obj | lookup body obj
 exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value with head arr | blockFromJSON value
-exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value | just (string x) | Right B = Right (function⟨ x ⟩ B end)
+exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value | just (string x) | Right B = Right (function "" ⟨ var x ⟩ is B end)
 exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value | just _ | Right B = Left "AstExprFunction args not a string array"
 exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value | nothing | Right B = Left "Unsupported AstExprFunction empty args"
 exprFromObject obj | just (string "AstExprFunction") | just (array arr) | just value | _ | Left err = Left err
@@ -78,7 +78,7 @@ statFromObject obj with lookup type obj
 statFromObject obj | just(string "AstStatLocal") with lookup vars obj | lookup values obj
 statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) with head(arr1) | head(arr2)
 statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(string x) | just(value) with exprFromJSON(value)
-statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(string x) | just(value) | Right M = Right (local x ← M)
+statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(string x) | just(value) | Right M = Right (local (var x) ← M)
 statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(string x) | just(value) | Left err = Left err
 statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(string x) | nothing = Left "AstStatLocal empty values"
 statFromObject obj | just(string "AstStatLocal") | just(array arr1) | just(array arr2) | just(_) | _ = Left "AstStatLocal vars not a string array"
@@ -89,7 +89,7 @@ statFromObject obj | just(string "AstStatLocal") | just(_) | nothing = Left "Ast
 statFromObject obj | just(string "AstStatLocal") | nothing | _ = Left "AstStatLocal missing vars"
 statFromObject obj | just(string "AstStatLocalFunction") with lookup name obj | lookup func obj
 statFromObject obj | just(string "AstStatLocalFunction") | just (string f) | just value with exprFromJSON value
-statFromObject obj | just(string "AstStatLocalFunction") | just (string f) | just value | Right (function⟨ x ⟩ B end) = Right (function f ⟨ x ⟩ B end)
+statFromObject obj | just(string "AstStatLocalFunction") | just (string f) | just value | Right (function "" ⟨ x ⟩ is B end) = Right (function f ⟨ x ⟩ is B end)
 statFromObject obj | just(string "AstStatLocalFunction") | just (string f) | just value | Left err = Left err
 statFromObject obj | just(string "AstStatLocalFunction") | just _ | just _ | Right _ = Left "AstStatLocalFunction func is not an AstExprFunction"
 statFromObject obj | just(string "AstStatLocalFunction") | just _ | just _ =  Left "AstStatLocalFunction name is not a string"
diff --git a/prototyping/Luau/Syntax/ToString.agda b/prototyping/Luau/Syntax/ToString.agda
index afec093..18d3617 100644
--- a/prototyping/Luau/Syntax/ToString.agda
+++ b/prototyping/Luau/Syntax/ToString.agda
@@ -1,13 +1,24 @@
 module Luau.Syntax.ToString where
 
-open import Luau.Syntax using (Block; Stat; Expr; nil; var; addr; _$_; function⟨_⟩_end; return; function_⟨_⟩_end ;local_←_; _∙_; done; block_is_end)
+open import Luau.Syntax using (Block; Stat; Expr; VarDec; FunDec; nil; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_)
 open import FFI.Data.String using (String; _++_)
 open import Luau.Addr.ToString using (addrToString)
+open import Luau.Type.ToString using (typeToString)
 open import Luau.Var.ToString using (varToString)
 
-exprToString′ : String → Expr → String
-statToString′ : String → Stat → String
-blockToString′ : String → Block → String
+varDecToString : ∀ {a} → VarDec a → String
+varDecToString (var x) = varToString x
+varDecToString (var x ∈ T) =  varToString x ++ " : " ++ typeToString T
+
+funDecToString : ∀ {a} → FunDec a → String
+funDecToString ("" ⟨ x ⟩∈ T) = "function(" ++ varDecToString x ++ "): " ++ typeToString T
+funDecToString ("" ⟨ x ⟩) = "function(" ++ varDecToString x ++ ")"
+funDecToString (f ⟨ x ⟩∈ T) = "function " ++ varToString f ++ "(" ++ varDecToString x ++ "): " ++ typeToString T
+funDecToString (f ⟨ x ⟩) = "function " ++ varToString f ++ "(" ++ varDecToString x ++ ")"
+
+exprToString′ : ∀ {a} → String → Expr a → String
+statToString′ : ∀ {a} → String → Stat a → String
+blockToString′ : ∀ {a} → String → Block a → String
 
 exprToString′ lb nil =
   "nil"
@@ -17,21 +28,21 @@ exprToString′ lb (var x) =
   varToString(x)
 exprToString′ lb (M $ N) =
   (exprToString′ lb M) ++ "(" ++ (exprToString′ lb N) ++ ")"
-exprToString′ lb (function⟨ x ⟩ B end) =
-  "function(" ++ x ++ ")" ++ lb ++
+exprToString′ lb (function F is B end) =
+  funDecToString F ++ lb ++
   "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
   "end"
 exprToString′ lb (block b is B end) =
-  "(function " ++ b ++ "()" ++ lb ++
+  "(" ++ b ++ "()" ++ lb ++
   "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
   "end)()"
 
-statToString′ lb (function f ⟨ x ⟩ B end) =
-  "local function " ++ f ++ "(" ++ x ++ ")" ++ lb ++
+statToString′ lb (function F is B end) =
+  "local " ++ funDecToString F ++ lb ++
   "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
   "end"
 statToString′ lb (local x ← M) =
-  "local " ++ x ++ " = " ++ (exprToString′ lb M)
+  "local " ++ varDecToString x ++ " = " ++ (exprToString′ lb M)
 statToString′ lb (return M) =
   "return " ++ (exprToString′ lb M)
 
@@ -39,11 +50,11 @@ blockToString′ lb (S ∙ done) = statToString′ lb S
 blockToString′ lb (S ∙ B) = statToString′ lb S ++ lb ++ blockToString′ lb B
 blockToString′ lb (done) = ""
 
-exprToString : Expr → String
+exprToString : ∀ {a} → Expr a → String
 exprToString = exprToString′ "\n"
 
-statToString : Stat → String
+statToString : ∀ {a} → Stat a → String
 statToString = statToString′ "\n"
 
-blockToString : Block → String
+blockToString : ∀ {a} → Block a → String
 blockToString = blockToString′ "\n"
diff --git a/prototyping/Luau/Value.agda b/prototyping/Luau/Value.agda
index 855e663..4768f85 100644
--- a/prototyping/Luau/Value.agda
+++ b/prototyping/Luau/Value.agda
@@ -1,14 +1,14 @@
 module Luau.Value where
 
 open import Luau.Addr using (Addr)
-open import Luau.Syntax using (Block; Expr; nil; addr; function⟨_⟩_end)
+open import Luau.Syntax using (Block; Expr; nil; addr)
 open import Luau.Var using (Var)
 
 data Value : Set where
   nil : Value
   addr : Addr → Value
 
-val : Value → Expr
+val : ∀ {a} → Value → Expr a
 val nil = nil
 val (addr a) = addr a
 
diff --git a/prototyping/PrettyPrinter.agda b/prototyping/PrettyPrinter.agda
index dfb2c05..4a6c7dd 100644
--- a/prototyping/PrettyPrinter.agda
+++ b/prototyping/PrettyPrinter.agda
@@ -15,7 +15,7 @@ open import Luau.Syntax using (Block)
 open import Luau.Syntax.FromJSON using (blockFromJSON)
 open import Luau.Syntax.ToString using (blockToString)
 
-runBlock : Block → IO ⊤
+runBlock : ∀ {a} → Block a → IO ⊤
 runBlock block = putStrLn (blockToString block)
 
 runJSON : Value → IO ⊤
diff --git a/prototyping/Properties/Step.agda b/prototyping/Properties/Step.agda
index 0eddd9f..eeda4ef 100644
--- a/prototyping/Properties/Step.agda
+++ b/prototyping/Properties/Step.agda
@@ -2,16 +2,16 @@ module Properties.Step where
 
 open import Agda.Builtin.Equality using (_≡_; refl)
 open import FFI.Data.Maybe using (just; nothing)
-open import Luau.Heap using (Heap; lookup; alloc; ok; function_⟨_⟩_end)
-open import Luau.Syntax using (Block; Expr; nil; var; addr; function⟨_⟩_end; block_is_end; _$_; local_←_; function_⟨_⟩_end; return; done; _∙_)
+open import Luau.Heap using (Heap; _[_]; alloc; ok; function_is_end)
+open import Luau.Syntax using (Block; Expr; nil; var; addr; function_is_end; block_is_end; _$_; local_←_; return; done; _∙_; name; fun; arg)
 open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; app ; beta; function; block; return; done; local; subst)
 open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotAFunction; UnboundVariable; SEGV; app; block; local; return)
 open import Luau.Substitution using (_[_/_]ᴮ)
 open import Luau.Value using (nil; addr; val)
 open import Properties.Remember using (remember; _,_)
 
-data StepResultᴮ (H : Heap) (B : Block) : Set
-data StepResultᴱ (H : Heap) (M : Expr) : Set
+data StepResultᴮ {a} (H : Heap a) (B : Block a) : Set
+data StepResultᴱ {a} (H : Heap a) (M : Expr a) : Set
 
 data StepResultᴮ H B where
   step : ∀ H′ B′ → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → StepResultᴮ H B
@@ -24,8 +24,8 @@ data StepResultᴱ H M where
   value : ∀ V → (M ≡ val V) → StepResultᴱ H M
   error : (RuntimeErrorᴱ H M) → StepResultᴱ H M
 
-stepᴱ : ∀ H M → StepResultᴱ H M
-stepᴮ : ∀ H B → StepResultᴮ H B
+stepᴱ : ∀ {a} H M → StepResultᴱ {a} H M
+stepᴮ : ∀ {a} H B → StepResultᴮ {a} H B
 
 stepᴱ H nil = value nil refl
 stepᴱ H (var x) = error (UnboundVariable x)
@@ -33,23 +33,23 @@ stepᴱ H (addr a) = value (addr a) refl
 stepᴱ H (M $ N) with stepᴱ H M
 stepᴱ H (M $ N) | step H′ M′ D = step H′ (M′ $ N) (app D)
 stepᴱ H (nil $ N) | value nil refl = error NilIsNotAFunction
-stepᴱ H (addr a $ N) | value (addr a) refl with remember (lookup H a)
+stepᴱ H (addr a $ N) | value (addr a) refl with remember (H [ a ])
 stepᴱ H (addr a $ N) | value (addr a) refl | (nothing , p) = error (app (SEGV a p))
-stepᴱ H (addr a $ N) | value (addr a) refl | (just(function f ⟨ x ⟩ B end) , p) = step H (block f is local x ← N ∙ B end) (beta p)
+stepᴱ H (addr a $ N) | value (addr a) refl | (just(function F is B end) , p) = step H (block fun F is (local arg F ← N) ∙ B end) (beta p)
 stepᴱ H (M $ N) | error E = error (app E)
-stepᴱ H (function⟨ x ⟩ B end) with alloc H (function "anon" ⟨ x ⟩ B end)
-stepᴱ H (function⟨ x ⟩ B end) | ok a H′ p = step H′ (addr a) (function p)
 stepᴱ H (block b is B end) with stepᴮ H B
 stepᴱ H (block b is B end) | step H′ B′ D = step H′ (block b is B′ end) (block D)
 stepᴱ H (block b is (return _ ∙ B′) end) | return V refl = step H (val V) return
 stepᴱ H (block b is done end) | done refl = step H nil done
 stepᴱ H (block b is B end) | error E = error (block b E)
+stepᴱ H (function F is C end) with alloc H (function F is C end)
+stepᴱ H function F is C end | ok a H′ p = step H′ (addr a) (function p)
 
-stepᴮ H (function f ⟨ x ⟩ C end ∙ B) with alloc H (function f ⟨ x ⟩ C end)
-stepᴮ H (function f ⟨ x ⟩ C end ∙ B) | ok a H′ p = step H′ (B [ addr a / f ]ᴮ) (function p)
+stepᴮ H (function F is C end ∙ B) with alloc H (function F is C end)
+stepᴮ H (function F is C end ∙ B) | ok a H′ p = step H′ (B [ addr a / fun F ]ᴮ) (function p)
 stepᴮ H (local x ← M ∙ B) with stepᴱ H M
 stepᴮ H (local x ← M ∙ B) | step H′ M′ D = step H′ (local x ← M′ ∙ B) (local D)
-stepᴮ H (local x ← _ ∙ B) | value V refl = step H (B [ V / x ]ᴮ) subst
+stepᴮ H (local x ← _ ∙ B) | value V refl = step H (B [ V / name x ]ᴮ) subst
 stepᴮ H (local x ← M ∙ B) | error E = error (local x E)
 stepᴮ H (return M ∙ B) with stepᴱ H M
 stepᴮ H (return M ∙ B) | step H′ M′ D = step H′ (return M′ ∙ B) (return D)