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
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
               `type(x)   --  returns unevaluated expression type(x)


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

Select your preferred way to display the comments and click "Save settings" to activate your changes.


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?