diff --git a/lib/elixir/lib/module/types/descr.ex b/lib/elixir/lib/module/types/descr.ex
index 0bb0677ac7d..b03f26b4de7 100644
--- a/lib/elixir/lib/module/types/descr.ex
+++ b/lib/elixir/lib/module/types/descr.ex
@@ -347,6 +347,11 @@ defmodule Module.Types.Descr do
     left == right or (subtype?(left, right) and subtype?(right, left))
   end
 
+  @doc """
+  Check if two types are disjoint.
+  """
+  def disjoint?(left, right), do: empty?(intersection(left, right))
+
   @doc """
   Checks if a type is a compatible subtype of another.
 
@@ -761,9 +766,7 @@ defmodule Module.Types.Descr do
 
   defp map_only?(descr), do: empty?(Map.delete(descr, :map))
 
-  defp map_fetch_static(:term, _key) do
-    {true, term()}
-  end
+  defp map_fetch_static(:term, _key), do: {true, term()}
 
   defp map_fetch_static(descr, key) when is_atom(key) do
     case descr do
@@ -777,15 +780,113 @@ defmodule Module.Types.Descr do
         end
 
       %{map: map} ->
-        map_split_on_key(map, key)
-        |> Enum.reduce(none(), &union/2)
-        |> pop_optional_static()
+        map_get(map, key) |> pop_optional_static()
 
       %{} ->
         {false, none()}
     end
   end
 
+  @doc """
+  Updates the `key` with a given type, assuming that the key is present
+  in the descr, and that it is exclusively a map (or dynamic).
+  """
+  def map_update(:term, _key, _type), do: :badmap
+  def map_update(descr, key, :term), do: map_update_static_value(descr, key, :term)
+
+  def map_update(descr, key, type) do
+    case :maps.take(:dynamic, type) do
+      :error -> map_update_static_value(descr, key, type)
+      {dynamic, _static} -> dynamic(map_update_static_value(descr, key, dynamic))
+    end
+  end
+
+  def map_update_static_value(descr, key, type) do
+    case :maps.take(:dynamic, descr) do
+      :error ->
+        cond do
+          subtype?(descr, open_map([{key, term()}])) -> map_put_static(descr, key, type)
+          map_only?(descr) -> :badkey
+          true -> :badmap
+        end
+
+      {dynamic, static} when static == @none ->
+        if not disjoint?(dynamic, open_map([{key, term()}])) do
+          dynamic(map_put_static(dynamic, key, type))
+        else
+          :badkey
+        end
+
+      {dynamic, static} ->
+        if not disjoint?(dynamic, open_map([{key, term()}])) and
+             subtype?(static, open_map([{key, type}])) do
+          dynamic = map_put_static(dynamic, key, type)
+          static = map_put_static(static, key, type)
+          Map.put(static, :dynamic, dynamic)
+        else
+          if map_only?(static) do
+            :badkey
+          else
+            :badmap
+          end
+        end
+    end
+  end
+
+  @doc """
+  Adds a `key` of a given type, assuming that the descr is exclusively
+  a map (or dynamic).
+  """
+  def map_put(:term, _key, _type), do: :badmap
+  def map_put(descr, key, :term), do: map_put_static_value(descr, key, :term)
+
+  def map_put(descr, key, type) do
+    case :maps.take(:dynamic, type) do
+      :error -> map_put_static_value(descr, key, type)
+      {dynamic, _static} -> dynamic(map_put_static_value(descr, key, dynamic))
+    end
+  end
+
+  def map_put_static_value(descr, key, type) do
+    case :maps.take(:dynamic, descr) do
+      :error ->
+        if map_only?(descr) do
+          map_put_static(descr, key, type)
+        else
+          :badmap
+        end
+
+      {dynamic, static} when static == @none ->
+        if descr_key?(dynamic, :map) do
+          dynamic(map_put_static(dynamic, key, type))
+        else
+          :badmap
+        end
+
+      {dynamic, static} ->
+        if descr_key?(dynamic, :map) and map_only?(static) do
+          dynamic = map_put_static(dynamic, key, type)
+          static = map_put_static(static, key, type)
+          union(dynamic(dynamic), static)
+        else
+          :badmap
+        end
+    end
+  end
+
+  # Directly inserts a key of a given type into every positive and negative map
+  def map_put_static(descr, key, type) do
+    map_delete_static(descr, key)
+    |> Map.update!(:map, fn dnf ->
+      Enum.map(dnf, fn {tag, fields, negs} ->
+        {tag, Map.put(fields, key, type),
+         Enum.map(negs, fn {neg_tag, neg_fields} ->
+           {neg_tag, Map.put(neg_fields, key, type)}
+         end)}
+      end)
+    end)
+  end
+
   defp pop_optional_static(type) do
     case type do
       %{bitmap: @bit_optional} ->
@@ -846,7 +947,7 @@ defmodule Module.Types.Descr do
     {:closed, new_fields}
   end
 
-  # Open and closed: result is closed, all fields from open should be in closed
+  # Open and closed: result is closed, all fields from open should be in closed, except not_set ones.
   defp map_literal_intersection(:open, open, :closed, closed) do
     :maps.iterator(open) |> :maps.next() |> map_literal_intersection_loop(closed)
   end
@@ -864,7 +965,12 @@ defmodule Module.Types.Descr do
         :maps.next(iterator) |> map_literal_intersection_loop(acc)
 
       _ ->
-        throw(:empty)
+        # If the key is marked as not_set in the open map, we can ignore it.
+        if type1 == @not_set do
+          :maps.next(iterator) |> map_literal_intersection_loop(acc)
+        else
+          throw(:empty)
+        end
     end
   end
 
@@ -874,19 +980,33 @@ defmodule Module.Types.Descr do
   end
 
   defp map_difference(dnf1, dnf2) do
-    Enum.reduce(dnf2, dnf1, fn {tag2, fields2, negs2}, dnf1 ->
-      Enum.reduce(dnf1, [], fn {tag1, fields1, negs1}, acc ->
-        acc = [{tag1, fields1, [{tag2, fields2} | negs1]} | acc]
-
-        Enum.reduce(negs2, acc, fn {neg_tag2, neg_fields2}, acc ->
-          try do
-            {tag, fields} = map_literal_intersection(tag1, fields1, neg_tag2, neg_fields2)
-            [{tag, fields, negs1} | acc]
-          catch
-            :empty -> acc
+    Enum.reduce(dnf2, dnf1, fn
+      # Optimization: we are removing an open map with one field.
+      {:open, fields2, []}, dnf1 when map_size(fields2) == 1 ->
+        Enum.reduce(dnf1, [], fn {tag1, fields1, negs1}, acc ->
+          {key, value} = Enum.at(fields2, 0)
+          t_diff = difference(Map.get(fields1, key, tag_to_type(tag1)), value)
+
+          if empty?(t_diff) do
+            acc
+          else
+            [{tag1, Map.put(fields1, key, t_diff), negs1} | acc]
           end
         end)
-      end)
+
+      {tag2, fields2, negs2}, dnf1 ->
+        Enum.reduce(dnf1, [], fn {tag1, fields1, negs1}, acc ->
+          acc = [{tag1, fields1, [{tag2, fields2} | negs1]} | acc]
+
+          Enum.reduce(negs2, acc, fn {neg_tag2, neg_fields2}, acc ->
+            try do
+              {tag, fields} = map_literal_intersection(tag1, fields1, neg_tag2, neg_fields2)
+              [{tag, fields, negs1} | acc]
+            catch
+              :empty -> acc
+            end
+          end)
+        end)
     end)
     |> case do
       [] -> 0
@@ -894,6 +1014,71 @@ defmodule Module.Types.Descr do
     end
   end
 
+  @doc """
+  Removes a key from a map type.
+
+  ## Algorithm
+
+  1. Split the map type based on the presence of the key.
+  2. Take the second part of the split, which represents the union of all
+     record types where the key has been explicitly removed.
+  3. Intersect this with an open record type where the key is explicitly absent.
+     This step eliminates the key from open record types where it was implicitly present.
+  """
+  def map_delete(:term, _key), do: :badmap
+
+  def map_delete(descr, key) do
+    case :maps.take(:dynamic, descr) do
+      :error ->
+        # Note: the empty typ is not a valid input
+        if descr_key?(descr, :map) and map_only?(descr) do
+          map_delete_static(descr, key)
+          |> intersection(open_map([{key, not_set()}]))
+        else
+          :badmap
+        end
+
+      {dynamic, static} ->
+        if descr_key?(dynamic, :map) and map_only?(static) do
+          dynamic_result = map_delete_static(dynamic, key)
+          static_result = map_delete_static(static, key)
+
+          union(dynamic(dynamic_result), static_result)
+          |> intersection(open_map([{key, not_set()}]))
+        else
+          :badmap
+        end
+    end
+  end
+
+  # Takes a static map type and removes a key from it.
+  defp map_delete_static(%{map: dnf}, key) do
+    Enum.reduce(dnf, none(), fn
+      # Optimization: if there are no negatives, we can directly remove the key.
+      {tag, fields, []}, acc ->
+        union(acc, %{map: map_new(tag, :maps.remove(key, fields))})
+
+      {tag, fields, negs}, acc ->
+        {fst, snd} = map_pop_key(tag, fields, key)
+
+        union(
+          acc,
+          case map_split_negative(negs, key) do
+            :empty ->
+              none()
+
+            negative ->
+              negative |> pair_make_disjoint() |> pair_eliminate_negations_snd(fst, snd)
+          end
+        )
+    end)
+  end
+
+  defp map_delete_static(:term, key), do: open_map([{key, not_set()}])
+
+  # If there is no map part to this static type, there is nothing to delete.
+  defp map_delete_static(_type, _key), do: none()
+
   # Emptiness checking for maps.
   #
   # Short-circuits if it finds a non-empty map literal in the union.
@@ -948,27 +1133,28 @@ defmodule Module.Types.Descr do
        end)) or map_empty?(tag, fields, negs)
   end
 
-  # Takes a map dnf and a key and returns a list of unions of types
-  # for that key. It has to traverse both fields and negative entries.
-  defp map_split_on_key(dnf, key) do
-    Enum.flat_map(dnf, fn
+  # Takes a map dnf and returns the union of types it can take for a given key.
+  # If the key may be undefined, it will contain the `not_set()` type.
+  defp map_get(dnf, key) do
+    Enum.reduce(dnf, none(), fn
       # Optimization: if there are no negatives,
       # we can return the value directly.
-      {_tag, %{^key => value}, []} ->
-        [value]
+      {_tag, %{^key => value}, []}, acc ->
+        value |> union(acc)
 
       # Optimization: if there are no negatives
       # and the key does not exist, return the default one.
-      {tag, %{}, []} ->
-        [tag_to_type(tag)]
+      {tag, %{}, []}, acc ->
+        tag_to_type(tag) |> union(acc)
 
-      {tag, fields, negs} ->
+      {tag, fields, negs}, acc ->
         {fst, snd} = map_pop_key(tag, fields, key)
 
-        case map_split_negative(negs, key, []) do
-          :empty -> []
-          negative -> negative |> pair_make_disjoint() |> pair_eliminate_negations(fst, snd)
+        case map_split_negative(negs, key) do
+          :empty -> none()
+          negative -> negative |> pair_make_disjoint() |> pair_eliminate_negations_fst(fst, snd)
         end
+        |> union(acc)
     end)
   end
 
@@ -979,15 +1165,12 @@ defmodule Module.Types.Descr do
     end
   end
 
-  defp map_split_negative([], _key, neg_acc), do: neg_acc
-
-  defp map_split_negative([{tag, fields} | negative], key, neg_acc) do
-    # A negation with an open map means the whole thing is empty.
-    if tag == :open and fields == %{} do
-      :empty
-    else
-      map_split_negative(negative, key, [map_pop_key(tag, fields, key) | neg_acc])
-    end
+  defp map_split_negative(negs, key) do
+    Enum.reduce_while(negs, [], fn
+      # A negation with an open map means the whole thing is empty.
+      {:open, fields}, _acc when map_size(fields) == 0 -> {:halt, :empty}
+      {tag, fields}, neg_acc -> {:cont, [map_pop_key(tag, fields, key) | neg_acc]}
+    end)
   end
 
   # Use heuristics to normalize a map dnf for pretty printing.
@@ -1336,8 +1519,7 @@ defmodule Module.Types.Descr do
         {true, term()}
 
       %{tuple: tuple} ->
-        tuple_split_on_index(tuple, index)
-        |> Enum.reduce(none(), &union/2)
+        tuple_get(tuple, index)
         |> pop_optional_static()
 
       %{} ->
@@ -1345,18 +1527,20 @@ defmodule Module.Types.Descr do
     end
   end
 
-  defp tuple_split_on_index(dnf, index) do
-    Enum.flat_map(dnf, fn
-      {tag, elements, []} ->
-        [Enum.at(elements, index, tag_to_type(tag))]
+  defp tuple_get(dnf, index) do
+    Enum.reduce(dnf, none(), fn
+      # Optimization: if there are no negatives, just return the type at that index.
+      {tag, elements, []}, acc ->
+        Enum.at(elements, index, tag_to_type(tag)) |> union(acc)
 
-      {tag, elements, negs} ->
+      {tag, elements, negs}, acc ->
         {fst, snd} = tuple_pop_index(tag, elements, index)
 
         case tuple_split_negative(negs, index) do
-          :empty -> []
-          negative -> negative |> pair_make_disjoint() |> pair_eliminate_negations(fst, snd)
+          :empty -> none()
+          negative -> negative |> pair_make_disjoint() |> pair_eliminate_negations_fst(fst, snd)
         end
+        |> union(acc)
     end)
   end
 
@@ -1409,10 +1593,11 @@ defmodule Module.Types.Descr do
   #            or {t and not (union{i=1..n} t_i), s}
   #
   # This eliminates all top-level negations and produces a union of pairs that
-  # are disjoint on their first component.
-  defp pair_eliminate_negations(negative, t, s) do
+  # are disjoint on their first component. The function `pair_eliminate_negations_fst`
+  # is optimized to only keep the first component out of those pairs.
+  defp pair_eliminate_negations_fst(negative, t, s) do
     {pair_union, diff_of_t_i} =
-      Enum.reduce(negative, {[], t}, fn {t_i, s_i}, {accu, diff_of_t_i} ->
+      Enum.reduce(negative, {none(), t}, fn {t_i, s_i}, {accu, diff_of_t_i} ->
         i = intersection(t, t_i)
 
         if empty?(i) do
@@ -1423,11 +1608,39 @@ defmodule Module.Types.Descr do
 
           if empty?(s_diff),
             do: {accu, diff_of_t_i},
-            else: {[i | accu], diff_of_t_i}
+            else: {union(i, accu), diff_of_t_i}
+        end
+      end)
+
+    union(pair_union, diff_of_t_i)
+  end
+
+  # The formula above is symmetric with respect to the first and second components.
+  # Hence the following also holds true:
+  #
+  #    {t, s} and not (union<i=1..n> {t_i, s_i})
+  #           = union<i=1..n> {t and not t_i, s and s_i}
+  #            or {t, s and not (union{i=1..n} s_i)}
+  #
+  # which is used to in the following function, optimized to keep the second component.
+  defp pair_eliminate_negations_snd(negative, t, s) do
+    {pair_union, diff_of_s_i} =
+      Enum.reduce(negative, {none(), s}, fn {t_i, s_i}, {accu, diff_of_s_i} ->
+        i = intersection(s, s_i)
+
+        if empty?(i) do
+          {accu, diff_of_s_i}
+        else
+          diff_of_s_i = difference(diff_of_s_i, s_i)
+          t_diff = difference(t, t_i)
+
+          if empty?(t_diff),
+            do: {accu, diff_of_s_i},
+            else: {union(i, accu), diff_of_s_i}
         end
       end)
 
-    [diff_of_t_i | pair_union]
+    union(diff_of_s_i, pair_union)
   end
 
   # Makes a union of pairs into an equivalent union of disjoint pairs.
diff --git a/lib/elixir/test/elixir/module/types/descr_test.exs b/lib/elixir/test/elixir/module/types/descr_test.exs
index 86a2151d681..0af9e74fa2d 100644
--- a/lib/elixir/test/elixir/module/types/descr_test.exs
+++ b/lib/elixir/test/elixir/module/types/descr_test.exs
@@ -141,6 +141,9 @@ defmodule Module.Types.DescrTest do
                closed_map(a: integer())
              )
 
+      assert intersection(closed_map(a: integer()), open_map(b: not_set())) ==
+               closed_map(a: integer())
+
       assert equal?(
                intersection(closed_map(a: integer()), closed_map(a: if_set(integer()))),
                closed_map(a: integer())
@@ -563,6 +566,138 @@ defmodule Module.Types.DescrTest do
       assert union(dynamic(open_map(a: atom())), open_map(a: integer()))
              |> map_fetch(:a) == {false, union(dynamic(atom()), integer())}
     end
+
+    test "map_delete" do
+      assert map_delete(term(), :a) == :badmap
+      assert map_delete(integer(), :a) == :badmap
+      assert map_delete(union(open_map(), integer()), :a) == :badmap
+      assert map_delete(closed_map(a: integer(), b: atom()), :a) == closed_map(b: atom())
+      assert map_delete(empty_map(), :a) == empty_map()
+      assert map_delete(closed_map(a: if_set(integer()), b: atom()), :a) == closed_map(b: atom())
+
+      # Deleting a non-existent key
+      assert map_delete(closed_map(a: integer(), b: atom()), :c) ==
+               closed_map(a: integer(), b: atom())
+
+      # Deleting from an open map
+      assert map_delete(open_map(a: integer(), b: atom()), :a)
+             |> equal?(open_map(a: not_set(), b: atom()))
+
+      # Deleting from a union of maps
+      assert map_delete(union(closed_map(a: integer()), closed_map(b: atom())), :a)
+             |> equal?(union(empty_map(), closed_map(b: atom())))
+
+      # Deleting from a dynamic map
+      assert map_delete(dynamic(), :a) == dynamic(open_map(a: not_set()))
+
+      # Deleting from a gradual map
+      assert map_delete(union(dynamic(), closed_map(a: integer())), :a)
+             |> equal?(union(dynamic(open_map(a: not_set())), empty_map()))
+
+      assert map_delete(dynamic(open_map(a: not_set())), :b)
+             |> equal?(dynamic(open_map(a: not_set(), b: not_set())))
+
+      # Deleting from an intersection of maps
+      assert map_delete(intersection(open_map(a: integer()), open_map(b: atom())), :a) ==
+               open_map(a: not_set(), b: atom())
+
+      # Deleting from a difference of maps
+      assert difference(closed_map(a: integer(), b: atom()), closed_map(a: integer()))
+             |> map_delete(:b)
+             |> equal?(closed_map(a: integer()))
+
+      assert difference(open_map(), open_map(a: not_set()))
+             |> map_delete(:a) == open_map(a: not_set())
+    end
+  end
+
+  test "map_put" do
+    assert map_put(term(), :a, integer()) == :badmap
+    assert map_put(integer(), :a, integer()) == :badmap
+    assert map_put(dynamic(integer()), :a, atom()) == :badmap
+    assert map_put(union(integer(), dynamic()), :a, atom()) == :badmap
+    assert map_put(empty_map(), :a, integer()) == closed_map(a: integer())
+
+    # Replace an existing key in a closed map
+    assert map_put(closed_map(a: integer()), :a, atom()) == closed_map(a: atom())
+
+    # Add a new key to a closed map
+    assert map_put(closed_map(a: integer()), :b, atom()) == closed_map(a: integer(), b: atom())
+
+    # Replace an existing key in an open map
+    assert map_put(open_map(a: integer()), :a, atom()) == open_map(a: atom())
+
+    # Add a new key to an open map
+    assert map_put(open_map(a: integer()), :b, atom()) == open_map(a: integer(), b: atom())
+
+    # Put a key-value pair in a union of maps
+    assert union(closed_map(a: integer()), closed_map(b: atom()))
+           |> map_put(:c, boolean())
+           |> equal?(
+             union(closed_map(a: integer(), c: boolean()), closed_map(b: atom(), c: boolean()))
+           )
+
+    # Put a key-value pair in a dynamic map
+    assert map_put(dynamic(open_map()), :a, integer()) == dynamic(open_map(a: integer()))
+
+    # Put a key-value pair in an intersection of maps
+    assert intersection(open_map(a: integer()), open_map(b: atom()))
+           |> map_put(:c, boolean())
+           |> equal?(open_map(a: integer(), b: atom(), c: boolean()))
+
+    # Put a key-value pair in a difference of maps
+    assert difference(open_map(), closed_map(a: integer()))
+           |> map_put(:b, atom())
+           |> equal?(difference(open_map(b: atom()), closed_map(a: integer())))
+
+    # Put a new key-value pair with dynamic type
+    # Note: setting a field to a dynamic type makes the whole map become dynamic.
+    assert map_put(open_map(), :a, dynamic()) == dynamic(open_map(a: term()))
+
+    # Put a key-value pair in a map with optional fields
+    assert map_put(closed_map(a: if_set(integer())), :b, atom())
+           |> equal?(closed_map(a: if_set(integer()), b: atom()))
+
+    # Fetching on a key-value pair that was put to a given type returns {false, type}
+    {false, type} = union(dynamic(), empty_map()) |> map_put(:a, atom()) |> map_fetch(:a)
+    assert equal?(type, atom())
+  end
+
+  test "map_update" do
+    assert map_update(empty_map(), :a, term()) == :badkey
+    assert map_update(open_map(), :a, term()) == :badkey
+    assert map_update(term(), :a, term()) == :badmap
+    assert map_update(closed_map(a: integer()), :b, atom()) == :badkey
+    assert map_update(open_map(a: integer()), :b, float()) == :badkey
+    assert map_update(closed_map(a: if_set(integer())), :b, atom()) == :badkey
+    assert map_update(union(dynamic(), empty_map()), :a, atom()) == :badkey
+    assert map_update(closed_map(a: integer()), :a, atom()) == closed_map(a: atom())
+    assert map_update(open_map(a: integer()), :a, atom()) |> equal?(open_map(a: atom()))
+    assert map_update(dynamic(open_map()), :a, integer()) == dynamic(open_map(a: integer()))
+
+    assert closed_map(a: if_set(atom()), b: float())
+           |> union(open_map(a: atom()))
+           |> map_update(:a, integer()) ==
+             :badkey
+
+    assert closed_map(a: if_set(atom()), b: float())
+           |> union(open_map(a: atom()))
+           |> difference(open_map(a: if_set(float())))
+           |> map_update(:a, integer())
+           |> map_fetch(:a) == {false, integer()}
+
+    assert map_update(difference(open_map(), open_map(a: not_set())), :a, fun()) ==
+             open_map(a: fun())
+
+    # Update a key-value pair with dynamic type
+    # Note: setting a field to a dynamic type makes the whole map become dynamic.
+    assert map_update(open_map(a: atom()), :a, dynamic()) |> equal?(dynamic(open_map(a: term())))
+  end
+
+  describe "disjoint" do
+    test "map" do
+      refute disjoint?(open_map(), open_map(a: integer()))
+    end
   end
 
   describe "to_quoted" do