Skip to main content

Questions tagged [type-theory]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
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,455
5 votes
1 answer
266 views

Is it possible to confirm that a pattern-matching statement is exhaustive when cases can be arbitrary predicates?

An algorithm to decide pattern match coverage can be complete by computing the complement for each case. For example: Nat The primitive constructors are ...
林子篆's user avatar
8 votes
1 answer
355 views

How, if at all, do kinds fit into the type universe hierarchy?

As I understand it, as a (value-level) function f that takes a value x of type T and returns ...
user570286's user avatar
5 votes
1 answer
213 views

How can we express type theory in a programming language?

Some would say type theory is fundamental to programming. A programming language implementation typically expresses a single type theory through its type system. Are there any specific features a ...
Bruce Adams's user avatar
  • 2,843
7 votes
5 answers
294 views

Why intersection types have more fields and union types have fewer fields?

There's a question that's been bothering me. I even implemented it backwards when I implemented the type system for my language. Why do intersection types have more fields and union types have fewer ...
Aster's user avatar
  • 3,218