Is anyone familiar with a language that allows for "gradual instantiation". What I mean by this, is that the initial algorithm can be stated using very vague types (but not no type) that are gradually narrowed until they reach machine language level. For example, Number -> Rational -> Float -> IEEE_754. or CustomerData -> ShippingCustomer -> AmazonCustomer -> {name, address, [items]} -> { String, {String,String,String, Number}, [String] } ... and so on. A language that supports this would need a monotonically reducing type system with some way of checking types at each level and detecting conflicts. For example: Number = Number + Number is fine, but Rational = Number + Number, requires that the RHS needs to be Rational as well (but no resolution specification, yet).

## Comment viewing options

### Scala supports this

Scala supports this elegantly via type parameter refinement. You eventually have to specify concrete bindings for the type parameters, but you can write multiple layers that only have lower type bounds, and then combine them via trait composition. Basically:

trait BaseA {
type T <: Number
def foo(a : T, b : T): a + b
}

trait BaseB : BaseA {
refine type T <: Rational
}


And that's it really. It doesn't really help for efficiency, if that's what you are aiming at. In that case, templates sort of operate on this principle in the treatment of template parameters.

### Does Scala ever reach machine language level?

JVM languages need marshalling to integrate with 'C', so I'm not sure if I would say they go all the way down to machine level. I would be looking for something with byte, word, float and double support, that has plain-old-data-structures with precise memory layouts like 'C' arrays and structs (and unions), and control of addressing that could be used to directly program hardware if talking about machine language.

I'm not sure about the gradual instantiation though. I would have thought the high level types would need to be precisely defined too. Number still needs precise semantics to be useful, Customer is just an 'object' with properties like name, address etc.

### Scala with Delite

The Stanford Delite Project, allows you to compile an embedded DSL in Scala down to the machined level, but that's not quite the same thing. There definitely need to be precise semantics at each level, but the higher levels can be more mathematical/human oriented without the limitations of actual machine code.