A riddle regarding type safety
Of course, I have explained to the students in my language theory class what type safety means (remember: progress + preservation) and we have studied this notion time and again for some of the TAPL languages. However, I don't feel like the notion really sinked in universally. Some students consider all this semantics and calculus stuff as obscure and there is a certain critical mass of notation, when passed, concepts are not understood anymore (by some if not many of the Bachelor-level students in my class).
Last night, I came up with a nice "semantics riddle" for type safety:
What would be a super-trivial language with a type system and an SOS semantics such that type safety is violated?
I gave the students 2 minutes to think about the question.
I emphasized several times that the language should be super-trivial.
I also asked them for a general strategy for mis-designing a language to be type-unsafe.
One idea that popped up was to support some notion of cast.
We agreed that this would not be trivial, certainly not super-trivial.
Here is my reference solution:
Syntax of expressions
e ::= v | z
(Hence, there are expressions (forms) x, y and z.)
Values (normal forms)
v := x | y
Types
t ::= a | b
(a and b are the possible types.)
Small-step relation
z -> x
(Yes, we only have one axiom.)
Typing rules
x : a
y : b
z : b
(Yes, we have only axioms here.)
Demonstration of lack of type safety
The term z is the culprit.
z : b but z -> x and x : a
Regards,
Ralf
More trivial solutions are possible with unityping and a lack of progress instead of a lack of preservation. A very degenerate case is
ReplyDeleteterm syntax
e ::= x
types
t ::= a
typing
x : a
values
none
reduction
none
So we have neither a reduction semantics for x nor is x a value.
But maybe that's too trivial to be a language? ;-) I'll try again
term syntax
e ::= x | y | z
types
t :: = a
typing
x : a
y : a
z : a
values
v ::= y
reduction
x -> z
So x reduces to z which has no defined reduction yet isn't a value.