Is there any object-oriented static typed language with variables with few types?

Question

I like reading about programming theories, so could you tell me if there is any object-oriented static typed language that allow variables to have a few types? Example in pesudocode:

var value: BigInteger | Double | Nil

I think about way of calling methods on this object. If object value have type BigInteger | Double language could allow user to call only shared methods (lake plus, minus) but when the type is BigInteger | Double | Nil then object of Nil hasn't methods plus and minus, so we can't do anything usefull with this object, because it has only few shared methods (like toString).

So is there any idea how should work calling methods on variable with few types in static typed object-oriented language?

Answer 1

It has not much to do with OO but (as far as I understand it) what you describe looks much like polymorphism as implemented by C++.

Answer 2

I'm not so sure if we really have a complete definition of what a static typed language is but I also hope that the language you describe wouldn't qualify as one.

One of my concerns is that if you add type T1 and T2 to be a part of your BigInteger | Double | Nil, how would they know about each other and how to handle the operations you defined? Now I realize you never said that the language would allow expanding the "implicit" conversion definition.

Come to think of it, C# does something that resembles this in its string handling

string s = -42 + '+' + "+" + -0.1 / -0.1 + "=" + (7 ^ 5) + 
  " is " + true + " and not " + AddressFamily.Unknown; 

=> "1+1=2 is True and not Unknown"

string str = 1 + 2 + "!=" + 1 + 2;

=> "3!=12"

And I do not like it.

Answer 3

I am not aware of any language that does this... sadly, I'd love to play around with it (but first, they should adopt type inference and parametric polymorphism ;) ).

Although it is alreapossible: Relatively elegantly in a structural type system (type a is a subtype of type b if a has everything b has), simply by specifying a type for value that is a structural subtype of BigInteger and of Double and of Nil and slightly less elegantly in a nominative type system (type a is a subtype of type b if and only if it inherits from it, directly or indirectly) by specifying a common ancestor of all three (if all else fails, object). Of course we'd need to go recursive - what is the type of toString? And what's the typ of (Integer | Double | BigInteger).+?!? This is far from trivial (in fact, looking for a solution made my head hurt a bit). I can't say if it is impossible, but no mainly-OO-language's type system is anywhere sophisticated enough for a possible solution.

The bottom line is: It'd be really cool if some whizz came along and sorted out the issues it raises. Propably not worth the effort...

Edit: Do you know algebraic data types? They are similar to your idea (but much older ;) ) in that an algebraic data type is composed of several types and can therefore contain e.g. a BigInteger, a Double and Nil - the actual value is one of these and a tag (as in tagged union) says which. But to use the value stored in an algebraic data type, you have to use pattern matching to extract it safely. This concept is very powerful, and still "simple" enough to be understood tools - e.g. type inference and static typechecking work.

Answer 4

What you are describing is an intersection type. They do exist in Java, for example, but they only arise within the type-checker as the result of capture conversion and type-inference. You cannot write one yourself.

I don't know of any language which uses them directly, but they are often used to describe or analyze type systems of languages, espececially languages which don't actually have a type system. For example, Diamondback Ruby, which is a static type system and type-inferencer for the dynamically typed Ruby programming language, uses both union and intersection types.

Note that the syntax you are using is generally used to denote union types, which are the dual of intersection types. Intersection types are generally written A & B & C.

Answer 5

Yes, OCaml has these in the form of polymorphic variants:

type my_var = Integer of int | Float of float;;
let x = Integer(10);;
let y = Float(3.14);;

Answer 6

Pike has them, as does Magpie, an optionally-typed language I'm working on. Google's Closure compiler for Javascript allows you to annotate types in Javascript using |.

They crop up frequently in languages that bridge static and dynamic typing because a lot of expressions in a dynamic language can yield one of a couple of types:

var a = 123;
if (foo) { a = "string"; }
bar(a);

The statically-determined type being passed to bar() is Number | String.