12/07/2011

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


1 comment:

  1. More trivial solutions are possible with unityping and a lack of progress instead of a lack of preservation. A very degenerate case is

    term 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.

    ReplyDelete