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?