I'd say every statically typed functional language is such. Why? There's a well-known relation between propositions and types, or more precisely between certain theories of logic and certain type theories going by the name of Curry--Howard correspondence. This relation has a less well-known cousin known as Curry--Howard--Lambek correspondence that extends it to categories. Thus, because every reasonable statically typed functional language is based on type theory, it has direct connection to category theory as well. You simply cannot escape it, try as you might. Bob Harper likes to call this The Holy Trinity -- categories, languages and logic.
The list of such languages follows: Haskell, ML, OCaml, Idris, Coq, Agda, etc.
Of course, you have to take all of this with a grain of salt. Safe for Coq and Agda -- both of which are foremost theorem provers -- these languages contain many industry-driven quirks that make them less susceptible to the formal reasoning mentioned in the first paragraph.
In a bit different direction, because type theory is so expressive (for example, it can replace set theory as foundations of mathematics), it's fairly straightforward to express many algebraic structures in it. All of the above languages use this feature profoundly, with e.g. monads in Haskell playing a very prominent role.