<p>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 <a href="http://matt.might.net/articles/c++-template-meta-programming-with-lambda-calculus/" rel="nofollow noreferrer">this</a> post by Matt Might for example). Haskell allows type-level partial functions by way of type families, etc.</p>

<p>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).</p>

<p>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 <em>Advanced Topics in Types and Programming Languages</em> (ATTAPL), or <em>Software Foundations</em> by Benjamin Pierce et al., and <em>Type-Driven Development with Idris</em> by Edwin Brady if you're more inclined to work with code.</p>

CC BY-SA 3.0
2018-02-26T22:54:12.393Z
Thanks. This is very helpful. Didn't know `C++` templates can do such a thing.
Sam R.
CC BY-SA 3.0
2018-02-26T22:56:35.350Z
@norbertpy The Scala type system also allows for rich type-level computation and is also Turing complete. Also, look for GHC type system extensions; they allow an amazing (and jaw-dropping) amount of type-level computation in Haskell.
xrq
CC BY-SA 3.0
2018-02-26T22:43:53.210Z
2018-02-26T22:52:30.337Z
2018-02-26T22:52:30.337Z
xrq
<p>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.</p>

<p>To clarify, imagine the following pseudo code:</p>

<pre><code>person = { name: 'jon', lastName: 'doe', age: 600 }
assoc = (k, v, obj) =&gt; 
   returns { name: 'jon', lastName: 'doe', age: 600, k: v }

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

<p>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:</p>

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

assoc = (k, v, type) =&gt; 
   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 }
</code></pre>

<p>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.</p>

<pl.programming-languages><type-systems>
programming language with type-level functions
Sam R.
# programming language with type-level functions

(Asked by: username_0 on 2018-02-26)

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.

**Tags:** pl.programming-languages, type-systems


---

## 1 answers

### Answer by username_1 on 2018-02-26. Score: 5 | Accepted answer

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](http://matt.might.net/articles/c++-template-meta-programming-with-lambda-calculus/) 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.

> **Comments:**
> **username_0**: Thanks. This is very helpful. Didn't know `C++` templates can do such a thing.  
> **username_1**: @norbertpy The Scala type system also allows for rich type-level computation and is also Turing complete. Also, look for GHC type system extensions; they allow an amazing (and jaw-dropping) amount of type-level computation in Haskell.  

---

