Lambda the Ultimate

I'm seeking languages which implement following features:

1) Types are first class citizens and can be treated as ordinary values
2) Support of partial evaluation for symbolic computation

The idea I try to follow can be best described using a little example. Say you have typed variables x:even, y:odd which are not yet bound by values. One can state explicit type rules for an operation add like this:

add(x:even, y:even) -> even
add(x:odd, y:even) -> odd
...

and write down any kind of permutation of argument types.

But instead one might compute the types using a function:

type(x) = case mod(x,2) of
               1 -> odd
               0 -> even
          else
               `type(x)   --  returns unevaluated expression type(x)

with

mod(x+y,k:int) = mod(mod(x,k)+mod(y,k),k)  -- use pattern matching for decomposition
mod(x*y,k:int) = mod(mod(x,k)*mod(y,k),k)
mod(x:even,2) = 0
mod(x:odd,2)  = 1

Now one can compute z = x*x+y*y+3 and deal with z as a variable of known type and perform type guarded simplifications.

Maybe someone has a pointer where to find reading material ( or even language implementations ) that deal with related ideas?