Lambda the Ultimate

Hi,
I'm interested in languages which do compile time restrictions on the values of variables. Specifically, does anything like the following exist:

x : int [0, 2, ... 10]
x = 50 //error
x = 3 // error
x = 2 // ok

x = rand() // error, rand() : [0.0 ... 1.0] doesn't match [0, 2, ... 10]
x = floor(rand() * 2) * 2 // ok [0, 2, 4] is a subset of [0, 2, ...10]

Thanks,

Alex