Skip to main content
Theoretical Computer Science

Return to Answer

added 311 characters in body
Source Link
xrq
xrq
  • 1.2k
  • 6
  • 17

Yes, and this is much, much more common than you may thinkhave thought. You can do meaningful (Turingand 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., etc.

Of course, the system that fits your description mostbest 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 close tonear 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.

Yes, and this is much, much more common than you may think. You can do (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., etc.

Of course, the system that fits your description most 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 close to 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.

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.

Source Link
xrq
xrq
  • 1.2k
  • 6
  • 17

Yes, and this is much, much more common than you may think. You can do (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., etc.

Of course, the system that fits your description most 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 close to 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.