# 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?

• Γ ⊢ A : τ₁  Γ ⊢ B : τ₂
———————————————————————
Γ ⊢ {or A B} : (U τ₁ τ₂)
• Γ ⊢ A : Boolean  Γ ⊢ B : Boolean
————————————————————————————————
Γ ⊢ {or A B} : Boolean
• Γ ⊢ A : τ  Γ ⊢ B : τ
————————————————————
Γ ⊢ {or A B} : τ
• None of the above

## Question 2 @ 2022-04-26 18:16

Which of the following is true about the PICKY language?

• it is lazy
• it is strongly normalizing
• it’s type system is sound
• it is statically typed
• it is statically scoped
• it is auto-curried
• it has second-order functionals

## 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?

• Yes, because the output of the function is not properly type-checked

• Yes, because the body of the function is not properly type-checked

• No, because we implemented Racket’s type-checking rather than the Hindley-Milner system

• No, because the body of the function is not properly typed

• No, because the output of the function is not properly typed

## 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} : τ₂

• We want to have infinite loops in the language, in the previous version, programs always terminated

• We want to have strong normalization in the updated Picky language, the previous version was weakly normalized

• The halting problem existed in our previous implementation

• All the above

• None of the above

## Question 5 @ 2022-04-26 21:12

Should we have a PLQ?