Having worked professionally with Ada for decades, I can tell you quite unequivocally that it's not fun; not in the least. The only reason to learn Ada is if you want to work on huge projects with hundreds of other programmers for defense contractors.
I've never used Cobol but what little I know suggests that it may be even less fun than Ada.
If you want to bend your mind into new shapes, Prolog would be useful. You can do things with Prolog that are much more difficult than with other languages. Prolog lets you program using the backtracking paradigm, which is useful in solving some artificial intelligence problems.
If you want to learn functional programming, Lisp is often recommended, although I would probably suggest that the Racket dialect of Scheme is a better choice.
As far as the other languages go, Forth is usually used to program microcontrollers, Fortran for mathematics heavy applications, Erlang for multicore applications.
J is an interesting suggestion, but I think that it is best learned along with another more conventional functional language such as Scala or Erlang. J was really innovative back in the 1960s when it was called APL, but now it is a bit of a niche language although still highly useful for financial applications.
Don't expect the ability to create something useful in it though.
I started SICP, but followed along in Clojure, and I've been having a blast, plus my eyes are opening to a lot of things that I needed someone smart to tell me.
I don't have plans to ship Clojure in production, but it has still shaped what I'm doing on a daily basis in other languages.
CL molds itself to the paradigm and problem domain with no bias. It allows ultimate macro power even over other Lisp dialects.
There are efficient compilers. It's not tied to the JVM so you can deploy native, but there is a JVM alternative if you want it.
By “pure”, I mean lacking unaccounted side effects (including crashing and non-termination).
I take a rather strong view, as you can tell, of what it means to “support” pure functional programming. That is, I think it is insufficient to show that your code lacks appeals to falsehood and rampant non-termination. Because your code is linked with other code from other sources, it must be shown that appeals to falsehood and rampant non-termination are in fact _impossible_.
(By “rampant non-termination” and “appeals to falsehood”, I mean the use of circular reasoning. This is distinct from structural recursion and coinduction, which can be used to do REPLs and servers.)
So yes, Virginia, there is indeed a Pure Functional Programming. But you can't do it in Haskell.
True, but if you want to get as close to purity as possible whilst actually writing usable software Haskell is the answer. I'd love it if Agda was actually a fully fledged programming language, but currently it is not.
What I really want is a proper Epigram with OTT (or, be still my quaking heart, HoTT).
That would be cool.
Don't know anything about Epigram though. Dependent types is still firmly on my todo list.