Type of system for programming language based on mathematical set theory

[elcaro]

TL;DR

Type systems in most programming languages are not very specific about the kind of values the type defines and miss the mathematical operations defined by mathematical set theory, like UNION, INTERSECTTION, MINUS. Is there a programming language which does have a type system that more or less conforms to mathematical set theory?

A type in a programming language more or less specifies what values are allowed for a given type. A type has some similarities with a set, but most programming languages lack the operations which a set has. For example, in C one can define a new type based on two other types as a union of those types with the union keyword, but there is no simple way to create a type based on the minus or interesction of two other types.
For languages like C++, one could define a class for such cases and define methods for defining such operations.

 

[PeterDonis]

most programming languages lack the operations which a set has

This is not correct. Most programming languages have set theoretic operations or equivalents. But most programming languages apply those operations to objects or values, not types. You are talking about applying those operations to types, which is a very different thing. I'm not aware of any programming language that treats types as sets and allows the full range of set theoretic operations on them.

 

[elcaro]

This is not correct. Most programming languages have set theoretic operations or equivalents. But most programming languages apply those operations to objects or values, not types. You are talking about applying those operations to types, which is a very different thing. I'm not aware of any programming language that treats types as sets and allows the full range of set theoretic operations on them.

Agree, my point was it is not part of the type system itself, you can't combine defined types into other types (apart from arrays, pointers, struct and union), and type specifications are rather unspecific, they are al based on a small set of basic types (like for example int with specifics only about the bit size and no restrictions on the values that the type defines, or what the value means and if they are comparable with other types that can contain the same value) and programming languages treat values that are based on the same base type as equal, while that in many cases is not true.

For example an error code with a value of 4 is distinct from an int value of 4 in an aritmethic operation, as arithmetic operations as +, -, * and / are not valid operations for for example error codes. In reality, the type for the error code and that for an artihmetic value - even when represented as the same base type = should not be the same type as it would compare apples with oranges or allow operations which are not valid for that type.

Only the type system of some program languages allow to make such distinctions (for example ADA).

It is debatable of course if these kind of abstractions are necessary within the type system of the language, or should be handled by the program itself, as such features are rather specific for the application domain, as it would make the language rather domain specific.

 

[PeterDonis]

you can't combine defined types into other types

You can in languages that allow multiple inheritance, like Python.

Only the type system of some program languages allow to make such distinctions

That's true, and it's probably a significant factor in people's choice of programming languages.

such features are rather specific for the application domain

Yes. And, as you say, that's why such things are often handled at the application level, not the programming language level.

 

[PeterDonis]

programming languages treat values that are based on the same base type as equal

Not necessarily. Plenty of languages let you define, for example, a type that has the same storage as a 32-bit integer, but is not type compatible with a 32-bit integer, so that the types cannot be used interchangeably.