0

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 ?

  • 2
    Or use something that always does type inference. – Telastyn Nov 19 '14 at 21:23
  • 4
    haskell.org – Giorgio Nov 19 '14 at 21:30
  • 7
    A note on terminology: What you call a typesafe language is usually known as a language with a static type system. What you call typeless would correspond to inferred types, except that the latter implies a static type system while you seem to consider dynamically typed languages typeless too. In summary, you want a language that infers (or rather, can infer) all types. – user7043 Nov 19 '14 at 21:41
  • 1
    I should point out that there is at least one very good reason why you do not want this feature as much as you think you do: it can make compiler error messages an absolute pain to understand. The last time I did any work in a language that worked like this (an ML-like language called Miranda) I spent more time trying to understand compiler errors than I did writing code. – Jules Nov 20 '14 at 9:26
  • 1
    @Jules: The Scala community places an extremely high value on readable, understandable, helpful compiler error messages. So much so, that they actually refuse to add features to the language that would be very helpful, because they haven't yet figured out a way to implement them in such a way as to still provide good error messages. A more powerful type inference algorithm is one of those things: they have the math, they have the algorithm, they know how to implement in the compiler, they just don't know how to make it understandable where it goes wrong, when it does … so it's left out. – Jörg W Mittag Nov 20 '14 at 9:41
10

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

  • I'm fuzzy on this one: In what way is C not type safe by your definiton (always has defined behavior)? I thought C had defined behavior for pretty much everything in the type system (not necessarily GOOD behavior, just I though it was defined). – Michael Kohne Nov 20 '14 at 2:33
  • @MichaelKohne: The C language is full of undefined behavior. For one rather egregious example specifically related to the type system, what does the following function prototype mean: void foo(int* bar);? Is the parameter supposed to be an array of ints, or a pointer to a single int (because C doesn't support pass-by-reference so it has to be faked by using this idiom)? And what happens if it's expecting an array but you pass it a pointer to a single int? – Mason Wheeler Nov 20 '14 at 2:39
  • 1
    @MichaelKohne Anything undefined is what a PL theorist means by "goes wrong" or "gets stuck". In practice of course the program does something. It's just that what happens isn't predictable so it's bad. A well typed program in C can go wrong, so it isn't type safe. – jozefg Nov 20 '14 at 4:17
  • @MichaelKohne In C you can hide whatever you want in a void pointer and cast it to anything else. I don't think you can do worse at being not typesafe than allowing basically all type conversions in such a way... Sure, you can restrict C to disallow some things (and I believe this is somewhat what was tried with Ada), but then it's not C, it's a different language with a different type system. – Bakuriu Nov 20 '14 at 7:27
  • 1
    @Jules Actually that's not quite true, there's a fascinating type of type system called a linear type system which can ensure that each malloc matches one and only one free at compile time. Rust sports a version of such a type system – jozefg Nov 20 '14 at 16:20
6

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.

1

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.

  • 1
    Is Boo still under active development? To be sure, it's going to be easier to pick up than ML or Haskell for someone coming from Python, but if it's a dead project... – Charles Duffy Nov 20 '14 at 5:18
  • @CharlesDuffy: It's slow going at the moment, but there's currently an active effort under way to bring it up to a 1.0 release. – Mason Wheeler Nov 20 '14 at 5:33
0

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. enter image description here

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.