type infered statically typed languages?

Question

are there any typeless typesafe languages? By typesafe I mean types are checked at compile time. By typeless I mean types are not declared.

I know this is easier than it sounds, maybe even impossible but for example if I had code like this

foo = {
   bar: 123;
}

In some imaginary language I can possibly know that bar is an int and foo is a struct/object/class with 1 int field.

Similarly if I do this

SomeFunc(v) {
  printInt(v.bar);
}

And elsewhere I do this

SomeFunc(foo);

All of that seems type checkable at compile time. With enough context it might even be type checkable across compilation units.

Are there any languages that have attempted this? Basically make it possible to rarely declare types and yet still be typesafe at compile time ?

Answer 1

Yes, pretty much everything in the Haskell/ML family does this. Here's a snippet of some relevant Haskell

 foo = 1 + bar
 bar = "Not a number :O"
 main = putStrLn foo

No types need to be explicitly annotated, but the error is still caught at compile time. In general we always infer some types in every language. Nothing would require something like

int bar = 1;
foo((bar : int) + (1 : int) : int) : string

Everyone supports at least inferring the types for subexpressions because otherwise the language is just unwritable. Usually the typechecker that the compiler runs will annotate the abstract syntax tree with these types. Only a few languages support global type inference, where we need write no types at all. There are some features which in general make complete type inference either difficult or impossible. An incomplete list

• Subtyping
• Polymorphism of rank 3 or higher
• Dependent types
• A completely monomorphic language (This is actually just ambiguous without some annotations)

PS I just wanted to make a note on terminology: type safe usually means that a well typed program always has defined behavior. Python is type safe and dynamically typed, C is not type safe and is statically typed.

I think what you want to say is a statically typed language that requires no type annotations :)

Answer 2

Type inference does exactly this. You do not generally have to declare types, as they can be inferred from usage. However, more complex type systems will still occasionally require explicit type annotations.

Your example can be written in Standard ML as

fun some_func {bar} = print (Int.toString bar);

val foo = {bar = 123};
some_func foo;

This uses pattern matching to obtain the bar field in the record passed to the some_func. The ML language pioneered type inference, but type inference is becoming a more common sight with various levels of support in Haskell, C++, C#, and Scala.

Answer 3

The answers so far have mentioned extreme functional languages. If you're looking for something a bit closer to the mainstream, have a look at Boo. Its syntax is heavily inspired by Python, but it's statically typed. Type declarations are required for defining class members, but for variables, method arguments and return types everything can be optionally given an explicit type, or type-inferenced if none is provided.

Answer 4

Maybe the least hard-core of the suggestions if FlowType (basically it is not a language, but a type annotation system for JavaScript). It is implemented using OCaml and has quite powerful type inference. I don't think a real task could be code based only on type inference, but in general FlowType can infer types for the most of cases.

You can play with it here.