Are there any statically-typed functional languages?

Question

I'm coming from a statically-typed background and investigating functional programming, but I'm not entirely excited about dynamic typing. I'm curious about what kind of options are out there.

One answer to start: ActionScript 3 is statically-typed and offers some functional paradigms, though AS3 programs don't often use them.

Limbic

Most "modern functional languages" are statically typed, with highly effective type inference. – Eskil

Answer 1

There are many. Haskell, OCaml and F# come to mind. If you are a Windows developer, F# is very nice and is well supported by Microsoft (along with a very strong StackOverflow community). Lisp family languages (Common Lisp, Scheme, Clojure) are examples of dynamic functional languages.

ActionScript 3 has optional static typing. The Haskell, OCaml and F# compilers, on the other hand, use type inference to deterministically infer types. When you first look at code written in OCaml the absence of explicit types gives it the clutter free look of a dynamically typed language with the type safety of static typing. It is my opinion that optional static typing for dynamic languages (a great idea) will eventually be replaced by type inference and that 10 years from now the static versus dynamic debate will be moot.

Alena

This comment has aged particularly well. – Gorki

F# is now officially supported on Linux and Mac. – Subtitle

Answer 2

My top recommendation for someone like you (presumably with a statically-typed, OO, imperative background) is Scala. Scala is an imperative-functional hybrid with better support for OO than Java and most other languages around. Scala compiles to JVM bytecode (.net is also supported, though used much less) and provides Java interoperability unmatched among non-Java JVM languages. I use Scala in my compiler - jgo and have found writing Scala code exceptionally fun and satisfying. The best resource for learning Scala is Programming in Scala, written by the language designer himself.

If you don't want a hybrid language and instead prefer to jump straight into the fray of FP, I'd go with Haskell. Haskell is a purely functional language; there's no (first-class) notion of mutability or effect. My favorite Haskell resource is the witty Learn You a Haskell for Great Good!. In fact, I'd heavily recommend reading some of LYAH whether or not you intend to go with Haskell, since it's a fantastic introduction to the world of statically typed FP. I'd start reading it even before thinking about language choice.

Purge

Answer 3

The type theory was first applied to the functional programming (typed lambda calculus), long before any imperative languages.

For the most advanced static type systems (you won't find anything comparable in the imperative world) check out Coq and Agda.

Molt

Actually, type theory comes from the same mathematical tradition that gave us the lambda calculus and the Turing machine, and predates programming languages. – Winegrower

@ibid, of course - I just would not separate functional programming from lambda calculus (and combinatory logic and alikes), and thus functional programming itself predates computing. – Molt

Well, type theory actually predates lambda calculus as well. The earliest instance I know is the type theory of Russell & Whitehead's Principia Mathematica (1910–1913); the Simple Type Theory, a precursor to typed lambda calculus, dates from the 1920s. See the Wikipedia entry. – Winegrower

Answer 4

haskell leaps to mind (although its type system is probably the most advanced out there), the ML family of languages, F# AFAIK.

Hoitytoity

Answer 5

Some statically typed languages with first-class lexical closures and guaranteed tail call elimination:

• Standard ML (1978-1997)
• Miranda (1983-1986)
• CAML (1985-1995)
• OCaml (1996-present)
• Haskell (1990-2010)
• F# (2005-present)

without tail call elimination:

• C# (1999-present)
• Scala (2008-present)

Pronunciation

@ericsoco: I don't think so. Those are just the last updates to the language that I could find quickly on the internet. – Pronunciation

@jon_harrop why did you specifically call out tail call elimination in your answer? – Limbic

@ericsoco: I personally don't regard languages without guaranteed TCO as functional languages because they cannot express basic functional idioms like continuation passing style robustly and efficiently. However, many people think Scala and C# are functional languages so I didn't want to exclude them entirely. – Pronunciation

@JonHarrop What is TCO? – Rodrique

@QiLuo: Tail call optimisation. – Pronunciation

I believe that the CLR has TCO, but I've been wrong before andI don't have a .NET environment set up. – Pacification

The CLR does have TCO but ONLY F# uses it and not C#. – Pronunciation

@JonHarrop In 2020, is it still true that Scala does not have tail call elimination? – Collocation

I believe so, yes. – Pronunciation

Scala has tail call optimization. – Ott

Answer 6

If you are familiar with the Java ecosystem, the very Haskell-like language Frege might be worth a look as it compiles to Java source code.

Audacity

As of Feb. 2021, Frege looks dead based on the lack of activity in its Github project. – Subtitle

Answer 7

Surprised to find that nobody has mentioned Kotlin here. Like scala, it is a statically typed multiparadigm language for the JVM with good support for functional programming. The standard library really encourages a functional style. Not only is Kotlin type safe, it is also null safe and has great type inference. It is also a bit simpler than scala (at the expense of features like macros) and has better Java interop.

Technically, you can do functional programming in Java, but the heavy syntax, lack of type inference and forced exception handling doesn't help you much.

Dunker