<p>Virtually every programming language employs types in some form or
other. Some languages use types only at run-time or only at compile-time,
but hybrids are also widespread.  Program specification and
verification often uses types. The fruitful connection between
programming languages and logic (Curry-Howard correspondence), which has led to technology transfer between both fields, is based on types. Many interesting
algorithmic questions arise from type-checking and type-inference.</p>

<p>All of the above are empirical evidence that types should be a core part of the study of programming languages.</p>

CC BY-SA 3.0
2015-02-16T12:52:45.350Z
2015-02-16T12:52:45.350Z
Martin Berger
<p>Why theoreticians consider 'types' as the core part of the programming languages? </p>

CC BY-SA 3.0
2015-02-13T07:03:27.213Z
I'm not sure about your background, so allow me to give two quick and simple reasons as a comment: (a) "data type" is a far better specified notion than "programming paradigm": you may raise all controversy you want with the latter, but you can already do math with the former; (b) types are ubiquitous and fundamental: the same data types are to be found in principle in all programming paradigms, while the other way around doesn't even make sense.
Basil
CC BY-SA 3.0
2015-02-13T07:11:19.817Z
(By the way, you might want to try this question in some other se forum.)
Basil
CC BY-SA 3.0
2015-02-16T11:47:01.583Z
@Basil To avoid any controversy I edited to a single and strait forward question.
o-0
CC BY-SA 3.0
2015-02-16T11:56:09.523Z
Okay, but to be honest I'm not even sure how "the core part" of pl should be construed (note the definite article!). Note that I didn't say that *your* question was controversial, just that it's often the case that people fight over ill-defined paradigms. You might want to read Harper's post [here](https://existentialtype.wordpress.com/2013/07/18/what-if-anything-is-a-declarative-language/), on declarative languages.
Basil
CC BY-SA 3.0
2015-02-16T22:11:07.013Z
I think this question is more suitable for [https://cs.stackexchange.com/](https://cs.stackexchange.com/).
Martin Berger
<type-theory>
Types as the Core of the Programming Languages
o-0
# Types as the Core of the Programming Languages

(Asked by: username_0 on 2015-02-12)

Why theoreticians consider 'types' as the core part of the programming languages?

**Tags:** type-theory

> **Comments:**
> **username_1**: I'm not sure about your background, so allow me to give two quick and simple reasons as a comment: (a) "data type" is a far better specified notion than "programming paradigm": you may raise all controversy you want with the latter, but you can already do math with the former; (b) types are ubiquitous and fundamental: the same data types are to be found in principle in all programming paradigms, while the other way around doesn't even make sense.  
> **username_1**: (By the way, you might want to try this question in some other se forum.)  
> **username_0**: @username_1 To avoid any controversy I edited to a single and strait forward question.  
> **username_1**: Okay, but to be honest I'm not even sure how "the core part" of pl should be construed (note the definite article!). Note that I didn't say that *your* question was controversial, just that it's often the case that people fight over ill-defined paradigms. You might want to read Harper's post [here](https://existentialtype.wordpress.com/2013/07/18/what-if-anything-is-a-declarative-language/), on declarative languages.  
> **username_2**: I think this question is more suitable for [https://cs.stackexchange.com/](https://cs.stackexchange.com/).  

---

## 1 answers

### Answer by username_2 on 2015-02-16. Score: 2

Virtually every programming language employs types in some form or
other. Some languages use types only at run-time or only at compile-time,
but hybrids are also widespread. Program specification and
verification often uses types. The fruitful connection between
programming languages and logic (Curry-Howard correspondence), which has led to technology transfer between both fields, is based on types. Many interesting
algorithmic questions arise from type-checking and type-inference.

All of the above are empirical evidence that types should be a core part of the study of programming languages.


---

