Questions tagged [type-systems]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
0 votes
2 answers
170 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 ...
Delfin's user avatar
  • 141
10 votes
1 answer
362 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-...
Aster's user avatar
  • 2,688
9 votes
1 answer
336 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 ...
blueberry's user avatar
  • 2,315
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 "...
blueberry's user avatar
  • 2,315
10 votes
1 answer
705 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 ...
kaya3's user avatar
  • 17.3k
11 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 ...
kaya3's user avatar
  • 17.3k
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 ...
Caleb Thomas's user avatar
141 votes
1 answer
46k 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’...
Alexis King's user avatar
  • 8,026
17 votes
4 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: ...
Bruce Adams's user avatar
  • 2,793
9 votes
6 answers
549 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: ...
Bruce Adams's user avatar
  • 2,793