PLQ #13Done on:   Tuesday, April 26th

Question 1 @ 2022-04-26 18:13

What should the type judgement for or look like, assuming we want the usual “Racket-like” semantics?


Question 2 @ 2022-04-26 18:16

Which of the following is true about the PICKY language?


Question 3 @ 2022-04-26 18:20

In one of our early Picky designs, we had a type system with an axiom for the types of functions:

Γ ⊢ {fun {x : τ₁} : τ₂ E} : (τ₁ -> τ₂)

According to this version of the language, is this

{fun {x : Number} : Number
  {call x 123}}

a valid expression?


Question 4 @ 2022-04-26 18:22

In one of our Picky language versions, we implemented typed recursion. Before extending Picky with recursion, what was different about the implementation?

For reference:

Γ[x:=τ₁] ⊢ E : τ₂  Γ[x:=τ₁] ⊢ V : τ₁
—————————————————————————————————————
    Γ ⊢ {rec {x : τ₁ V} E} : τ₂

Question 5 @ 2022-04-26 21:12

Should we have a PLQ?