|
|
|
|
|
|
by black_knight
2390 days ago
|
|
|
Some type systems have set theoretical semantics, but this does not usually correspond to the semantics of the program. For instance the type ∀ A. (A → A) → A would be empty in the set theoretical semantics, but in many programming languages there are terms of this type – the fixed point operator. A better framework for semantics of many programming languages is domain theory[0]. But it also has its limitations. The type system types the terms of the language. Thus it has to be intertwined with them. One of the purposes is to allow only well-typed terms, which then have a better understood semantics. [0]: https://en.wikipedia.org/wiki/Domain_theory |
|
|