Answers to theory exercise 8.2

The given solution confuses the type joinhandle A with join tid

In 8.2b it states

Sigma(tid) = A
--------------
Sigma | Gamma |- tid : A

Which should be

Sigma(tid) = A
Sigma | Gamma |- tid : joinhandle A

In 8.2d it gives an configuration [joinhandle 1; joinhandle 0] By definition a configuration is a list of expressions. But joinhandle is a type. Correct would be [join 1; join 0]

For 8.2e, I would suggest to add that this is because we have no typing rule for tid's.

Note: we can now show that |- cfg [(lam x. join x) (spawn (join 0))] : A:

[A] | x : joinhandle A |- x : joinhandle A
[A] | x : joinhandle A |- join x : A
[A] |  |- (lam x. join x) : joinhandle A -> A
[A] |  |- 0 : joinhandle A
[A] |  |- join 0 : A
[A] |  |- spawn (join 0) : joinhandle A
[A] |  |- (lam x. join x) (spawn (join 0)) : A

Luckily it is not required that |- cfg [e] : A ==> |- e : A