## Languages with first order types and partial evaluation

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


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?

## Comment viewing options

### Aldor

In the late 90s I worked (a little) on the Aldor language. It was originally developed as the scripting language for Axiom (a computer algebra system) but has since been released separately. It has both first-order types and partial evaluation. I don't know how actively it's being maintained these days, but if nothing else the documentation may still be of interest.

### Dependent Types in Aldor?

IIRC, an Aldor user can't use things like vector and vector interchangeably. Is that correct?