Questions tagged [type-systems]
The type-systems tag has no usage guidance.
11
questions
3
votes
2
answers
223
views
What programming languages exist which model the human beings using the application as language level constructs?
Most programming languages model the human beings using the system, as data like any other data. It is only through loose convention and framework level convention that things like authentication and ...
- 139
1
vote
2
answers
308
views
What is the mathematical abstraction of bitflags for use in a purely functional language?
A lot of C APIs like to have something called bit flags to signal the functions configuration options like Vulkan, OpenCL, SQLite and much more, it a typical pattern to it.
This common pattern of ...
- 159
12
votes
1
answer
760
views
What is the difference between GAT and HKT?
I implemented a basic generics-free, parameterless trait (type class) system. And I want to parameterize my trait system. The alternative paths I know of are Generic Associated Types (GAT) and Higher-...
- 3,238
9
votes
1
answer
345
views
Why does ATTAPL's linear product introduction rule not delete the objects from the context?
In Chapter 1 of Advanced Topics in Types and Programming Languages, the following rule is presented for the introduction of a product in a linear/unrestricted type system:
($\circ$ is context ...
- 2,587
30
votes
2
answers
8k
views
How expressive of a type system is too expressive, for the average programmer?
The advantages of an expressive type system cannot be denied. The usual definition applies - how much valid behaviour a chosen system allows, while also preventing invalid behaviour.
In terms of "...
- 2,587
10
votes
1
answer
739
views
Can type-checking algorithms be practically generated from formal descriptions of type systems?
It's well-known that a formal grammar (a formal description of a language's syntax) can be used to programmatically generate a parser (an algorithm which analyses that syntax); tools which do this are ...
- 20k
12
votes
4
answers
1k
views
How can type systems be a useful formal framework for modeling things other than type-checking?
Quoting one of Alexis King's answers:
Many programming language researchers would call many things “type systems” that programmers probably don’t think of as type systems. Many forms of static ...
- 20k
19
votes
4
answers
3k
views
To what extent is type theory relevant to dynamically typed languages?
There seem to be two conflicting views regarding the status of "type systems" used in dynamically typed languages:
That dynamically typed languages are actually just unityped static ...
- 193
145
votes
1
answer
47k
views
How should I read type system notation?
I sometimes read articles or papers about type systems that use some funny-looking, two-dimensional notation with lots of unfamiliar symbols and Greek letters. The notation seems mathematical, but it’...
- 9,156
18
votes
5
answers
3k
views
When do we need complex type inference?
Two of the most significant type inference schemes are Hindley-Milner and Bidirectional typing but when do we actually need do type inference?
The simple case is something like:
...
- 2,853
9
votes
6
answers
579
views
What is the 'type' (and correct name) of a member of an enumeration?
Consider a C style enum:
enum colour {
red,
blue,
green
};
In haskell this would be:
...
- 2,853