tausigma.rkt (1729B)
1 #lang at-exp s-exp phc-thesis/scribblings/equations-lang 2 3 @; This file is NOT under the CC0 license, as it contains rules and definitions 4 @; copied with permission from Sam Tobin-Hochstadt's Ph.D thesis. I obtained the 5 @; permission to copy these rules, but did not ask for a relicensing under the 6 @; CC0 license. 7 8 @cases["τ,σ" #:first-sep "⩴" 9 @acase{⊤@tag*{top}} 10 @acase{@num-τ @tag*{number singleton}} 11 @acase{@Numberτ @tag*{any number}} 12 @acase{@true-τ @tag*{boolean singleton}} 13 @acase{@false-τ} 14 @acase{@symτ[@sym*] @tag*{symbol singleton}} 15 @acase{@Symbolτ @tag*{any symbol}} 16 @acase{@f→[(@repeated{τ}) R] @tag*{function}} 17 @acase{@f*[(@repeated{τ} τ) R] @tag*{variadic function}} 18 @acase{@f…[(@repeated{τ} @polydot[τ α]) R] 19 @tag*{variadic polymorphic function}} 20 @acase{@∀r[(@repeated{α}) τ]@tag*{polymorphic type}} 21 @acase{@∀r[(@repeated{α} @polydotα[α]) τ] 22 @tag*{variadic polymorphic type}} 23 @acase{α @P β@tag*{polymorphic type variable}} 24 @acase{@un[@repeatset{τ}]@tag*{union}} 25 @acase{@∩τ[@repeatset{τ}] @tag*{intersection}} 26 @acase{@consτ[τ τ]@tag*{pair}} 27 @acase{@null-τ @tag*{null (end of lists)}} 28 @acase{@List…τ[τ α] @tag*{variadic polymorphic list}} 29 @acase{@promiseτ[R] @tag*{promise}} 30 @acase{@recτ[r τ] @tag*{recursive type}}] 31 32 #:Boolean 33 34 @$${ 35 @=:def[@Booleanτ @un[@true-τ @false-τ]] 36 } 37 38 #:Listτ 39 40 @$${ 41 \begin{aligned} 42 @=:def[@Listτ[τ @repeated{σ}] @consτ[τ @Listτ[@repeated{σ}]]] \\ 43 @=:def[@Listτ[] @null-τ] 44 \end{aligned} 45 } 46 47 #:Listofτ 48 49 @$${ 50 @=:def[@Listofτ[τ] @recτ[r @un[@null-τ @consτ[τ r]]]] 51 }