programming language with type-level functions

Question

Is there any programming language out there that allows the same set of tools it offers, to be used at the type level as well? I know, Haskell and some other ML family languages allow parametric types but those are usually very limited and have a very adhoc syntax to define a new type.

To clarify, imagine the following pseudo code:

person = { name: 'jon', lastName: 'doe', age: 600 }
assoc = (k, v, obj) => 
   returns { name: 'jon', lastName: 'doe', age: 600, k: v }

assoc('color', 'red', person)
   // evaluates to { name: 'jon', lastName: 'doe', age: 600, color: 'red' }

So this is at the value-level. But I'm looking for a language that allows me to do the same thing at the type level:

type Person = { name: String, lastName: String, age: Int }
type Color = Red | Yellow

assoc = (k, v, type) => 
   returns a new type { name: String, lastName: String, age: Int, k: v }

assoc(color, Color, Person)
   // evaluates to { name: String, lastName: String, age: Int, color: Color }

You get the point, right? Basically, things that the PL allows you to do on values can be done on the types as well. It treats types as values, if you will.

Answer 1

Yes, and this is much, much more common than you may have thought. You can do meaningful (and actually Turing-complete!) type-level computation in C++ (see this post by Matt Might for example). Haskell allows type-level partial functions by way of type families, etc.

Of course, the system that fits your description best is probably dependent typing, which unify types and terms, i.e. there is no differentiation between type-level and value-level computation in a dependently-typed language. There are a myriad dependent type systems (Calculus of Constructions, Martin-Lof type theory, Zhaohui Luo's UTT, etc.), and also plenty of dependently-typed programming languages (Coq, Agda, Idris, you name it).

So, I doubt this question is anywhere near research-level. But the answer to your question is, yes, there are such languages, and a lot, and the theory of such languages is already fairly well-researched. For a reference on dependent types, you might want to consult Chapter 2 of Advanced Topics in Types and Programming Languages (ATTAPL), or Software Foundations by Benjamin Pierce et al., and Type-Driven Development with Idris by Edwin Brady if you're more inclined to work with code.