Lambda the Ultimate

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

The site math viewer is consistently crashing my iPad; it makes a note that it is trying to load something math.js for awhile before Safari just dies. Either this is an iOS issue, or an iOS + great firewall issue (if the font files aren't hosted locally, they are usually hosted by a blocked-in-china google).