diff --git a/prototyping/Examples.agda b/prototyping/Examples.agda
index fe396eff..212067b7 100644
--- a/prototyping/Examples.agda
+++ b/prototyping/Examples.agda
@@ -4,4 +4,4 @@ module Examples where
 import Examples.Syntax
 import Examples.OpSem
 import Examples.Run
-
+import Examples.Type
diff --git a/prototyping/Examples/Type.agda b/prototyping/Examples/Type.agda
new file mode 100644
index 00000000..5d35e8c1
--- /dev/null
+++ b/prototyping/Examples/Type.agda
@@ -0,0 +1,21 @@
+module Examples.Type where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import FFI.Data.String using (_++_)
+open import Luau.Type using (nil; _∪_; _∩_; _⇒_)
+open import Luau.Type.ToString using (typeToString)
+
+ex1 : typeToString(nil) ≡ "nil"
+ex1 = refl
+
+ex2 : typeToString(nil ⇒ nil) ≡ "(nil) -> nil"
+ex2 = refl
+
+ex3 : typeToString(nil ⇒ (nil ⇒ nil)) ≡ "(nil) -> (nil) -> nil"
+ex3 = refl
+
+ex4 : typeToString(nil ∪ (nil ⇒ (nil ⇒ nil))) ≡ "((nil) -> (nil) -> nil)?"
+ex4 = refl
+
+ex5 : typeToString(nil ⇒ ((nil ⇒ nil) ∪ nil)) ≡ "(nil) -> ((nil) -> nil)?"
+ex5 = refl
diff --git a/prototyping/Luau/Type.agda b/prototyping/Luau/Type.agda
index 6ff05c89..60de2d1b 100644
--- a/prototyping/Luau/Type.agda
+++ b/prototyping/Luau/Type.agda
@@ -1,5 +1,7 @@
 module Luau.Type where
 
+open import FFI.Data.Maybe using (Maybe; just; nothing)
+
 data Type : Set where
   nil : Type
   _⇒_ : Type → Type → Type
@@ -23,3 +25,17 @@ tgt none = none
 tgt any = any
 tgt (S ∪ T) = (tgt S) ∪ (tgt T)
 tgt (S ∩ T) = (tgt S) ∩ (tgt T)
+
+optional : Type → Type
+optional nil = nil
+optional (T ∪ nil) = (T ∪ nil)
+optional T = (T ∪ nil)
+
+normalizeOptional : Type → Type
+normalizeOptional (S ∪ T) with normalizeOptional S | normalizeOptional T
+normalizeOptional (S ∪ T) | (S′ ∪ nil) | (T′ ∪ nil) = (S′ ∪ T′) ∪ nil
+normalizeOptional (S ∪ T) | S′ | nil = optional S′
+normalizeOptional (S ∪ T) | nil | T′ = optional T′
+normalizeOptional (S ∪ T) | S′ | T′ = S′ ∪ T′
+normalizeOptional T = T
+
diff --git a/prototyping/Luau/Type/ToString.agda b/prototyping/Luau/Type/ToString.agda
index 09a6d920..7533a3d7 100644
--- a/prototyping/Luau/Type/ToString.agda
+++ b/prototyping/Luau/Type/ToString.agda
@@ -1,13 +1,28 @@
 module Luau.Type.ToString where
 
 open import FFI.Data.String using (String; _++_)
-open import Luau.Type using (Type; nil; _⇒_; none; any; _∪_; _∩_)
+open import Luau.Type using (Type; nil; _⇒_; none; any; _∪_; _∩_; normalizeOptional)
 
+{-# TERMINATING #-}
 typeToString : Type → String
+typeToStringᵁ : Type → String
+typeToStringᴵ : Type → String
+
 typeToString nil = "nil"
 typeToString (S ⇒ T) = "(" ++ (typeToString S) ++ ") -> " ++ (typeToString T)
 typeToString none = "none"
 typeToString any = "any"
-typeToString (S ∪ T) = (typeToString S) ++ " | " ++ (typeToString T)
-typeToString (S ∩ T) = (typeToString S) ++ " & " ++ (typeToString T)
+typeToString (S ∪ T) with normalizeOptional(S ∪ T)
+typeToString (S ∪ T) | ((S′ ⇒ T′) ∪ nil) = "(" ++ typeToString (S′ ⇒ T′) ++ ")?"
+typeToString (S ∪ T) | (S′ ∪ nil) = "(" ++ typeToString S′ ++ "?"
+typeToString (S ∪ T) | (S′ ∪ T′) = "(" ++ typeToStringᵁ (S ∪ T) ++ ")"
+typeToString (S ∪ T) | T′ = typeToString T′
+typeToString (S ∩ T) = "(" ++ typeToStringᴵ (S ∩ T) ++ ")"
 
+typeToStringᵁ (S ⇒ T) = "(" ++ typeToString (S ⇒ T) ++ ")"
+typeToStringᵁ (S ∪ T) = (typeToStringᵁ S) ++ " | " ++ (typeToStringᵁ T)
+typeToStringᵁ T = typeToString T
+
+typeToStringᴵ (S ⇒ T) = "(" ++ typeToString (S ⇒ T) ++ ")"
+typeToStringᴵ (S ∩ T) = (typeToStringᴵ S) ++ " & " ++ (typeToStringᴵ T)
+typeToStringᴵ T = typeToString T