diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index e939d8ff3..0aaa7fe69 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -10,15 +10,15 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
 
       - name: Set up PureScript toolchain
         uses: purescript-contrib/setup-purescript@main
         with:
-          purescript: "0.15.7"
+          purescript: "0.15.13"
 
       - name: Cache PureScript dependencies
-        uses: actions/cache@v2
+        uses: actions/cache@v3
         with:
           key: ${{ runner.os }}-spago-${{ hashFiles('packages.dhall') }}
           path: |
@@ -38,9 +38,9 @@ jobs:
             22-Projects/.spago
 
       - name: Set up Node toolchain
-        uses: actions/setup-node@v2
+        uses: actions/setup-node@v3
         with:
-          node-version: "16"
+          node-version: "lts/*"
 
       - name: Install dependencies
         run: |
diff --git a/01-Getting-Started/01-Why-Learn-PureScript.md b/01-Getting-Started/01-Why-Learn-PureScript.md
index 5aa3c9c97..9115651bc 100644
--- a/01-Getting-Started/01-Why-Learn-PureScript.md
+++ b/01-Getting-Started/01-Why-Learn-PureScript.md
@@ -65,6 +65,7 @@ One of the main issues with JavaScript is a poor type system. Many errors aren't
 
 TypeScript seems to address this type safety issue. Just consider its name! However, a few people who are using PureScript now have said this about TypeScript: "You might as well be writing Javascript." TypeScript does not provide any real guarantees; it only pretends. PureScript does provide such guarantees.
 
+- [`fp-ts`'s Migration guide from PureScript to TypeScript](https://gcanti.github.io/fp-ts/guides/purescript.html). This is helpful for seeing 1) how much more TypeScript code it takes to implement the same feature in PureScript, and 2) how the resulting syntax IMO is of lesser quality and clarity than the corresponding PureScript code is.
 - [TypeScript vs PureScript: Not All Compilers Are Created Equal](https://blog.logrocket.com/typescript-vs-purescript-not-all-compilers-are-created-equal-c16dadaa7d3e)
 - [JavaScript, TypeScript, and PureScript](https://www.youtube.com/watch?v=JTEfpNtEoSA) or "Why TypeScript only 'pretends' to have types."
 - [Various examples comparing PureScript and TypeScript](https://discourse.purescript.org/t/type-system-showdown-purescript-and-typescript/2084)
diff --git a/01-Getting-Started/04-Install-Guide.md b/01-Getting-Started/04-Install-Guide.md
index 70f255c4c..f5d9ee229 100644
--- a/01-Getting-Started/04-Install-Guide.md
+++ b/01-Getting-Started/04-Install-Guide.md
@@ -48,7 +48,7 @@ Unlike the manual install, `nvm` properly handles the npm prefix for you. So, yo
 Once you have installed `npm`, we can use it to install everything in one command:
 
 ```sh
-npm i -g purescript@0.15.7 spago@0.20.9 esbuild@0.15.7 purs-tidy@0.9.2 purs-backend-es@1.3.1 purescript-psa@0.8.2
+npm i -g purescript@0.15.13 spago@0.21.0 esbuild@0.19.8 purs-tidy@0.10.0 purs-backend-es@1.4.2 purescript-psa@0.8.2
 ```
 
 
@@ -63,9 +63,9 @@ npm i -g purs-backend-es
 The following commands should now work:
 
 ```sh
-purs --version        # 0.15.7
-spago --version       # 0.20.9
-esbuild --version     # 0.15.7
+purs --version        # 0.15.13
+spago --version       # 0.21.0
+esbuild --version     # 0.19.8
 ```
 
 ### Building This Project
diff --git a/03-Build-Tools/Readme.md b/03-Build-Tools/Readme.md
index a30faa689..7210080e3 100644
--- a/03-Build-Tools/Readme.md
+++ b/03-Build-Tools/Readme.md
@@ -10,7 +10,11 @@ This folder accomplishes the following:
 
 ## History: How We Got Here
 
-The following explanation does not cover all the tools used in PureScript's ecosystem. However it provides context for later files. In short, `spago` is both the official dependency manager and build tool. `bower` can be thought of as a deprecated dependency manager; the community is in the process of building a registry that will replace the Bower registry since it no longer accepts uploads. `pulp` is a build tool that uses `bower`; its usage will become more common again once the registry is built.
+The following explanation does not cover all the tools used in PureScript's ecosystem. However it provides context for later files. 
+
+In short, `spago` is both the official dependency manager and build tool. It was originally written in Haskell. It's currently being rewritten in PureScript. The Haskell version is called `spago-legacy` whereas the rewrite is the alpha `spago`. Whenever this repo mentions `spago`, it's always in reference to `spago-legacy`.
+
+There are two other tools that are only around because alpha `spago` hasn't been finished yet. `bower` can be thought of as a deprecated dependency manager; the community used this tool because it provided a registry. `pulp` is a build tool that uses `bower`; its usage has become less frequent because of the migration towards `spago`.
 
 ### Phase 1: Initial Tooling
 
@@ -24,6 +28,8 @@ Bodil Stokke (with later contributions from Harry Garrood) later wrote a tool ca
 - publish libraries and their docs
 - easily bump the project's version
 
+This is why most of the "core" libraries (PureScript libraries stored under the `purescript` GitHub organization) still have `bower.json` files as their dependencies.
+
 ### Phase 2: The `psc-package` Experiment
 
 `Bower` worked fine, but there were a few user-interface issues that made it difficult to use, especially when a new PureScript release was made that included breaking changes.
@@ -40,7 +46,7 @@ See the below image to visualize this:
 
 ### Phase 3: Improving the `psc-package` Developer Workflow via `Spago`
 
-From the above image, one should infer that using `pulp` and `bower` was overall easier to use and explain. Thus, Justin Woo and Fabrizo Ferrai started a project called `spago`. `spago` evolved out of `spacchetti` and reimplemented parts of `psc-package` into one program with a seamless developer workflow. While `psc-package` can still be used, it's better to use `spago`.
+From the above image, one should infer that using `pulp` and `bower` was overall easier to use and explain. Thus, Justin Woo and Fabrizo Ferrai started a project called `spago`. `spago` evolved out of `spacchetti` and reimplemented parts of `psc-package` into one program with a seamless developer workflow. While `psc-package` can still be used, it became better to use `spago`.
 
 The below image summarizes the current state:
 
@@ -48,9 +54,9 @@ The below image summarizes the current state:
 
 ### Phase 4: `Spago` becomes mainstream while `psc-package` is less used
 
-Spago dropped support for `psc-package` commands in the `v0.11.0` release. `psc-package` is still usable and is more or less feature-complete. However, no further work on it will be done. Rather, Spago has become the main dependency manager when utilizing package-sets.
+Spago dropped support for `psc-package` commands in the `v0.11.0` release. `psc-package` was still usable and was more or less feature-complete. However, no further work was being done on it. Rather, Spago had become the main dependency manager when utilizing package-sets.
 
-The community is now split between `pulp` + `bower` workflows and `spago` workflows. One must still use `pulp` + `bower` if they want to do the following:
+At this point, part of the community used `pulp` + `bower` workflows while the rest used `spago` workflows. One must still use `pulp` + `bower` if they want to do the following:
 - publish their library's docs to Pursuit
 - include their library in a package set, so `spago` users can use it
 
@@ -58,20 +64,11 @@ The community is now split between `pulp` + `bower` workflows and `spago` workfl
 
 The Bower registry stopped accepting new uploads. The community quickly updated their tooling to workaround how libraries are published and installed. However, it was clear that PureScript now needed to create a registry.
 
-Fabrizio Ferrai led the effort to build this registry with significant input from Harry Garrood. The registry is not yet complete, so the community is in this in-between stage.
-
-Regardless, the following is still true:
-- most people are now using `spago`
-- the `pulp` + `bower` workflow is still needed to publish a library, but it works differently now.
-    - See [these instructions for how to use `bower` to publish a library in this in-between context](https://discourse.purescript.org/t/up-to-date-instructions-for-publishing-new-packages/1953)
-    - See the `Dependency Managers/Bower Explained` file for clarification on how to install packages as dependencies if one is using `bower`
-- Thomas has written a [Recommended Tooling for PureScript Applications](https://discourse.purescript.org/t/recommended-tooling-for-purescript-applications-in-2019/948) post.
-
-See [The `bower` registry is no longer accepting package submissions](https://discourse.purescript.org/t/the-bower-registry-is-no-longer-accepting-package-submissions/1103/) for more context.
+Fabrizio Ferrai led the effort to build this registry with significant input from Harry Garrood. The registry is not yet complete, so the community is in this in-between stage. See [The `bower` registry is no longer accepting package submissions](https://discourse.purescript.org/t/the-bower-registry-is-no-longer-accepting-package-submissions/1103/) for more context.
 
 ### Phase 6: Updating JavaScript output to ES modules and delegating bundling to 3rd-party tools
 
-In PureScript `0.15.0`, we stopped compiling PureScript source code to CommonJS modules and started compiling to ES modules. As a result, we dropped the buggy and broken bundler provided via `purs bundle` and instead directed endusers to use 3rd-party bundlers like `esbuild`, `webpack`, and `parecel`. Such bundlers often produced smaller bundles than `purs bundle`. Moreover, it gave the core team in charge of PureScript one less thing to maintain.
+In PureScript `0.15.0`, we stopped compiling PureScript source code to CommonJS modules and started compiling to ES modules. As a result, we dropped the buggy and broken bundler provided via `purs bundle` and instead directed end-users to use 3rd-party bundlers like `esbuild`, `webpack`, and `parcel`. Such bundlers often produced smaller bundles than `purs bundle`. Moreover, it gave the core team in charge of PureScript one less thing to maintain.
 
 See the [0.15.0 Migration Guide](https://github.com/purescript/documentation/blob/master/migration-guides/0.15-Migration-Guide.md) for more details.
 
@@ -81,15 +78,29 @@ While the Purescript compiler produces correct JavaScript code, there were a num
 
 Soon after the time that PureScript `0.15.4` was released, a new project called `purs-backend-es` was released. This project works on the `CoreFn` representation and transforms it to JavaScript. However, it also optimizes the code significantly during this tranformation. For a few example, see [the `purs` and `purs-backend-es` comparison table in its README](https://github.com/aristanetworks/purescript-backend-optimizer#overview).
 
-While this tool's main purpose is to produce optimized JavaScript code, it enables others to produce new backends. A backend is a target language to which PureScript can be compiled. Before this tool, every backend had to reinvent a lot of code to make it work for that language. With the underlying library, `purescript-backend-optimizer`, one can more easily produce a new backend.
+While this tool's main purpose is to produce optimized JavaScript code, it enables others to produce new backends more easily. A backend is a target language to which PureScript can be compiled. Before this tool, every backend had to reinvent a lot of code to make it work for that language. With the underlying library, `purescript-backend-optimizer`, one can more easily produce a new backend.
+
+### Phase 8: The Registry and the Spago Rewrite
+
+The Registry's speed of development was lackluster for quite some time. Fortunately, Thomas Honeyman made it a personal goal to see the Registry implemented. Since then, the Registry's development picked up and eventually became useable, although it's still not yet finished.
+
+More recently, Fabrizio decided to rewrite Spago in PureScript. The main advantage of doing this was the ability to leverage the Registry codebase within Spago, allowing for a more seamless publishing workflow among other things. Such work is still on-going as of this writing (Sept 2023). But, the version of Spago written in Haskell is now known as "Spago Legacy" and the version written in PureScript is "Spago Next" because one install spago next via `npm i spago@next`.
+
+## Spago: Haskell Legacy codebase or PureScript rewrite codebase?
+
+| Type | NPM Package | Versions | Install via | Alternative |
+| - | - | - | - | - |
+| Legacy Spago | `spago` | `0.0.1` - `0.21.0` | `npm i spago` | `npm i spago-legacy` (installs `spago@0.21.0` under binary name `spago-legacy`) |
+| Rewrite Spago | `spago` | `0.92.0` - `0.93.x` | `npm i spago@next` | - |
 
 ## Overview of Tools
 
 | Name | Type/Usage | Comments | URL |
 | - | - | - | - |
 | purs | PureScript Compiler | Used to be called `psc` | -- |
-| spago | Build Tool | Front-end to `purs` and `package-set`-based projects | https://github.com/purescript/spago
-| pulp | Build Tool | Front-end to `purs`. Builds & publishes projects | https://github.com/purescript-contrib/pulp |
+| spago (rewrite) | Build Tool | Front-end to `purs`; `package-set`-based or dependency-range -based projects | https://github.com/purescript/spago |
+| spago (legacy) | Build Tool | Front-end to `purs` and `package-set`-based projects | https://github.com/purescript/spago-legacy
+| pulp | Build Tool | Front-end to `purs`. Builds & publishes projects (being deprecated) | https://github.com/purescript-contrib/pulp |
 | bower | Dependency Manager (being deprecated) | -- | https://bower.io/ |
 | purs-tidy | PureScript Formatter | -- | https://github.com/natefaubion/purescript-tidy
 | purs-backend-es | Produces optimized JavaScript from PureScript | Only intended for production-level usage | https://github.com/aristanetworks/purescript-backend-optimizer
diff --git a/11-Syntax/01-Basic-Syntax/src/16-Visible-Type-Applications/01-Intro.purs b/11-Syntax/01-Basic-Syntax/src/16-Visible-Type-Applications/01-Intro.purs
new file mode 100644
index 000000000..213853edc
--- /dev/null
+++ b/11-Syntax/01-Basic-Syntax/src/16-Visible-Type-Applications/01-Intro.purs
@@ -0,0 +1,88 @@
+module Syntax.Basic.VisibleTypeApplications.Intro where
+                                                                            {-
+Visible Type Applications is a feature that only works completely 
+as of PureScript 0.15.13. While it was supported earlier than that,
+there were a few bugs that hindered its usage. The content in this file
+and those that follow in this folder assume one is using PureScript 0.15.13.
+
+Sometimes, using polymorphic code can be annoying
+because the compiler cannot infer what type you want to use.                -}
+
+polymorphicCode :: forall pleaseInferThisType. pleaseInferThisType -> Int
+polymorphicCode _someValue = 1
+                                                                            {-
+problematicUsage :: Int
+problematicUsage = polymorphicCode []
+
+The above code is commented out because it will produce a compiler error.
+The empty array is inferred by the compiler to have the type,
+`forall a. Array a`. Because there are no elements within the
+array, the compiler has no idea what the element type is. So, it infers it
+to the most generic type it can be: `forall a. a`.
+
+In this situation, we would need to tell the compiler what that type is
+by doing one of two things:
+- indicating what the input type of `polymorphicCode` is
+- indicating what the element type of the empty array is
+
+
+There's two ways to tell the compiler what the type should be 
+when the compiler cannot figure it out.
+
+The first way is to add a type annotation (usually after wrapping 
+the expression in parenthesis). This is annoying to do because 
+of the added parenthesis, two colons, and in some cases the need to
+fully specify all the types of the function or value.                                               -}
+
+usage_inputType :: Int
+usage_inputType = (polymorphicCode :: Array String -> Int) []
+
+usage_elemType :: Int
+usage_elemType = polymorphicCode ([] :: Array String)
+                                                                            {-
+The second way is using "visible type applications".
+
+Using `forall someType. someType -> Int` as an example, the 
+`forall someType.` part is really a function. We could read the above as
+"Given an argument that is a type (e.g. `String`) rather than a value 
+(e.g. "foo"), I will return to you a function that takes a value of that type 
+and produce a value of type `Int`."
+
+"Visible Type Applications" are called thus because these type arguments
+are applied to these kinds of functions, but these applications that were
+previously invisible to the user are now made visible. Put differently,
+the compiler would automatically apply these type arguments but without the
+user's knowledge or input. Now, however, the user can also apply these type arguments.
+
+Visible Type Applications (or VTAs for short) are opt-in syntax. 
+They only work if one writes their `forall` part a specific way 
+by adding a `@` character in front of the type variable name 
+(e.g. `someType` becomes `@someType`).
+
+Rewriting `polymorphicCode` to use this opt-in syntax, we get:                        -}
+
+polymorphicCode2 :: forall @pleaseInferThisType. pleaseInferThisType -> Int
+polymorphicCode2 _someValue = 1
+
+-- And now we can use it by applying the type `String` to that type variable.
+-- We apply the type by putting a `@` character in front of the type name.
+usage2_example :: Int
+usage2_example = polymorphicCode2 @String "bar"
+
+-- In our original case of using a higher-kinded type (e.g. `Array Int`),
+-- we need to wrap the type in parenthesis.
+
+usage2_inputType :: Int
+usage2_inputType = polymorphicCode2 @(Array String) []
+
+-- Since `[]`'s inferred type is `forall a. Array a` rather than `forall @a. Array a`,
+-- we cannot use VTAs to determine the element type.
+-- This code is commented out because we'll get a compiler error.
+--    usage2_elemType :: Int
+--    usage2_elemType = polymorphicCode2 ([] @String))
+
+-- Lastly, if we opt-in to this VTA syntax, we must either use it or not use it doesn't mean we have to use VTAs
+-- to make the function work. The below code is valid
+
+usage3 :: Int
+usage3 = polymorphicCode2 true
diff --git a/11-Syntax/01-Basic-Syntax/src/16-Visible-Type-Applications/02-Order-Matters.purs b/11-Syntax/01-Basic-Syntax/src/16-Visible-Type-Applications/02-Order-Matters.purs
new file mode 100644
index 000000000..97a21deca
--- /dev/null
+++ b/11-Syntax/01-Basic-Syntax/src/16-Visible-Type-Applications/02-Order-Matters.purs
@@ -0,0 +1,71 @@
+module Syntax.Basic.VisibleTypeApplications.OrderMatters where
+
+-- When we write the following function...
+basicFunction :: Int -> String -> Boolean -> String
+basicFunction _i _s _b = "returned value"
+
+-- ... we know that the order of the arguments matters.
+-- The below usage is valid
+usage :: String
+usage = basicFunction 1 "foo" false
+
+-- whereas this one is not because the first argument must be an `Int`
+--    usage2 :: String
+--    usage2 = basicFunction "foo" 1 false
+
+-- Similarly, because functions are curried, 
+-- when we apply just one argument, we get back a function
+-- that takes the remaining arguments
+
+basicFunction' :: String -> Boolean -> String
+basicFunction' = basicFunction 1
+
+-- These same ideas apply to VTAs. Notice below that VTA support is only added
+-- to the second and fourth type variable.
+vtaFunction
+  :: forall first @second third @fourth
+   . first
+  -> second
+  -> third
+  -> fourth
+  -> String
+vtaFunction _first _second _third _fourth = "returned value"
+
+-- Type-level arguments (e.g. VTAs) are always applied before value-level arguments.
+-- Why? Because those arguments appear earlier in the function.
+-- If we want to use VTAs to specify which types `second` and `fourth` are,
+-- we must apply those type arguments BEFORE applying any value arguments. In other words,
+-- the below code is correct:
+
+usage3 :: String
+usage3 = vtaFunction @Int @Int "first" 2 "third" 4
+
+-- whereas this code would be incorrect:
+--    usage3 :: String
+--    usage3 = vtaFunction "first" @Int 2 "third" @Int 4
+
+-- Put differently, we can define a new function by only applying a single type argument.
+
+vtaFunction'
+  :: forall first third fourth
+   . first
+  -> Int
+  -> third
+  -> fourth
+  -> String
+vtaFunction' = vtaFunction @Int -- force `second` to be `Int`
+
+-- Or by type-applying multiple arguments
+vtaFunction''
+  :: forall first third
+   . first
+  -> Int
+  -> third
+  -> Int
+  -> String
+vtaFunction'' = vtaFunction @Int @Int -- force `second` and `fourth` to be `Int`
+
+-- Note: the astute reader will have noticed that the `@` characters don't appear in
+-- `vtaFunction'` and `vtaFunction''`. Since this is opt-in syntax, one must
+-- opt-in every time a new function is defined, even if that function
+-- is derived from applying one argument to a multi-argument curried function.
diff --git a/11-Syntax/01-Basic-Syntax/src/16-Visible-Type-Applications/03-Skipping-Wildcards.purs b/11-Syntax/01-Basic-Syntax/src/16-Visible-Type-Applications/03-Skipping-Wildcards.purs
new file mode 100644
index 000000000..5d2bbb7c0
--- /dev/null
+++ b/11-Syntax/01-Basic-Syntax/src/16-Visible-Type-Applications/03-Skipping-Wildcards.purs
@@ -0,0 +1,44 @@
+module Syntax.Basic.VisibleTypeApplications.SkippingWildcards where
+
+-- Because order matters and because a single function may have 
+-- multiple VTA-supported type variables, we may sometimes run
+-- into another problem.
+
+multipleTypes
+  :: forall @skip @specify @other1 @other2
+   . skip
+  -> specify
+  -> other1
+  -> other2
+  -> String
+multipleTypes _skip _specify _other1 _other2 = "returned value"
+
+-- Let's say we only want to use VTAs to specify the type for the 
+-- second VTA-supported type variable (i.e `specify` above) 
+-- without specifying the first one (e.g. `skip`).
+-- We can only type-apply the second one after we have 
+-- type-applied the first. So, how can we achieve our goal?
+
+-- Fortunately, PureScript uses the wildcard VTA syntax (i.e. `@_`)
+-- to skip type variables, so that one can type-apply other ones.
+
+onlySpecifyTypeApplied
+  :: forall skip other1 other2
+   . skip
+  -> String
+  -> other1
+  -> other2
+  -> String
+onlySpecifyTypeApplied = multipleTypes @_ @String
+
+-- Again, if we want the VTA-support to be added to the derived function
+-- we need to opt-in to that syntax:
+
+onlySpecifyTypeApplied'
+  :: forall @skip @other1 @other2
+   . skip
+  -> String
+  -> other1
+  -> other2
+  -> String
+onlySpecifyTypeApplied' = multipleTypes @_ @String
diff --git a/11-Syntax/01-Basic-Syntax/src/16-Visible-Type-Applications/04-Usage.purs b/11-Syntax/01-Basic-Syntax/src/16-Visible-Type-Applications/04-Usage.purs
new file mode 100644
index 000000000..127cf003a
--- /dev/null
+++ b/11-Syntax/01-Basic-Syntax/src/16-Visible-Type-Applications/04-Usage.purs
@@ -0,0 +1,44 @@
+module Syntax.Basic.VisibleTypeApplications.Usage where
+
+-- When one opts-in to the VTA-supported type variables,
+-- one does not need to use VTAs to call the function.
+
+multiVtaFn :: forall @a @b @c. a -> b -> c -> String
+multiVtaFn _a _b _c = "returned value"
+
+-- Proof that we don't have to use VTAs for the function to still work.
+-- The compiler will infer that `a`, `b`, and `c` have type `Int`.
+usage_noVtas :: String
+usage_noVtas = multiVtaFn 1 2 3
+
+-- Proof that we can type-apply only as many types as we want.
+usage_useVtas1 :: forall b c. Int -> b -> c -> String
+usage_useVtas1 = multiVtaFn @Int
+
+usage_useVtas2 :: forall a c. a -> Int -> c -> String
+usage_useVtas2 = multiVtaFn @_ @Int
+
+usage_useVtas2b :: forall a c. a -> Int -> c -> String
+usage_useVtas2b = multiVtaFn @_ @Int @_ -- The second @_ is pointless but unharmful.
+
+usage_useVtas3 :: forall a b. a -> b -> Int -> String
+usage_useVtas3 = multiVtaFn @_ @_ @Int
+
+-- Proof that we can apply the third type argument and apply the first value argument
+-- to get a derived function.
+usage_mixed :: forall b. b -> Int -> String
+usage_mixed = multiVtaFn @_ @_ @Int "a"
+
+-- Here's a more interesting usage of VTAs. Once a type variable is brought into scope,
+-- whether through a normal type variable (e.g. `forall a.`) 
+-- or VTA-supported type variable (e.g. `forall @a.`), 
+-- we can apply that type variable as a type argument to functions that support VTAs.
+-- In the below example, `returnFoo`'s `x` is being specified to whatever `a` and `b` are.`
+outerFunction :: forall a b. a -> b -> String
+outerFunction aVal bVal = returnSecond (returnFoo @a aVal) (returnFoo @b bVal)
+  where
+  returnFoo :: forall @x. x -> String
+  returnFoo _x = "foo"
+
+  returnSecond :: forall first second. first -> second -> first
+  returnSecond first _ = first
\ No newline at end of file
diff --git a/11-Syntax/01-Basic-Syntax/src/16-Visible-Type-Applications/05-TypeClasses.purs b/11-Syntax/01-Basic-Syntax/src/16-Visible-Type-Applications/05-TypeClasses.purs
new file mode 100644
index 000000000..ed04521fd
--- /dev/null
+++ b/11-Syntax/01-Basic-Syntax/src/16-Visible-Type-Applications/05-TypeClasses.purs
@@ -0,0 +1,73 @@
+module Syntax.Basic.VisibleTypeApplications.TypeClasses where
+
+-- When it comes to functions, VTA-support is opt-in.
+-- But for type classes, VTAs are always supported for the
+-- type variables in the class head.
+
+class MyClass typeVariableInClassHead where
+  toString :: typeVariableInClassHead -> String
+
+instance MyClass String where
+  toString x = x
+
+instance MyClass Int where
+  toString _ = "foo"
+
+-- The type of `toString` is `forall @a. MyClass a => a -> String`.
+-- So, we can choose which instance to use by using VTAs
+
+stringExample1 = toString @String "foo"
+intExample1 = toString @Int 1
+
+-- Again, the type signature of `multi` here is
+-- `multi :: forall @a @b @c. Multi a b c => a -> b -> c -> String`
+class Multi a b c where
+  multi :: a -> b -> c -> String
+
+instance Multi Int Int String where
+  multi _ _ _ = "string"
+
+instance Multi Int Int Int where
+  multi _ _ _ = "int"
+
+-- So, using it here looks like
+stringExample2 = multi @Int @Int @String 1 2 "3"
+intExample2 = multi @Int @Int @Int 1 2 3
+
+-- Before PureScript 0.15.13, the following type class was invalid.
+
+class UniqueValue a where
+  uniqueValue :: String
+
+-- The compiler uses the arguments passed to a type class member
+-- (e.g. `uniqueValue`) to determine which types specify the
+-- type variables in the type class head. But because the
+-- type variable in the class head (i.e. `a`) never appears in the
+-- type signature of `uniqueValue`, there was no way for the compiler
+-- to figure out which instance should be used. So, it would fail
+-- with a compiler error. Thus, the compiler prevented one
+-- from even writing such a class.
+
+-- Now that we have VTAs, this class is only valid because the compiler
+-- assumes one will use VTAs to select the instance.
+-- The full type signature of `uniqueValue` is now
+--    `uniqueValue :: forall @a. UniqueValue a => String`
+
+instance UniqueValue Int where
+  uniqueValue = "Int"
+instance UniqueValue String where
+  uniqueValue = "String"
+
+stringExample3 :: String
+stringExample3 = uniqueValue @String
+
+intExample3 :: String
+intExample3 = uniqueValue @Int
+
+-- VTAs are useful because they allow us to specify which type class 
+-- instance to use in a concise way. This is more apparent when
+-- we use type classes to derive functions from their members.
+
+-- Moreover, now that VTAs are supported, `Proxy` arguments 
+-- are no longer needed. `Proxy` arguments are covered in 
+-- more detail in the type-level programming syntax folder.
diff --git a/11-Syntax/01-Basic-Syntax/src/16-Visible-Type-Applications/11-Gotchas.purs b/11-Syntax/01-Basic-Syntax/src/16-Visible-Type-Applications/11-Gotchas.purs
new file mode 100644
index 000000000..c095873ad
--- /dev/null
+++ b/11-Syntax/01-Basic-Syntax/src/16-Visible-Type-Applications/11-Gotchas.purs
@@ -0,0 +1,27 @@
+module Syntax.Basic.VisibleTypeApplications.Gotchas where
+
+-- Gotcha #1: Different orders between definition and usage
+-- One can define two VTA-supported type variables but use the second one in the
+-- type signature before the first one.
+
+possibleGotcha
+  :: forall @definedFirstUsedSecond @definedSecondUsedFirst
+   . definedSecondUsedFirst
+  -> definedFirstUsedSecond
+  -> Int
+possibleGotcha _firstArg _secondArg = 2
+
+-- Type-applying `String` here affects the type of the second argument to this function,
+-- not the first, because that's where `definedFirstUsedSecond` is used.
+unexpectedFunction :: forall firstArg. firstArg -> String -> Int
+unexpectedFunction = possibleGotcha @String
+
+
+-- Gotcha #2: forgetting to opt-in to VTA support when deriving a function
+
+mainFunction :: forall @a @b. a -> b -> Int
+mainFunction _a _b = 1
+
+-- Unless we specify `forall @b` here, the type signature will be `forall b`
+derivedFunction :: forall b. Int -> b -> Int
+derivedFunction = mainFunction @Int
diff --git a/11-Syntax/03-Type-Level-Programming-Syntax/src/04-Using-Type-Level-Values/01-Reflection.purs b/11-Syntax/03-Type-Level-Programming-Syntax/src/04-Using-Type-Level-Values/01-Reflection.purs
index f367374bb..b8ad8e875 100644
--- a/11-Syntax/03-Type-Level-Programming-Syntax/src/04-Using-Type-Level-Values/01-Reflection.purs
+++ b/11-Syntax/03-Type-Level-Programming-Syntax/src/04-Using-Type-Level-Values/01-Reflection.purs
@@ -3,6 +3,10 @@ module Syntax.TypeLevel.Reflection where
 -- ignore this
 import Prelude (class Show)
 
+-- In PureScript 0.15.13, Visible Type Applications were fully supported.
+-- Before that release, we had to use `Proxy` arguments.
+-- Now, we can use VTAs in some contexts. This file will show both for clarity.
+
 -- Reflection syntax
 --  Converting a type-level value into a value-level value
 
@@ -20,6 +24,8 @@ reflectVL TypeValue = "value-level value"
 data CustomKind
 foreign import data CustomKindValue :: CustomKind
 
+-- PureScript <0.15.13 Approach: use Proxy arguments
+
 data Proxy :: forall k. k -> Type
 data Proxy kind = Proxy
 
@@ -31,6 +37,17 @@ class TLI_to_VLI customKind where
 instance TLI_to_VLI CustomKindValue where {-
   reflectCustomKind Proxy = "value-level value" -}
   reflectCustomKind _     = "value-level value"
+
+-- PureScript >=0.15.13 Approach: use Visible Type Applications
+
+-- "type-level value to value-level value"
+class TLI_to_VLI_Vta :: CustomKind -> Constraint
+class TLI_to_VLI_Vta customKind where
+  reflectCustomKindVta :: Value_Level_Type
+
+instance TLI_to_VLI_Vta CustomKindValue where
+  reflectCustomKindVta = "value-level value"
+
 ----------------------------
 
 -- An example using the Boolean-like data type YesNo:
@@ -40,6 +57,7 @@ data YesNoKind
 foreign import data YesK :: YesNoKind
 foreign import data NoK  :: YesNoKind
 
+-- PureScript <0.15.13 Approach: use Proxy arguments
 {-
 Read yesK and noK as:
   yesK = (YesNoProxyValue :: YesNoProxy Yes) - a value of type "YesNoProxy Yes"
@@ -86,6 +104,42 @@ else instance IsYes a where
 --    isYes yesK
 --    isYes noK
 
+-- PureScript >=0.15.13 Approach: use Visible Type Applications
+
+class IsYesNoKindVta :: YesNoKind -> Constraint
+class IsYesNoKindVta a where
+  reflectYesNoVta :: YesNo
+
+instance IsYesNoKindVta YesK where
+   reflectYesNoVta = Yes
+
+instance IsYesNoKindVta NoK where
+   reflectYesNoVta = No
+
+
+-- We can also use instance chains here to distinguish
+-- one from another
+
+class IsYesVta :: YesNoKind -> Constraint
+class IsYesVta a where
+  isYesVta :: YesNo
+
+instance IsYesVta YesK where
+  isYesVta = Yes
+else instance IsYesVta a where
+  isYesVta = No
+
+-- Using instance chains here is more convenient if we had
+-- a lot more type-level values than just 2. In some cases,
+-- it is needed in cases where a type-level type can have an
+-- infinite number of values, such as a type-level String
+
+-- Open a REPL, import this module, and then run this code:
+--    reflectYesNoVta @YesK
+--    reflectYesNoVta @NoK
+--    isYesVta @YesKyesK
+--    isYesVta @NoK
+
 
 -- necessary for not getting errors while trying the functions in the REPL
 
diff --git a/11-Syntax/03-Type-Level-Programming-Syntax/src/04-Using-Type-Level-Values/02-Reification.purs b/11-Syntax/03-Type-Level-Programming-Syntax/src/04-Using-Type-Level-Values/02-Reification.purs
index 7266f8993..2b3f215cb 100644
--- a/11-Syntax/03-Type-Level-Programming-Syntax/src/04-Using-Type-Level-Values/02-Reification.purs
+++ b/11-Syntax/03-Type-Level-Programming-Syntax/src/04-Using-Type-Level-Values/02-Reification.purs
@@ -39,6 +39,8 @@ data YesNoKind
 foreign import data YesK :: YesNoKind
 foreign import data NoK  :: YesNoKind
 
+-- PureScript <0.15.13 Approach: use Proxy arguments
+
 data Proxy :: forall k. k -> Type
 data Proxy kind = Proxy
 
@@ -62,13 +64,39 @@ instance IsYesNoKind NoK where
 -- the corresponding type-level value as its only argument
 -- (where we do type-level programming):
 
-reifyYesNo :: forall returnType
-            . YesNo
-            -> (forall b. IsYesNoKind b => Proxy b -> returnType)
-            -> returnType
+reifyYesNo 
+  :: forall returnType
+   . YesNo
+  -> (forall b. IsYesNoKind b => Proxy b -> returnType)
+  -> returnType
 reifyYesNo Yes function = function yesK
 reifyYesNo No  function = function noK
 
+
+
+-- PureScript >=0.15.13 Approach: use Visible Type Applications
+
+class IsYesNoKindVta :: YesNoKind -> Constraint
+class IsYesNoKindVta a where
+  reflectYesNoVta :: YesNo
+
+instance IsYesNoKindVta YesK where
+  reflectYesNoVta = Yes
+
+instance IsYesNoKindVta NoK where
+  reflectYesNoVta  = No
+
+-- We can reify a YesNo by defining a callback function that 
+-- has the corresponding type-level value type-applied
+
+reifyYesNoVta
+  :: forall returnType
+  . YesNo
+  -> (forall @b. IsYesNoKindVta b => returnType)
+  -> returnType
+reifyYesNoVta Yes function = function @YesK
+reifyYesNoVta No  function = function @NoK
+
 -- necessary for not getting errors while trying the functions in the REPL
 
 instance Show YesNo where
diff --git a/11-Syntax/03-Type-Level-Programming-Syntax/src/04-Using-Type-Level-Values/10-Conventions.purs b/11-Syntax/03-Type-Level-Programming-Syntax/src/04-Using-Type-Level-Values/10-Conventions.purs
index 0af8dedb9..f777feb00 100644
--- a/11-Syntax/03-Type-Level-Programming-Syntax/src/04-Using-Type-Level-Values/10-Conventions.purs
+++ b/11-Syntax/03-Type-Level-Programming-Syntax/src/04-Using-Type-Level-Values/10-Conventions.purs
@@ -15,6 +15,8 @@ type Value_Level_Type = String
 data KindName
 foreign import data Value :: KindName
 
+-- PureScript <0.15.13 Approach: use Proxy arguments
+
 data Proxy :: forall k. k -> Type
 data Proxy kind = Proxy
 
@@ -43,3 +45,32 @@ reifyKindName :: forall r
           -> (forall a. IsKindName a => Proxy a -> r)
           -> r
 reifyKindName _valueLevel function = function inst
+
+
+
+-- PureScript >=0.15.13 Approach: use Visible Type Applications
+
+-- Note: below we will add the 'Vta'
+-- suffix so as not to clash names with the previous class
+
+-- The class name is usually "Is[KindName]".
+class IsKindNameVta :: KindName -> Constraint
+class IsKindNameVta a where
+  -- and the reflect function is usually "reflect[KindName]"
+  reflectKindNameVta :: Value_Level_Type
+
+instance IsKindNameVta Value where
+  reflectKindNameVta = "value-level value"
+
+-- NANS
+class IsKindNameVta a <= ConstrainedToKindNameVta a
+
+-- NANS
+instance ConstrainedToKindNameVta Value
+
+-- Usually reify[KindName]
+reifyKindNameVta :: forall r
+           . Value_Level_Type
+          -> (forall @a. IsKindNameVta a => r)
+          -> r
+reifyKindNameVta _valueLevel function = function @Value
diff --git a/21-Hello-World/02-Effect-and-Aff/src/01-Effect/01-Native-Side-Effects-via-Effect.md b/21-Hello-World/02-Effect-and-Aff/src/01-Effect/01-Native-Side-Effects-via-Effect.md
index 819029d07..0a1004b36 100644
--- a/21-Hello-World/02-Effect-and-Aff/src/01-Effect/01-Native-Side-Effects-via-Effect.md
+++ b/21-Hello-World/02-Effect-and-Aff/src/01-Effect/01-Native-Side-Effects-via-Effect.md
@@ -35,7 +35,7 @@ unit = Unit
 type PendingComputation a = (Unit -> a)
 
 -- | A data structure that stores a pending computation.
-data Effect a = Box (PendingComputation a -> a)
+data Effect a = Box (PendingComputation a)
 
 -- | This unwraps the data structure to get the
 -- | pending computation, uses it to compute a value,
diff --git a/21-Hello-World/05-Application-Structure/src/02-MTL/02-Implementing-a-Monad-Transformer/03-A-Magical-Monad.md b/21-Hello-World/05-Application-Structure/src/02-MTL/02-Implementing-a-Monad-Transformer/03-A-Magical-Monad.md
index bca3a7c80..59b1f2cb9 100644
--- a/21-Hello-World/05-Application-Structure/src/02-MTL/02-Implementing-a-Monad-Transformer/03-A-Magical-Monad.md
+++ b/21-Hello-World/05-Application-Structure/src/02-MTL/02-Implementing-a-Monad-Transformer/03-A-Magical-Monad.md
@@ -210,7 +210,7 @@ instance (Monad m) => Monad (StateT state monad)
 ### MonadState
 
 ```haskell
-instance (Monad m) => Monad (StateT state monad) where
+instance (Monad monad) => MonadState state (StateT state monad) where
   state :: forall value. (state -> Tuple value state) -> StateT state monad value
   state f = StateT (\s -> pure $ f s)
 ```
diff --git a/21-Hello-World/06-Type-Level-Programming/Readme.md b/21-Hello-World/06-Type-Level-Programming/Readme.md
index 1e825e358..b51f4d548 100644
--- a/21-Hello-World/06-Type-Level-Programming/Readme.md
+++ b/21-Hello-World/06-Type-Level-Programming/Readme.md
@@ -35,7 +35,7 @@ elemAtIndex 3 (IndexedArray 3 [0, 1]) -- compiler error!
 elemAtIndex 0 (IndexedArray Empty []) -- compiler error!
 ```
 
-This is exactly what the library [Vec](https://pursuit.purescript.org/packages/purescript-sized-vectors/3.1.0/docs/Data.Vec#t:Vec) does.
+This is exactly what the library [sized-vectors](https://pursuit.purescript.org/packages/purescript-sized-vectors/3.1.0/docs/Data.Vec#t:Vec) does.
 
 ## Issues with Type-Level Programming
 
@@ -49,7 +49,10 @@ Consider purchasing the `Thinking with Types` book mentioned in `ROOT_FOLDER/Syn
 ## Compilation Instructions
 
 ```bash
-spago run -m TLP.SymbolExample
-spago run -m TLP.IntegerExample
-spago run -m TLP.RowExample
+spago run -m TLP.SymbolExample.Proxy
+spago run -m TLP.SymbolExample.VTAs
+spago run -m TLP.IntegerExample.Proxy
+spago run -m TLP.IntegerExample.VTAs
+spago run -m TLP.RowExample.Proxy
+spago run -m TLP.RowExample.VTAs
 ```
diff --git a/21-Hello-World/06-Type-Level-Programming/src/02-Symbol-Example.purs b/21-Hello-World/06-Type-Level-Programming/src/02-Symbol-Example/01-Proxy.purs
similarity index 97%
rename from 21-Hello-World/06-Type-Level-Programming/src/02-Symbol-Example.purs
rename to 21-Hello-World/06-Type-Level-Programming/src/02-Symbol-Example/01-Proxy.purs
index 998750484..3c45bcb87 100644
--- a/21-Hello-World/06-Type-Level-Programming/src/02-Symbol-Example.purs
+++ b/21-Hello-World/06-Type-Level-Programming/src/02-Symbol-Example/01-Proxy.purs
@@ -1,4 +1,5 @@
-module TLP.SymbolExample where
+-- This file uses Proxy arguments in its examples
+module TLP.SymbolExample.Proxy where
 
 import Prelude
 import Data.Tuple(Tuple(..))
diff --git a/21-Hello-World/06-Type-Level-Programming/src/02-Symbol-Example/02-VTAs.purs b/21-Hello-World/06-Type-Level-Programming/src/02-Symbol-Example/02-VTAs.purs
new file mode 100644
index 000000000..3fef78c35
--- /dev/null
+++ b/21-Hello-World/06-Type-Level-Programming/src/02-Symbol-Example/02-VTAs.purs
@@ -0,0 +1,128 @@
+-- This file uses Visible Type Applications in its examples
+module TLP.SymbolExample.VTAs where
+
+import Prelude
+
+import Data.Reflectable (class Reflectable, reflectType)
+import Data.Symbol (class IsSymbol, reflectSymbol)
+import Data.Tuple (Tuple(..))
+import Effect (Effect)
+import Effect.Console (log)
+import Prim.Ordering as O
+import Prim.Symbol as Symbol
+import Type.Proxy (Proxy(..))
+
+-- Note: `Data.Reflectable` still uses Proxy arguments. 
+-- It should be defined as
+--   class Reflectable t v | t -> v where
+--     reflectType :: v
+--
+-- This will be fixed in the PureScript 0.16.0 ecosystem update.
+-- So for now, we'll define our own type class to show how things would work.
+
+class Reflect :: forall k. k -> Type -> Constraint
+class Reflect ty val | ty -> val where
+  reflectTy :: val
+
+instance (Reflectable ty val) => Reflect ty val where
+  reflectTy = reflectType (Proxy  :: Proxy ty)
+
+main :: Effect Unit
+main = do
+  printAppend
+  printCons
+  printCompare
+
+--- Append ---
+
+combine :: forall @l @r both
+         . Symbol.Append l r both
+        => Reflect both String
+        => String
+combine = reflectTy @both
+
+prefix :: forall @string @suffix prefix
+        . Symbol.Append prefix suffix string
+       => Reflect prefix String
+       => String
+prefix = reflectTy @prefix
+
+suffix :: forall @string @prefix suffix
+        . Symbol.Append prefix suffix string
+       => Reflect suffix String
+       => String
+suffix = reflectTy @suffix
+
+printAppend :: Effect Unit
+printAppend = do
+    printHeader "Append"
+    printLine "combine: " $ combine @"apple" @"apple"
+    printLine "suffix:  " $ suffix @"apple" @"app"
+    printLine "prefix:  " $ prefix @"apple" @"le"
+
+--- Cons ---
+
+symbolHead :: forall @string head tail
+            . Symbol.Cons head tail string
+           => Reflect head String
+           => String
+symbolHead = reflectTy @head
+
+symbolTail :: forall @string head tail
+            . Symbol.Cons head tail string
+           => Reflect tail String
+           => String
+symbolTail = reflectTy @tail
+
+symbolCons :: forall @head @tail string
+            . Symbol.Cons head tail string
+           => Reflect string String
+           => String
+symbolCons = reflectTy @string
+
+printCons :: Effect Unit
+printCons = do
+  printHeader "Cons"
+  printLine "head: " $ symbolHead @"apple"
+  printLine "tail: " $ symbolTail @"apple"
+  printLine "cons: " $ symbolCons @"a" @"pple"
+
+--- Compare ---
+
+banana :: Proxy "banana"
+banana = Proxy
+
+symbolCompare :: forall @left @right ordering
+               . Symbol.Compare left right ordering
+              => Reflect ordering Ordering
+              => Ordering
+symbolCompare = reflectTy @ordering
+
+printCompare :: Effect Unit
+printCompare = do
+  printHeader "Compare"
+  printOrdering "EQ: " $ symbolCompare @"apple" @"apple"
+  printOrdering "LT: " $ symbolCompare @"apple" @"banana"
+  printOrdering "GT: " $ symbolCompare @"banana" @"apple"
+
+--- Reflectable ---
+
+printReflectable :: Effect Unit
+printReflectable = do
+  printHeader "Reflectable"
+  log $ "apple: " <> reflectTy @"apple"
+  log $ "banana: " <> reflectTy @"banana"
+
+-------------
+
+printHeader :: String -> Effect Unit
+printHeader s = log $ "=== " <> s <> " ==="
+
+printOrdering :: String -> Ordering -> Effect Unit
+printOrdering subhead ord = printLine subhead case ord of
+  LT -> "LT"
+  GT -> "GT"
+  EQ -> "EQ"
+
+printLine :: String -> String -> Effect Unit
+printLine s computation = log $ s <> computation
diff --git a/21-Hello-World/06-Type-Level-Programming/src/03-Integer-Example.purs b/21-Hello-World/06-Type-Level-Programming/src/03-Integer-Example/01-Proxy.purs
similarity index 98%
rename from 21-Hello-World/06-Type-Level-Programming/src/03-Integer-Example.purs
rename to 21-Hello-World/06-Type-Level-Programming/src/03-Integer-Example/01-Proxy.purs
index 003225149..ab987365c 100644
--- a/21-Hello-World/06-Type-Level-Programming/src/03-Integer-Example.purs
+++ b/21-Hello-World/06-Type-Level-Programming/src/03-Integer-Example/01-Proxy.purs
@@ -1,4 +1,4 @@
-module TLP.IntegerExample where
+module TLP.IntegerExample.Proxy where
 
 import Prelude
 import Data.Reflectable (class Reflectable, reflectType)
diff --git a/21-Hello-World/06-Type-Level-Programming/src/03-Integer-Example/02-VTAs.purs b/21-Hello-World/06-Type-Level-Programming/src/03-Integer-Example/02-VTAs.purs
new file mode 100644
index 000000000..8514a0f5b
--- /dev/null
+++ b/21-Hello-World/06-Type-Level-Programming/src/03-Integer-Example/02-VTAs.purs
@@ -0,0 +1,144 @@
+module TLP.IntegerExample.VTAs where
+
+import Prelude
+
+import Data.Reflectable (class Reflectable, reflectType)
+import Effect (Effect)
+import Effect.Console (log)
+import Prim.Int as Int
+import Type.Proxy (Proxy(..))
+
+-- Note: `Data.Reflectable` still uses Proxy arguments. 
+-- It should be defined as
+--   class Reflectable t v | t -> v where
+--     reflectType :: v
+--
+-- This will be fixed in the PureScript 0.16.0 ecosystem update.
+-- So for now, we'll define our own type class to show how things would work.
+
+class Reflect :: forall k. k -> Type -> Constraint
+class Reflect ty val | ty -> val where
+  reflectTy :: val
+
+instance (Reflectable ty val) => Reflect ty val where
+  reflectTy = reflectType (Proxy  :: Proxy ty)
+
+main :: Effect Unit
+main = do
+  printAddSubtract
+  printMul
+  printToString
+
+--- Add ---
+
+intAdd
+  :: forall @l @r sum
+   . Int.Add l r sum
+  => Reflect sum Int
+  => Int
+intAdd = reflectTy @sum
+
+intSubtract
+  :: forall @total @value answer
+   . Int.Add answer value total
+  => Reflect answer Int
+  => Int
+intSubtract = reflectTy @answer
+
+printAddSubtract :: Effect Unit
+printAddSubtract = do
+    printHeader "Add/Subtract"
+    printInt " 0 + 1: " $ intAdd @0 @1
+    printInt "-1 + 1: " $ intAdd @(-1) @1
+    printInt " 0 - 1: " $ intSubtract @0 @1
+
+--- Mul ---
+
+intMultiply
+  :: forall @l @r total
+   . Int.Mul l r total
+  => Reflect total Int
+  => Int
+intMultiply = reflectTy @total
+
+printMul :: Effect Unit
+printMul = do
+  printHeader "Mul"
+  printInt "1 * 1: " $ intMultiply @1 @1
+  printInt "2 * 1_000_000: " $ intMultiply @2 @1_000_000
+  printInt "3 * 2: " $ intMultiply @3 @2
+
+--- Compare ---
+
+intCompare
+  :: forall @l @r ord
+   . Int.Compare l r ord
+  => Reflect ord Ordering
+  => Ordering
+intCompare = reflectTy @ord
+
+printCompare :: Effect Unit
+printCompare = do
+  printHeader "Compare"
+  printOrdering "EQ: " $ intCompare @0 @0
+  printOrdering "LT: " $ intCompare @0 @1
+  printOrdering "GT: " $ intCompare @1 @0
+
+--- ToString ---
+
+toTLString
+  :: forall @i sym
+   . Int.ToString i sym
+  => Reflect sym String
+  => String
+toTLString = reflectTy @sym
+
+printToString :: Effect Unit
+printToString = do
+  printHeader "ToString"
+  printLine "       -1: " $ toTLString @(-1)
+  printLine "        0: " $ toTLString @0
+  printLine "        1: " $ toTLString @1
+  printLine "1,000,000: " $ toTLString @1_000_000
+
+--- Reflectable ---
+
+
+type MaxReflectableInt = 2147483647
+type MinReflectableInt = (-2147483648)
+
+printReflectable :: Effect Unit
+printReflectable = do
+  printHeader "Reflectable"
+  log $ "neg1: " <> (show $ reflectTy @(-1))
+  log $ "0: " <> (show $ reflectTy @0)
+  log $ "1: " <> (show $ reflectTy @1)
+  log $ "1,000,000: " <> (show $ reflectTy @1_000_000)
+  log ""
+  log $ "Type-Level Int values outside the JavaScript range for an integers "
+      <> " will not be solved by the compiler"
+  log $ "(max)  2147483647: " <> (show $ reflectTy @MaxReflectableInt)
+  log $ "(min) -2147483648: " <> (show $ reflectTy @MinReflectableInt)
+
+  -- These two examples will fail to compile since both values are outside the range of JavaScript integer.
+  -- log $ " 2147483648: " $ intAdd @MaxReflectableInt @1
+  -- log $ "-2147483649: " $ intSubtract @MaxReflectableInt @1
+
+  -- See `purescript-bigints` to reflect the integer to a BigInt as a workaround.
+
+-------------
+
+printHeader :: String -> Effect Unit
+printHeader s = log $ "=== " <> s <> " ==="
+
+printOrdering :: String -> Ordering -> Effect Unit
+printOrdering subhead ord = printLine subhead case ord of
+  LT -> "LT"
+  GT -> "GT"
+  EQ -> "EQ"
+
+printInt :: String -> Int -> Effect Unit
+printInt subhead int = printLine subhead $ show int
+
+printLine :: String -> String -> Effect Unit
+printLine s computation = log $ s <> computation
diff --git a/21-Hello-World/06-Type-Level-Programming/src/21-Row-Example.purs b/21-Hello-World/06-Type-Level-Programming/src/21-Row-Example/01-Proxy.purs
similarity index 98%
rename from 21-Hello-World/06-Type-Level-Programming/src/21-Row-Example.purs
rename to 21-Hello-World/06-Type-Level-Programming/src/21-Row-Example/01-Proxy.purs
index d5d8361df..266c41d5a 100644
--- a/21-Hello-World/06-Type-Level-Programming/src/21-Row-Example.purs
+++ b/21-Hello-World/06-Type-Level-Programming/src/21-Row-Example/01-Proxy.purs
@@ -1,4 +1,4 @@
-module TLP.RowExample where
+module TLP.RowExample.Proxy where
 
 import Prelude
 import Effect (Effect)
diff --git a/21-Hello-World/06-Type-Level-Programming/src/21-Row-Example/02-VTAs.purs b/21-Hello-World/06-Type-Level-Programming/src/21-Row-Example/02-VTAs.purs
new file mode 100644
index 000000000..85abc6496
--- /dev/null
+++ b/21-Hello-World/06-Type-Level-Programming/src/21-Row-Example/02-VTAs.purs
@@ -0,0 +1,46 @@
+module TLP.RowExample.VTAs where
+
+import Prelude
+import Effect (Effect)
+import Effect.Console (log)
+import Prim.Row (class Union, class Nub, class Cons)
+import Type.Proxy (Proxy(..))
+
+type First = (name :: String, age :: Int)
+type Second = (pets :: Array Pet)
+                                                                                          {-
+A function that can change what the outputted Record type must be
+based on the row type it receives.
+
+`g` does the following type-level computation:
+    - combine two rows using union
+    - add another field using cons (age :: Int)
+    - remove a duplicate field using Nub
+    - union the result with `(otherField :: String`)                                    -}
+g
+  :: forall a @row1 @row2 row1And2 row1And2PlusAge nubbedRow1And2PlusAge finalRow
+  . Union row1 row2 row1And2
+  => Cons "age" Int row1And2 row1And2PlusAge
+  => Nub row1And2PlusAge nubbedRow1And2PlusAge
+  => Union nubbedRow1And2PlusAge (otherField :: String) finalRow
+  => a
+  -> (a -> Record finalRow) 
+  -> Record finalRow
+g a function = function a
+
+main :: Effect Unit
+main = do
+  -- These examples show that the type of the returned record differs
+  -- depending on what the two rows we pass to `g` are
+  log $ show $ g @First @Second
+    5
+    (\five -> { age: five, name: "John", pets: [Pet], otherField: "other"})
+
+  log $ show $ g @First @(singlePet :: Pet) 5
+    (\five -> { age: five, name: "John", singlePet: Pet, otherField: "other"})
+
+-- needed to compile
+
+data Pet = Pet
+instance Show Pet where
+  show _ = "Pet"
diff --git a/21-Hello-World/06-Type-Level-Programming/src/22-RowList/01-Simple.purs b/21-Hello-World/06-Type-Level-Programming/src/22-RowList/01-Simple/01-Proxy.purs
similarity index 98%
rename from 21-Hello-World/06-Type-Level-Programming/src/22-RowList/01-Simple.purs
rename to 21-Hello-World/06-Type-Level-Programming/src/22-RowList/01-Simple/01-Proxy.purs
index 8d961e1ef..27b0a0ac5 100644
--- a/21-Hello-World/06-Type-Level-Programming/src/22-RowList/01-Simple.purs
+++ b/21-Hello-World/06-Type-Level-Programming/src/22-RowList/01-Simple/01-Proxy.purs
@@ -1,4 +1,5 @@
-module TLP.RowList.Simple where
+-- This is the same file as the next one but specified to use Proxy arguments.
+module TLP.RowList.Simple.Proxy where
 
 import Prelude
 
diff --git a/21-Hello-World/06-Type-Level-Programming/src/22-RowList/01-Simple/02-VTAs.purs b/21-Hello-World/06-Type-Level-Programming/src/22-RowList/01-Simple/02-VTAs.purs
new file mode 100644
index 000000000..38b9a1800
--- /dev/null
+++ b/21-Hello-World/06-Type-Level-Programming/src/22-RowList/01-Simple/02-VTAs.purs
@@ -0,0 +1,225 @@
+-- This is the same file as the next one but specified to use Visible Type Applications.
+module TLP.RowList.Simple.VTAs where
+
+import Prelude
+
+import Data.Array as Array
+import Data.List.Types (List(..))
+import Prim.RowList as RL
+import Data.Reflectable (class Reflectable, reflectType)
+import Type.Proxy (Proxy(..))
+
+                                                                              {-
+Let's say we want to produce a `Show` instance that
+only shows the keys of a record. Since a `Show` instance
+already exists for all Records, we'll need to define
+a newtype and its `Show` instance to achieve this desired behavior.                  -}
+
+newtype ShowKeysOnly :: Row Type -> Type
+newtype ShowKeysOnly r = ShowKeysOnly (Record r)
+                                                                              {-
+Once implemented, our code should work like this in the REPL:
+---
+> show $ ShowKeysOnly { a: 4, b: 6, c: "apple", z: false }
+["a", "b", "c", "z"]
+---
+
+How would we implement the `Show` instance for `ShowKeysOnly`?
+
+We implement it by defining another type class called `ShowKeysInRecord`
+that computes that information for all records, not just records wrapped
+in the `ShowKeysOnly`. Since this type class must work for all records,
+it cannot know anything about the record itself. This type class
+(and any other like it) will always use `RowList` to accomplish its goal.
+
+`RowList` is almost always used to implement anything that involves type
+classes and operating on the keys/values of any record that we know nothing of.
+A `RowList` functions like a type-level list but one that is specialized to
+work with row kinds.
+
+A `RowList` kind has two type-level values:
+- Nil (the base case)
+- Cons (the recursive case)
+
+At its most basic idea, it allows you to do a `Data.Foldable.foldl`-like
+computation on a record where the "next" element is the next key/field in
+that record.
+
+Let's remember what a fold-left looks like by using List.
+---
+data List a
+  = Nil
+  | Cons a (List a)
+---
+
+Read the below function as
+  Given
+    1. a function that takes the previous accumulated value and the next
+        element in the list and produces the next accumulated value
+    2. the initial accumulated value
+    3. a list of elements
+  Produce the final accumulated value                                           -}
+foldLeft
+  :: forall element accumulatedValue
+   . (accumulatedValue -> element -> accumulatedValue)
+  -> accumulatedValue
+  -> List element
+  -> accumulatedValue
+foldLeft _ finalAccumulatedValue Nil =
+  -- base case: we're done
+  finalAccumulatedValue
+foldLeft f initialOrNextAccumulatedValue (Cons nextElement restOfList) =
+  -- recursive case: do one step and continue
+  let
+    nextAccumulatedValue = f initialOrNextAccumulatedValue nextElement
+  in foldLeft f nextAccumulatedValue restOfList
+
+{-
+The first step we need to do is convert a row kind (i.e. the `r` in `{ | r }`
+or `Record r`) into a list-like structure, `RowList`. This is done by using
+the type class, `RL.RowToList`, a type-level function.
+
+Once we have a `RowList`, we can simulate a fold-left at the type-level
+by defining two instances, one for each value of `RowList`.
+1. The first instance corresponds to the `Nil` case above: it ends
+    the recursiong and returns the final version of the accumulated value.
+    Most of the time, this instance is very very boring.
+2. The second instance corresponds to the `Cons` case above: it computes
+    the next computation and adds it to the accumulated value and then
+    continues the recursion. Since this computes something using type-level
+    information, there are numerous other type class constraints that
+    enable such computations to occur at runtime.
+
+Great. Let's now show an example.
+
+We'll first define the `ShowKeysInRowList` type class. Since type classes
+infer what their types are based on runtime values, we need to include a
+`Proxy` runtime value in the type signature of `buildKeyList`. Otherwise,
+the compiler will hav eno idea which `rowList` we're referring to.           -}
+class ShowKeysInRowList :: RL.RowList Type -> Constraint
+class ShowKeysInRowList rowList where
+  buildKeyList :: List String
+
+-- As I said before, the base case is quite boring. It just ends the recursion.
+instance ShowKeysInRowList RL.Nil where
+  buildKeyList :: List String
+  buildKeyList = Nil
+
+{-
+The recursive case is more interesting. First, write the initial instance
+boilerplate:
+
+instance ShowKeysInRowList (RL.Cons sym k rest) where
+  buildKeyList :: List String
+  buildKeyList =
+
+Second, let's implement this instance. Since the type-level
+`RowList` is a `Cons`, our value-level `List` should also be a `Cons`
+
+instance ShowKeysInRowList (RL.Cons sym k rest) where
+  buildKeyList :: List String
+  buildKeyList = Cons key remainingKeys
+    where
+    key = ???
+    remainingKeys = ???
+
+Third, we'll compute what `key` should be. We know that a `Symbol`,
+a type-level `String`, can be converted into a value-level `String`
+via `reflectType` as defined by the `Reflectable` type class. So,
+let's add the `Reflectable` class as a constraint to expose `reflectType`
+and then use that function to produce our key:
+
+instance (Reflectable sym String) => ShowKeysInRowList (RL.Cons sym k rest) where
+  buildKeyList = Cons key remainingKeys
+    where
+      key = reflectType (Proxy :: Proxy sym)
+      remainingKeys = ???
+
+Fourth, we need to compute what the remaining keys are. Wait, isn't that
+what we're already doing? Let's use `buildKeyList` on the rest of the
+rows. Since `buildKeyList` is defined by `ShowKeysInRowList`, we need
+to add that constraint, so we can use that function:
+
+instance (Reflectable sym String, ShowKeysInRowList rest)
+  => ShowKeysInRowList (RL.Cons sym k rest) where
+  buildKeyList = Cons key remainingKeys
+    where
+      key = reflectType (Proxy :: Proxy sym)
+      remainingKeys = buildKeyList @rest
+
+And that's it! We've now defined our type class instance. You'll notice
+that the constraints get a bit long. So, the final version below
+will use indentation to make it easier to read (at least in my opinion):      -}
+
+instance 
+  ( Reflectable sym String
+  , ShowKeysInRowList rest
+  ) => ShowKeysInRowList (RL.Cons sym k rest) where
+  buildKeyList = Cons key remainingKeys
+    where
+      key = reflectType (Proxy :: Proxy sym)
+      remainingKeys = buildKeyList @rest
+
+-- Let's show all three parts together now for easier readability.
+-- We'll add a `2` so that the code still compiles:
+class ShowKeysInRowList2 :: RL.RowList Type -> Constraint
+class ShowKeysInRowList2 rowList where
+  buildKeyList2 :: List String
+
+instance ShowKeysInRowList2 RL.Nil where
+  buildKeyList2 :: List String
+  buildKeyList2 = Nil
+
+instance 
+  ( Reflectable sym String
+  , ShowKeysInRowList2 rest
+  ) => ShowKeysInRowList2 (RL.Cons sym k rest) where
+  buildKeyList2 = Cons key remainingKeys
+    where
+      -- this would be `reflectType @sym` but the type class
+      -- hasn't been updated yet as of this writing.
+      key = reflectType (Proxy :: Proxy sym)
+      remainingKeys = buildKeyList2 @rest
+
+{-
+To actually implement our `Show` instance, we'll add the constraints
+needed to compute these values
+-}
+instance (
+  -- 1. First convert the `recordRows` to a `RowList`
+  RL.RowToList recordRows rowList,
+  -- 2. Then bring `buildKeyList2` into scope
+  ShowKeysInRowList2 rowList
+  ) => Show (ShowKeysOnly recordRows) where
+  show (ShowKeysOnly _rec) =
+    -- 4. And convert the `List` into an `Array` and reuse the
+    --    Array's `show` to produce our desired result.
+    show $ Array.fromFoldable keyList
+    where
+    -- 3. Then build the key list
+    keyList = buildKeyList2 @rowList
+                                                                              {-
+Below are a few examples to prove that this works.
+Run the following in the REPL to confirm it for yourself:
+---
+spago repl
+example1
+example2
+---
+                                                                              -}
+example1 :: ShowKeysOnly ( a :: String, b :: Int, c :: Boolean )
+example1 = ShowKeysOnly { a: "", b: 0, c: false }
+
+example2 :: ShowKeysOnly ( rowlists :: String, are :: Int, cool :: Boolean )
+example2 = ShowKeysOnly { rowlists: "", are: 0, cool: false }
+
+{-
+Did you notice how the output of `example2` is unexpected?
+It prints
+  ["are","cool","rowlists"]
+rather than
+  ["rowlists","are","cool"]
+
+It seems like `RowToList` will sort the rows labels before returning them
+as a new list.
+-}
diff --git a/21-Hello-World/06-Type-Level-Programming/src/23-Example-Comparisons.md b/21-Hello-World/06-Type-Level-Programming/src/23-Example-Comparisons.md
new file mode 100644
index 000000000..0e5aa895f
--- /dev/null
+++ b/21-Hello-World/06-Type-Level-Programming/src/23-Example-Comparisons.md
@@ -0,0 +1,7 @@
+# Example Comparisons
+
+The examples in the preceding files demonstrated what using `Proxy` arguments are like and what using Visible Type Applications (VTAs) are like. Both can be used to achieve the same output of a given computation. The difference is in how.
+
+`Proxy` arguments are value-level arguments. So, one can define multiple functions, compose them together, and get a final result. VTAs, on the other hand, are not value-level arguments. So, all of the computation one wants to do is often put into the entire function or value where it's used.
+
+However, because `VTAs` aren't value-level arguments, it also means the type class dictionary overhead can be more easily optimized away. The same can't be said for `Proxy` arguments.
diff --git a/21-Hello-World/07-Testing/test/Readme.md b/21-Hello-World/07-Testing/test/Readme.md
index 196c5a973..c76633c0b 100644
--- a/21-Hello-World/07-Testing/test/Readme.md
+++ b/21-Hello-World/07-Testing/test/Readme.md
@@ -39,6 +39,8 @@ For more details, see these links:
 
 ## What is Property Testing and Why It Succeeds
 
+See [Testing the Hard Stuff and Staying Sane](https://www.youtube.com/watch?v=V8v-1PnFisU), a talk from one of the guys who wrote QuickCheck, a Haskell library used to do property testing.
+
 Property-testing verifies that a function (e.g. `reverse`) that receives **any** value of some data type (e.g. `String`) will output an expected value of the same/different data type; the expected value is calculated using the given input.
 
 One might immediately think of this code before realizing that it doesn't work:
@@ -87,6 +89,11 @@ Still, before deciding that one must use unit tests, consider using state machin
 - [Intro to state machine testing](http://qfpl.io/posts/intro-to-state-machine-testing-1/)
 - (haskell library) [An in-depth look at quickcheck-state-machine](http://www.well-typed.com/blog/2019/01/qsm-in-depth/)
 
+## Other Property Testing Links
+
+- [`falsify`](https://well-typed.com/blog/2023/04/falsify/) - a Haskell library that has not been ported to PureScript but has some interesting ideas
+- [How to Specify It! A Guide to Writing Properties of Pure Functions](https://research.chalmers.se/publication/517894/file/517894_Fulltext.pdf)
+
 ## Conclusion
 
 As much as possible, use Property Testing. When that does not suffice, consider state-machine testing. Otherwise, use unit testing.
diff --git a/31-Design-Patterns/38-Free-Boolean-Cube.md b/31-Design-Patterns/38-Free-Boolean-Cube.md
new file mode 100644
index 000000000..f91d42349
--- /dev/null
+++ b/31-Design-Patterns/38-Free-Boolean-Cube.md
@@ -0,0 +1,3 @@
+# The Free Boolean Cube
+
+See [The Free Boolean Cube](https://apotheca.io/articles/Free-Boolean-Cube.html).
\ No newline at end of file
diff --git a/31-Design-Patterns/41-GADTs.md b/31-Design-Patterns/41-GADTs.md
index 7329b23a3..a4189aa8d 100644
--- a/31-Design-Patterns/41-GADTs.md
+++ b/31-Design-Patterns/41-GADTs.md
@@ -5,3 +5,4 @@ GADTs or Generalized Algebraic Data Types have already been explained elsewhere:
 - [The Original Paper](https://www.cs.ox.ac.uk/files/3060/gadtless.pdf)
 - [The Purescript Approximation](http://code.slipthrough.net/2016/08/10/approximating-gadts-in-purescript/)
 - [PureScript GADTs Alternative - Recap](https://hgiasac.github.io/posts/2018-12-18-PureScript-GADTs-Alternatives---Recap.html)
+- [Defeating Return Type Polymorphism](https://philipphagenlocher.de/post/defeating-return-type-polymorphism/)
diff --git a/CHANGELOG.d/breaking_purs-update.md b/CHANGELOG.d/breaking_purs-update.md
new file mode 100644
index 000000000..6938f9b79
--- /dev/null
+++ b/CHANGELOG.d/breaking_purs-update.md
@@ -0,0 +1 @@
+* Update PureScript to v0.15.13
\ No newline at end of file
diff --git a/CHANGELOG.d/breaking_spago-update.md b/CHANGELOG.d/breaking_spago-update.md
new file mode 100644
index 000000000..81bbb86ec
--- /dev/null
+++ b/CHANGELOG.d/breaking_spago-update.md
@@ -0,0 +1 @@
+* Update Spago to 0.21.0
\ No newline at end of file
diff --git a/CHANGELOG.d/feature_falsify-and-other-links.md b/CHANGELOG.d/feature_falsify-and-other-links.md
new file mode 100644
index 000000000..e61190c3e
--- /dev/null
+++ b/CHANGELOG.d/feature_falsify-and-other-links.md
@@ -0,0 +1 @@
+* Link to `falsify` and other property-testing-related links
\ No newline at end of file
diff --git a/CHANGELOG.d/feature_fp-ts-migration-guide.md b/CHANGELOG.d/feature_fp-ts-migration-guide.md
new file mode 100644
index 000000000..890641de9
--- /dev/null
+++ b/CHANGELOG.d/feature_fp-ts-migration-guide.md
@@ -0,0 +1 @@
+* Link to `fp-ts`' migration guide from PS to TS
\ No newline at end of file
diff --git a/CHANGELOG.d/feature_link-boolean-cube.md b/CHANGELOG.d/feature_link-boolean-cube.md
new file mode 100644
index 000000000..fc12689af
--- /dev/null
+++ b/CHANGELOG.d/feature_link-boolean-cube.md
@@ -0,0 +1 @@
+* Link to Free Boolean Cube
\ No newline at end of file
diff --git a/CHANGELOG.d/feature_link-to-defeating-polymorphism.md b/CHANGELOG.d/feature_link-to-defeating-polymorphism.md
new file mode 100644
index 000000000..88404515f
--- /dev/null
+++ b/CHANGELOG.d/feature_link-to-defeating-polymorphism.md
@@ -0,0 +1 @@
+* Add link to GADTs: Defeating Return Type Polymorphism
\ No newline at end of file
diff --git a/CHANGELOG.d/feature_spago-codebase.md b/CHANGELOG.d/feature_spago-codebase.md
new file mode 100644
index 000000000..d17b33cc8
--- /dev/null
+++ b/CHANGELOG.d/feature_spago-codebase.md
@@ -0,0 +1 @@
+* Adds a table clarifying the difference `spago` Haskell and PureScript codebases
\ No newline at end of file
diff --git a/CHANGELOG.d/feature_vtas.md b/CHANGELOG.d/feature_vtas.md
new file mode 100644
index 000000000..6c3799f8d
--- /dev/null
+++ b/CHANGELOG.d/feature_vtas.md
@@ -0,0 +1,8 @@
+* Add an initial explanation for Visible Type Applications (VTAs)
+
+  This change affects the following folders:
+  - Basic Syntax
+  - Type-Level Syntax
+  - Hello World/Type-Level Programming
+
+  Reading through each is needed to get the full picture of VTAs.
diff --git a/CHANGELOG.d/fix_effect-monad.md b/CHANGELOG.d/fix_effect-monad.md
new file mode 100644
index 000000000..26d14221b
--- /dev/null
+++ b/CHANGELOG.d/fix_effect-monad.md
@@ -0,0 +1 @@
+* Fix erroneous Effect example
\ No newline at end of file
diff --git a/CHANGELOG.d/fix_monad-state.md b/CHANGELOG.d/fix_monad-state.md
new file mode 100644
index 000000000..bf80793f6
--- /dev/null
+++ b/CHANGELOG.d/fix_monad-state.md
@@ -0,0 +1 @@
+* Fix instantiation of `StateT`'s `MonadState` example
diff --git a/CHANGELOG.d/fix_update-build-tool-history.md b/CHANGELOG.d/fix_update-build-tool-history.md
new file mode 100644
index 000000000..7c346f1fb
--- /dev/null
+++ b/CHANGELOG.d/fix_update-build-tool-history.md
@@ -0,0 +1 @@
+* Miscellaneous tweaks to build tool history
\ No newline at end of file
diff --git a/Readme.md b/Readme.md
index 2f17c8667..03796c7e2 100644
--- a/Readme.md
+++ b/Readme.md
@@ -2,7 +2,7 @@
 
 This repo is my way of using the [Feynman Technique](https://medium.com/taking-note/learning-from-the-feynman-technique-5373014ad230) to learn Purescript and its ecosystem.
 
-All code uses PureScript `0.15.7`
+All code uses PureScript `0.15.13`
 
 To learn PureScript using this project:
 1. Git clone this repo