commit f553454767c54d1bd7b2403158e050126cc19d19
parent 5492ca4eff506d6171c0c69b64f97ad313aa00e3
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Thu, 10 Aug 2017 17:41:22 +0200
Started on operational semantics
Diffstat:
9 files changed, 255 insertions(+), 89 deletions(-)
diff --git a/from-dissertation-tobin-hochstadt/operational-semantics.rkt b/from-dissertation-tobin-hochstadt/operational-semantics.rkt
@@ -0,0 +1,62 @@
+#lang at-exp s-exp phc-thesis/from-dissertation-tobin-hochstadt/lang-util
+
+@; This file is NOT under the CC0 license, as it contains rules and definitions
+@; copied with permission from Sam Tobin-Hochstadt's Ph.D thesis. I obtained the
+@; permission to copy these rules, but did not ask for a relicensing under the
+@; CC0 license.
+
+#:E-Delta
+
+@$inferrule[@${δ(c,v) = v'}
+ @${(c v) ↪ v'}
+ @${@textsc{E-Delta}}]
+
+#:E-Beta
+
+@$inferrule[-
+ @${@app[@λe[(@repeated{x:τ}) e_b] @repeated{e_a}]
+ ↪ e_b@subst[@repeated{x ↦ e_a}]}
+ @${@textsc{E-Beta}}]
+
+#:E-Beta*
+
+@$inferrule[-
+ @${
+ @app[@λe[(@repeated[#:n "n"]{x:τ} @${\ .\ } @${x_r:τ_r*}) e_b]
+ @repeated[#:n "n"]{e_a} @repeated[#:n "m"]{e_r}]
+ ↪ e_b@subst[x_r ↦ @listv[@repeated[#:n "m"]{e_r}]
+ @repeated[#:n "n"]{x ↦ e_a}]}
+ @${@textsc{E-Beta*}}]
+
+#:E-TBeta
+
+@$inferrule[-
+ @${@at[@Λe[(@repeated{α}) e] @repeated{τ}] ↪ e}
+ @${@textsc{E-TBeta}}]
+
+#:E-TDBeta
+
+@$inferrule[-
+ @${@at[@Λe[(@repeated{α} @polydotα[β]) e] @repeated{τ}] ↪ e}
+ @${@textsc{E-TDBeta}}]
+
+@λe[(@repeated{x:τ} @${\ .\ } @${x:τ*}) e]
+
+#:E-IfFalse
+
+@$inferrule[-
+ @${@ifop[@false-v e₂ e₃] ↪ e₃}
+ @${@textsc{E-IfFalse}}]
+
+#:E-IfTrue
+
+@$inferrule[-
+ @${@ifop[@false-v e₂ e₃] ↪ e₃}
+ @${@textsc{E-IfTrue}}]
+
+#:E-Context
+
+;; TODO: check what this means (and is it the right kind of arrow?)
+@$inferrule[@${L ↪ R}
+ @${E[L] → E[R]}
+ @${@textsc{E-Context}}]
+\ No newline at end of file
diff --git a/from-dissertation-tobin-hochstadt/phi-psi-o-path.rkt b/from-dissertation-tobin-hochstadt/phi-psi-o-path.rkt
@@ -13,9 +13,9 @@
@cases["ψ" #:first-sep "⩴"
@acase{τ_{π(@loc)}
- @tag*{@${(ℰ[v] = \mathbf{?}) ⇒ ℰ[π(@loc)]@text{ is of type @${τ}}}}}
+ @tag*{@${(v = \mathbf{?}) ⇒ π(@loc)@text{ is of type @${τ}}}}}
@acase{@!{τ}_{π(@loc)}
- @tag*{@${(ℰ[v] = \mathbf{?}) ⇒ ℰ[π(@loc)]@text{ is not of type @${τ}}}}}
+ @tag*{@${(v = \mathbf{?}) ⇒ π(@loc)@text{ is not of type @${τ}}}}}
@acase{⊥@tag*{contradiction}}]
#:loc
diff --git a/from-dissertation-tobin-hochstadt/rules.scrbl b/from-dissertation-tobin-hochstadt/rules.scrbl
@@ -97,22 +97,29 @@ following values:
@include-equation["v.rkt"]
-@subsubsub*section{Run-time environment}
-
-Lambda functions are closures over their execution environment. The execution
-environment maps to their value those variables which were within the scope of
-the closure. In principle, it also maps type variables and dotted type
-variables to the type or types used to instantiate the polymorphic functions
-which are part of the scope of the closure. Typed Racket uses @emph{type
- erasure} however, that is to say that the compile-time type of values does not
-persist at run-time. Primitive types are still implicitly tagged with their
-type (which allows for untagged unions and predicates such as
-@racket[number?]), but the type of a function cannot be determined at run-time
-for example. This means that the type-variable-to-type mapping of @${ℰ} is not
-effectively present at run-time with the current implementation of Typed
-Racket.
-
-@include-equation["envrt.rkt"]
+The @listv value notation is defined as a shorthand for a @|null-v|-terminated
+linked list of pairs.
+
+@include-equation["v.rkt" listv]
+
+@;{
+ @subsubsub*section{Run-time environment}
+
+ Lambda functions are closures over their execution environment. The execution
+ environment maps to their value those variables which were within the scope of
+ the closure. In principle, it also maps type variables and dotted type
+ variables to the type or types used to instantiate the polymorphic functions
+ which are part of the scope of the closure. Typed Racket uses @emph{type
+ erasure} however, that is to say that the compile-time type of values does not
+ persist at run-time. Primitive types are still implicitly tagged with their
+ type (which allows for untagged unions and predicates such as
+ @racket[number?]), but the type of a function cannot be determined at run-time
+ for example. This means that the type-variable-to-type mapping of @${ℰ} is not
+ effectively present at run-time with the current implementation of Typed
+ Racket.
+
+ @include-equation["envrt.rkt"]
+}
@subsubsub*section{Evaluation contexts}
@@ -191,11 +198,14 @@ allows recursive types to be described with the @recτ* combinator.
Additionally, the @Booleanτ type is defined as the union of the @true-τ and
@false-τ singleton types, and the @Listτ type operator is a shorthand for
-describing the type of heterogeneous linked lists of pairs, with a fixed
-length.
+describing the type of @|null-v|-terminated heterogeneous linked lists of
+pairs, with a fixed length. The @Listofτ type operator is a shorthand for
+describing the type of @|null-v|-terminated homogeneous linked lists of pairs,
+with an unspecified length.
@include-equation["tausigma.rkt" Boolean]
@include-equation["tausigma.rkt" Listτ]
+@include-equation["tausigma.rkt" Listofτ]
@subsubsub*section{Filters (value-dependent propositions)}
@@ -347,7 +357,25 @@ represent the type of the value assigned to a variadic polymorphic function's
@subsubsub*section{Operational semantics}
-@todo{TODO}
+For simplicity, we assume that promises only contain pure expressions, and
+therefore that the expression always produces the same value (modulo object
+identity, i.e. pointer equality issues). In practice, @typedracket allows
+expressions relying on external state, and caches the value obtained after
+forcing the promise for the first time. The subset of the language which we
+present here does not contain any mutable value, and does not allow mutation
+of variables either, so the expression wrapped by promises is, by definition,
+pure. We note here that we implemented a small library for @typedracket which
+allows the creation of promises encapsulating a pure expression, and whose
+result is not cached.
+
+@$p[@include-equation["operational-semantics.rkt" E-Delta]
+ @include-equation["operational-semantics.rkt" E-Beta]
+ @include-equation["operational-semantics.rkt" E-Beta*]
+ @include-equation["operational-semantics.rkt" E-TBeta]
+ @include-equation["operational-semantics.rkt" E-TDBeta]
+ @include-equation["operational-semantics.rkt" E-IfFalse]
+ @include-equation["operational-semantics.rkt" E-IfTrue]
+ @include-equation["operational-semantics.rkt" E-Context]]
@subsubsub*section{Type validity rules}
@@ -392,47 +420,37 @@ filters. @htodo{and objects}
@subsubsub*section{Typing rules}
-
-
-@include-equation["trules.rkt" T-Promise]
-@include-equation["trules.rkt" T-Symbol]
-@include-equation["trules.rkt" T-Gensym]
+The rules below relate the simple expressions to their type.
@htodo{Are the hypotheses for T-Eq? necessary? After all, in Racket eq? works
on Any.}
-@include-equation["trules.rkt" T-Eq?]
-@include-equation["trules.rkt" T-Var]
-@include-equation["trules.rkt" T-Primop]
-@include-equation["trules.rkt" T-True]
-@include-equation["trules.rkt" T-False]
-@include-equation["trules.rkt" T-Num]
-@include-equation["trules.rkt" T-Null]
-
-@htodo{The original TD-Map rule (p.95) seems wrong, as it allows un-dotted
- references to α in the function's type. But it is impossible to construct such
- a function, and the meaning of α in that case is unclear. I think the rule
- should instead expect a polymorphic function, with occurrences of α in τ_r
- replaced with the new β variable, as shown below.}
-
-@include-equation["trules.rkt" T-DMap]
+@$p[@include-equation["trules.rkt" T-Symbol]
+ @include-equation["trules.rkt" T-Gensym]
+ @include-equation["trules.rkt" T-Promise]
+ @include-equation["trules.rkt" T-Var]
+ @include-equation["trules.rkt" T-Primop]
+ @include-equation["trules.rkt" T-True]
+ @include-equation["trules.rkt" T-False]
+ @include-equation["trules.rkt" T-Num]
+ @include-equation["trules.rkt" T-Null]
+ @include-equation["trules.rkt" T-Eq?]]
Below are the rules for the various flavours of lambda functions and
polymorphic abstractions.
-@include-equation["trules.rkt" T-AbsPred]
-
@htodo{Technically, in the rules T-Abs and T-DAbs, we should keep any φ and o information concerning outer
variables (those not declared within the lambda, and therefore still available
after it finishes executing).}
-@include-equation["trules.rkt" T-Abs]
-@include-equation["trules.rkt" T-DAbs]
-
@todo{Should the φ⁺ φ⁻ o be preserved in T-TAbs and T-DTAbs?}
-@include-equation["trules.rkt" T-TAbs]
-@include-equation["trules.rkt" T-DTAbs]
+@$p[@include-equation["trules.rkt" T-AbsPred]
+ @include-equation["trules.rkt" T-Abs]
+ @include-equation["trules.rkt" T-Abs*]
+ @include-equation["trules.rkt" T-DAbs]
+ @include-equation["trules.rkt" T-TAbs]
+ @include-equation["trules.rkt" T-DTAbs]]
The @${\vphantom{φ}@substφo[x ↦ z]} operation restricts the information
contained within a @${φ} or @${o} so that the result only contains information
@@ -443,31 +461,69 @@ about the variable @${x}, and renames it to @${z}. When applied to a filter
The @${⊥} cases of the @${\operatorname{apo}} operator
from@~cite[#:precision "pp. 65,75" "tobin-hochstadt_typed_2010"] are covered
-by the corresponding cases in the @${@restrict} and @${@remove} operators, and
-therefore should not need to be included in our @${\vphantom{φ}@substφo[x ↦ z]}
-operator.
+by the corresponding cases in the @${@restrict} and @${@remove} operators
+defined below, and therefore should not need to be included in our @${
+ \vphantom{φ}@substφo[x ↦ z]} operator. The subst
@include-equation["trules.rkt" substφ]
@include-equation["trules.rkt" substo]
+@htodo{The definition of Γ' does not specify what the other cases ≠ x are
+ (they are the same as the original Γ, but this is only implicit).}
+
+The @racket[map] function can be called like any other function, but also has
+a specific rule allowing a more precise result type when mapping a polymorphic
+function over a @List…τ[τ α]. @racket[ormap], @racket[andmap] and
+@racket[apply] similarly have special rules for variadic polymorphic lists. We
+include the rule for @racket[map] below as an example. The other rules are
+present in @~cite[#:precision "pp. 96" "tobin-hochstadt_typed_2010"].
+
+@htodo{The original TD-Map rule (p.95) seems wrong, as it allows un-dotted
+ references to α in the function's type. But it is impossible to construct such
+ a function, and the meaning of α in that case is unclear. I think the rule
+ should instead expect a polymorphic function, with occurrences of α in τ_r
+ replaced with the new β variable, as shown below.}
+
+@include-equation["trules.rkt" T-DMap]
+
Below are the typing rules for the various flavours of function application and
instantiation of polymorphic abstractions.
-@include-equation["trules.rkt" T-App]
-
@todo{For the inst rules, are the φ⁺ φ⁻ o preserved?}
-@include-equation["trules.rkt" T-Inst]
-@include-equation["trules.rkt" T-DInst]
-@include-equation["trules.rkt" T-DInstD]
+@$p[@include-equation["trules.rkt" T-App]
+ @include-equation["trules.rkt" T-Inst]
+ @include-equation["trules.rkt" T-DInst]
+ @include-equation["trules.rkt" T-DInstD]]
+
+@;=====================TODO:write something vvvvvvvvvvvv
+
+The rule for @ifop uses the information gained in the condition to narrow the
+type of variables in the @emph{then} and @emph{else} branches. This is the
+core rule of the occurrence typing aspect of @|typedracket|.
+
@include-equation["trules.rkt" T-If]
-@htodo{The definition of Γ' does not specify what the other cases ≠ x are
- (they are the same as the original Γ, but this is only implicit).}
+The @${Γ + φ} operator narrows the type of variables in the environment using
+the information contained within @${φ}.
@include-equation["trules.rkt" Γ+]
+
+The @update operator propagates the information contained within a @${ψ} down
+to the affected part of the type.
+
@include-equation["trules.rkt" update]
+
+The @update operator can then apply @restrict to perform the intersection of
+the type indicated by the @|ifop|'s condition and the currently-known type for
+the subpart of the considered variable.
+
@include-equation["trules.rkt" restrict]
+
+The @update operator can also apply
+the @remove operator when the condition determined that the subpart of the
+considered variable is @emph{not} of a given type.
+
@include-equation["trules.rkt" remove]
@;{Shouldn't no-overlap be simplified to @${@no-overlap(τ, τ') = (@<:[σ τ]
@@ -478,17 +534,34 @@ instantiation of polymorphic abstractions.
@todo{Δ is not available here.}
@todo{The non-nested use of σ is not quite correct syntactically speaking}
+The @restrict operator and the @simplify* operator described later both rely
+on @no-overlap to determine whether two types have no intersection, aside from
+the @${⊥} type.
+
@include-equation["trules.rkt" no-overlap]
@htodo{Say that there are more rules in the implementation, to handle various
boolean operations.}
+The @combinefilter operator is used to combine the @${φ} information from the
+two branches of the @ifop expression, based on the @${φ} information of the
+condition. This allows @typedracket to correctly interpret @racket[and],
+@racket[or] as well as other boolean operations, which are implemented as
+macros translating down to nested @racket[if] conditionals. @Typedracket will
+therefore be able to determine that in the @emph{then} branch of
+@racket[(if (and (string? x) (number? y)) 'then 'else)], the type of
+@racketid[x] is @racket[String], and the type of @racketid[y] is
+@racket[Number]. We only detail a few cases of combinefilter here, a more
+complete description of the operator can be found
+in@~cite[#:precision "pp. 69,75–84" "tobin-hochstadt_typed_2010"].
+
@include-equation["trules.rkt" combinefilter]
@htodo{The Γ ⊢ x : τ … does not generate a Γ(x) = τ, I suspect. There should
be indicated somewhere an equivalence between these two notations (and we
should fix the @${Γ,x:update(…)}, as it is a third notation).}
+
@subsubsub*section{Simplification of intersections}
In some cases, intersections are simplified, and the eventual resulting @${⊥}
@@ -512,4 +585,7 @@ unions which contain @${⊥}, for the traversed parts of the type.
@subsubsub*section{δ-rules}
+Finally, the type and semantics of primitive functions are expressed using the
+δ-rules given below.
+
@include-equation["deltarules.rkt"]
diff --git a/from-dissertation-tobin-hochstadt/simplify.rkt b/from-dissertation-tobin-hochstadt/simplify.rkt
@@ -46,12 +46,12 @@
&= @promiseτ[@simplify[R]]\\
@simplify[@recτ[r τ]]
&= @recτ[r @simplify[τ]] \\
- @simplify[τ] &= τ \qquad @otherwise
+ @simplify[τ] &= τ \qquad @otherwise \\
@simplify[@R[τ φ⁺ φ⁻ o]] &= @R[@simplify[τ] @simplify[φ⁺] @simplify[φ⁻] o]\\
@simplify[@repeatset{ψ}] &= @repeatset{@simplify[ψ]}\\
@simplify[@${τ_{π(loc)}}] &= @simplify[τ]_{π(loc)}\\
@simplify[@${@!{τ}_{π(loc)}}] &= @!{@simplify[τ]}_{π(loc)}\\
- @simplify[⊥] = ⊥ \\
+ @simplify[⊥] = ⊥
\end{aligned}
}
diff --git a/from-dissertation-tobin-hochstadt/tausigma.rkt b/from-dissertation-tobin-hochstadt/tausigma.rkt
@@ -38,6 +38,14 @@
#:Listτ
@$${
- @=:def[@Listτ[τ @repeated{σ}] @consτ[τ @Listτ[@repeated{σ}]]]
+ \begin{aligned}
+ @=:def[@Listτ[τ @repeated{σ}] @consτ[τ @Listτ[@repeated{σ}]]] \\
@=:def[@Listτ[] @null-τ]
+ \end{aligned}
+}
+
+#:Listofτ
+
+@$${
+ @=:def[@Listofτ[τ] @recτ[r @un[@null-τ @consτ[τ r]]]]
}
\ No newline at end of file
diff --git a/from-dissertation-tobin-hochstadt/trules.rkt b/from-dissertation-tobin-hochstadt/trules.rkt
@@ -87,11 +87,11 @@
#:T-AbsPred
-@$inferrule[@${@Γ[@${x₀:σ₀} @repeated{xᵢ:σ} ⊢ e @R[τ φ⁺ φ⁻ o]] \\
+@$inferrule[@${@Γ[@${x₀:σ₀} @repeated{xᵢ:σᵢ} ⊢ e @R[τ φ⁺ φ⁻ o]] \\
φ⁺' = φ⁺\vphantom{φ}@substφo[x₀ ↦ •] \\
φ⁻' = φ⁻\vphantom{φ}@substφo[x₀ ↦ •] \\
o' = o\vphantom{o}@substφo[x₀ ↦ •]}
- @${@Γ[⊢ @λe[(@repeated{x:σ}) e]
+ @${@Γ[⊢ @λe[(x₀:σ₀ @repeated{xᵢ:σᵢ}) e]
@R[(f→ (@repeated{σ})
@R[τ
@${φ⁺'}
@@ -102,7 +102,7 @@
#:T-Abs
-@$inferrule[@${@Γ[⊢ e @R[τ φ⁺ φ⁻ o]]}
+@$inferrule[@${@Γ[@repeated{x:σ} ⊢ e @R[τ φ⁺ φ⁻ o]]}
@${@Γ[⊢ @λe[(@repeated{x:σ}) e]
@R[(f→ (@repeated{σ})
@R[τ
@@ -112,6 +112,18 @@
ϵ ⊥ ∅]]}
@${@textsc{T-Abs}}]
+#:T-Abs*
+
+@$inferrule[@${@Γ[@repeated{x:σ} @${x_r:@Listofτ[σ_r]} ⊢ e @R[τ φ⁺ φ⁻ o]]}
+ @${@Γ[⊢ @λe[(@repeated{x:σ} @${\ .\ } @${x_r:σ_r*}) e]
+ @R[(f→ (@repeated{σ})
+ @R[τ
+ ϵ
+ ϵ
+ ∅])
+ ϵ ⊥ ∅]]}
+ @${@textsc{T-Abs*}}]
+
#:T-DAbs
@$inferrule[@${@repeated{Δ ⊢ τₖ} \\
@@ -286,7 +298,7 @@
@aligned{
@remove(τ, σ) &= ⊥ &@textif @<:[τ σ] \\
- @remove((⋃ @repeatset{τ}), σ) &= (⋃ @repeatset{@remove(τ,σ)} &\\
+ @remove((⋃ @repeatset{τ}), σ) &= (⋃ @repeatset{@remove(τ,σ)}) &\\
@remove(τ, σ) &= τ &@otherwise
}
diff --git a/from-dissertation-tobin-hochstadt/v.rkt b/from-dissertation-tobin-hochstadt/v.rkt
@@ -10,16 +10,25 @@
@acase{@num-v @tag*{number}}
@acase{@true-v @tag*{booleans}}
@acase{@false-v}
- @acase{@λv[ℰ (@repeated{x:τ}) e] @tag*{lambda function}}
- @acase{@λv[ℰ (@repeated{x:τ} @${\ .\ } @${x:τ*}) e]
+ @acase{@λv[(@repeated{x:τ}) e] @tag*{lambda function}}
+ @acase{@λv[(@repeated{x:τ} @${\ .\ } @${x:τ*}) e]
@tag*{variadic function}}
- @acase{@λv[ℰ (@repeated{x:τ} @${\ .\ } @${x:@polydot[τ α]}) e]
+ @acase{@λv[(@repeated{x:τ} @${\ .\ } @${x:@polydot[τ α]}) e]
@tag*{variadic polymorphic function}}
- @acase{@Λv[ℰ (@repeated{α}) e]
+ @acase{@Λv[(@repeated{α}) e]
@tag*{polymorphic abstraction}}
- @acase{@Λv[ℰ (@repeated{α} @polydotα[α]) e]
+ @acase{@Λv[(@repeated{α} @polydotα[α]) e]
@tag*{variadic polymorphic abstraction}}
@acase{@consv[v v] @tag*{pair}}
@acase{@null-v @tag*{null}}
- @acase{@promisev[ℰ e] @tag*{promise}}
- @acase{@symv[@sym*] @tag*{symbol}}]
-\ No newline at end of file
+ @acase{@promisev[e] @tag*{promise}}
+ @acase{@symv[@sym*] @tag*{symbol}}]
+
+#:listv
+
+@$${
+ \begin{aligned}
+ @listv[v₀ @repeated{vᵢ}] &≝ @consv[v₀ @listv[@repeated{vᵢ}]] \\
+ @listv[] &≝ @null-v \\
+ \end{aligned}
+}
+\ No newline at end of file
diff --git a/scribblings/adt-row-shorthands.scrbl b/scribblings/adt-row-shorthands.scrbl
@@ -28,19 +28,15 @@ shorthand for the above lambda functions.
As per the typing rules given in @secref{adt-row-trules}, these functions have
the following types:
-@$${
- @$inferrule[
- @${@textsc{T-Abs}}
- @${Γ ⊢ @ctor[κ] : (∀ (α) (α → @ctor[κ α])) ; ϵ|⊥ ; ∅}
- ]
-}
+@htodo{The rules below are the same??? Probably an unfinished copy-paste}
-@$${
- @$inferrule[
- @${…}
- @${Γ ⊢ @ctor[κ] : (∀ (α) (α → @ctor[κ α])) ; ϵ|⊥ ; ∅}
- ]
-}
+@$inferrule[-
+ @${Γ ⊢ @ctor[κ] : (∀ (α) (α → @ctor[κ α])) ; ϵ|⊥ ; ∅}
+ @${@textsc{T-Abs}}]
+
+@$inferrule[-
+ @${Γ ⊢ @ctor[κ] : (∀ (α) (α → @ctor[κ α])) ; ϵ|⊥ ; ∅}
+ @${…}]
@todo{Write their types here too.}
diff --git a/scribblings/adt-utils.rkt b/scribblings/adt-utils.rkt
@@ -58,14 +58,14 @@
(define-syntax variant (defop "V"))
(define-syntax ifop (defop "if"))
(define-syntax mapop (defop "map"))
-(define-syntax-rule (λv env (arg ...) expr)
- @${[@(stringify env), λ(@(list (stringify arg) ...)).@(stringify expr)]})
+(define-syntax-rule (λv (arg ...) expr)
+ @${λ(@(list (stringify arg) ...)).@(stringify expr)})
(define-syntax-rule (λe (arg ...) expr)
@${λ(@(spaces (stringify arg) ...)).@(stringify expr)})
(define-syntax-rule (Λe (arg ...) expr)
@${Λ(@(spaces (stringify arg) ...)).@(stringify expr)})
-(define-syntax-rule (Λv env (arg ...) expr)
- @${[@(stringify env), Λ(@(spaces (stringify arg) ...)).@(stringify expr)]}) ;; TODO: is the env necessary here? It's a type env, right?
+(define-syntax-rule (Λv (arg ...) expr)
+ @${Λ(@(spaces (stringify arg) ...)).@(stringify expr)}) ;; TODO: is the env necessary here? It's a type env, right?
(define (repeated #:n [n #f] . l)
(if n
@${\overrightarrow{@l}\overset{\scriptscriptstyle\,\ifmathjax{\raise1mu{@|n|}}\iflatex{@|n|}}{\vphantom{@l}}}
@@ -165,6 +165,7 @@
(define-syntax consp (defop "cons"))
(define-syntax-rule (consv a b) @${⟨@(stringify a), @(stringify b)⟩})
+(define-syntax listv (defop "list"))
(define-syntax-rule (consτ a b) @${⟨@(stringify a), @(stringify b)⟩})
(define-syntax-rule (polydot τ α)
@${@(stringify τ) \mathbf{…}_{@(stringify α)}})
@@ -174,6 +175,7 @@
(define-syntax-rule (List…τ τ α)
@List…τ*[@polydot[τ α]])
(define-syntax Listτ (defop "List"))
+(define-syntax Listofτ (defop "Listof"))
@;(define-syntax →Values (defop "Values"))
(define-syntax-rule (→Values v ...) (spaces (stringify v) ...))
(define @emptypath @${ϵ})
