Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

A few small improvements to the template tutorial #47

Merged
merged 1 commit into from
Sep 2, 2024
Merged

A few small improvements to the template tutorial #47

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions src/Explanation_Template_Polymorphism.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -209,7 +209,7 @@ About lazyT.
(* lazyT : Type@{lazyT.u0} -> Type@{max(Set,lazyT.u1+1)} *)

(** But it is required by the [lazy] function, which takes a [lazyT.u1], thus
structurally smaller than [lazyT] which lives at level [lazyT.u1+1]. *)
smaller than [lazyT] which lives at level [lazyT.u1+1]. *)
About lazy.
(* lazy : forall {A : Type@{lazyT.u1}}, (unit -> A) -> lazyT A *)

Expand Down Expand Up @@ -249,7 +249,7 @@ Print Universes Subgraph (lazyT.u1 uprod).
Because we've defined [lazy_pure_mprod], this is inconsistent with existing
constraints, so the definition doesn't typecheck! *)
Fail Definition mprod_lazy {A B: Type} (a: A) (b: B):
mprod (layzT A) (lazyT B) :=
mprod (lazyT A) (lazyT B) :=
mpair _ _ (lazy_pure a) (lazy_pure b).

(** This definition would have been accepted had we not defined
Expand All @@ -263,7 +263,7 @@ Fail Definition mprod_lazy {A B: Type} (a: A) (b: B):
(** *** Principle *)

(** Template universe polymorphism is a middle-ground between monomorphic
universes and proper polymorphic universes that allow for some degree of
universes and proper polymorphic universes that allows for some degree of
flexibility. We can see it mentioned in the description of [prod] from the
standard library; [About] says "[prod] is template universe polymorphic on
[prod.u0] [prod.u1]". This has no effect on the printed type, because it
Expand Down Expand Up @@ -320,7 +320,7 @@ Print Universes Subgraph (

(** *** Template polymorphism doesn't go through intermediate definitions *)

(** And thus, that's the problem solved... but only when the universe at fault
(** And thus, the problem is solved... but only when the universe at fault
comes from an inductive type directly (here, [prod]). Template polymorphic
universes don't propagate to any other derived definition. So if we define
the state monad for example, it will not itself be universe polymorphic at
Expand Down Expand Up @@ -353,7 +353,7 @@ Fail Definition state_lazy {S T: Type} (t: T): state S (lazyT T) :=

(** These limitations are rather annoying because constructions based on [prod]
are _everywhere_ in the standard library and in projects. The state monad is
just one in a million. It's also the same problem with [sum] many other
just one in a million. It's also the same problem with [sum] and many other
core types like [list]. *)
About sum.
About list.
Expand Down
Loading