Skip to main content
165 votes

How should I read type system notation?

The notation used to describe type systems varies from presentation to presentation, so giving a comprehensive overview is impossible. However, most presentations share a large, common subset, so this ...
Alexis King's user avatar
  • 8,731
31 votes
Accepted

What are the pros and cons of having a unit type over C-like void?

In C, void is used in four and a half different ways. A unit type is equally good for one, worse for a second, better for two more, and totally unsuitable for the ...
Davislor's user avatar
  • 1,062
30 votes
Accepted

What does it mean that a language has an "effect system"?

I struggle to get the thing about "algebraic effect systems". What is it really about? Since you're not asking for a formal definition, but rather saying that you don't intuitively grasp ...
Eric Lippert's user avatar
  • 3,459
30 votes
Accepted

How are "strong" and "weak" typing defined?

The Wikipedia article, and the blog post, are correct that these terms are not well-defined and are not useful for communicating in general, and at best can be used in a relative way within a ...
Michael Homer's user avatar
  • 13k
28 votes

What optimizations does the strict aliasing rule facilitate?

The main thing the optimizer wants to know here is whether writes through one pointer might affect reads through other pointers or names. When it knows for sure that two pointers are unrelated in this ...
rpjohnst's user avatar
  • 824
22 votes

What are the pros and cons of having a unit type over C-like void?

An advantage of having a unit type instead of a void type is: unit is a regular type that ...
Eldritch Conundrum's user avatar
20 votes
Accepted

Do you need an "Any" type when implementing a statically typed programming language?

Any is commonly known as a Top type: a type that is a super-type of every type. Some strongly typed languages have quite restricted notions of sub-typing, so the concept of top type makes no sense ...
Mike Samuel's user avatar
20 votes

When do we need complex type inference?

It is true that, with a sufficiently simple type system, type inference is almost trivial. For example, writing a typechecker for the simply typed lambda calculus (STLC) is extraordinarily ...
Alexis King's user avatar
  • 8,731
19 votes

Are there any situations in which it would make sense to return a never type?

If you have a function f1() that returns Never, and you are writing a function f2() that ...
Eldritch Conundrum's user avatar
18 votes
Accepted

Are there disadvantages of including a never type?

The C standard specifies that infinite loops with no side-effects are undefined behaviour1, and LLVM follows this, so the LLVM optimiser sometimes "optimises away" such infinite loops (by ...
pxeger's user avatar
  • 848
17 votes

Are there any practical use cases for subtyping primitive types?

Yes. One application of subtyping is to produce an object that behaves the same way as another object, but records the operations performed on it. This recording can be used in a number of ways, e.g....
occipita's user avatar
  • 569
16 votes
Accepted

To what extent is type theory relevant to dynamically typed languages?

You are talking about type systems, not type theory I think it is worth drawing a distinction between type theory and the theory of type systems. Yes, this nomenclature is confusing, and yes, I ...
Alexis King's user avatar
  • 8,731
15 votes

What are the advantages/disadvantages of prefix type syntax?

Consider this line of C: foo(*bar); This could be: A declaration of a variable named bar, which is of type ...
Pseudonym's user avatar
  • 4,726
15 votes

Are there any situations in which it would make sense to return a never type?

The never type is often an un-inhabited type, i.e., a type that is not inhabited by any value. Therefore, there is no value you could return. For example, in Scala, ...
Jörg W Mittag's user avatar
13 votes

Do you need an "Any" type when implementing a statically typed programming language?

Any enables dynamic typing and type erasure in a statically-typed language. This turns out to be very useful, to the point where even Haskell and SML (languages ...
tarzh's user avatar
  • 3,924
13 votes

Are there any practical use cases for subtyping primitive types?

Refinement Types A Refinement Type is a subtype of some type, whose inhabitants can be described by a predicate. It looks like this: Even = { n ∈ ℤ | n mod 2 = 0 }. ...
Longinus's user avatar
  • 1,853
13 votes

Why can you implement a Monoid type in Java or C#, but not Monad or Functor?

You need higher-kinded types. A way to introduce a generic parameter, which is itself generic. Translating your Haskell example to Java-ish syntax, it might look something like this: ...
Fyodor Soikin's user avatar
12 votes

What are the advantages/disadvantages of prefix type syntax?

The main advantage is that the syntax is shorter ─ one less keyword function, and one less character of punctuation :. A ...
kaya3's user avatar
  • 19.7k
12 votes

Why don't many languages have integer range types?

The most popular reason is simply that having additional types is more work for the authors of compilers and libraries. Every feature starts with -100 points, and only gets implemented when there's a ...
dan04's user avatar
  • 1,959
11 votes

How can I infer the type of an empty literal?

As you said, "unknown" is a placeholder. It holds the place for a concrete type that has not yet been seen. When you see ["hello"] + [], you're ...
zdimension's user avatar
11 votes
Accepted

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

Sometimes kinds are a second universe level In languages with a strict separation between types and kinds, and where kinds themselves are not given sorts, it is possible to view them as equivalent to ...
Alexis King's user avatar
  • 8,731
11 votes

What are the advantages of having a set number of fixed sized integers versus defining the exact number of bits in every integer?

You need to distinguish between two meanings of “5-bit integer”: An integer which occupies 5 bits of storage, so that three of them will fit into a 16-bit word. An integer which can hold values ...
Martin Kochanski's user avatar
11 votes

When do we need complex type inference?

when do we actually need do type inference? One time when you need type inference is when the type is "unspeakable". In C# 3 we added anonymous types; there is no syntax for describing an ...
Eric Lippert's user avatar
  • 3,459
11 votes

Are there any practical use cases for subtyping primitive types?

User-defined subtypes of primitive types are a thorny issue, because primitive types have many operations which return new values of the primitive type. For example, if you add two of your ...
kaya3's user avatar
  • 19.7k
11 votes
Accepted

How can type systems be a useful formal framework for modeling things other than type-checking?

Formally speaking, type systems are defined as logical judgments. As described in my answer explaining the notation, inference rules are really just a fancy way of writing logical implication. This is ...
Alexis King's user avatar
  • 8,731
11 votes

To box or not to box? (how to determine if a value can be more efficiently passed by value or by reference)

I am not aware of any such compile-time algorithm, and I doubt an optimal one may exist. Calling convention One consideration that is missing from your table is calling convention. When compiling to ...
Matthieu M.'s user avatar
  • 3,038
10 votes

What design trade-offs led to the "Norway problem" in YAML, and when are they worthwhile?

It is a somewhat reasonable idea to provide convenient facilities for presumed common cases, but when done carelessly, it tends to backfire in unexpected situations. Javascript is notoriously plagued ...
abel1502's user avatar
  • 2,527
10 votes
Accepted

What are the advantages and disadvantages of making types as a first class value?

I think the way in which you represent types as values affects the kind of performance characteristics. Here are a few: Types as guard predicates A type is usable as a function that is called to ...
Mike Samuel's user avatar
10 votes

When do we need complex type inference?

The examples you give are correct, but do not convey the right message, I believe. The first ones, with integers, are way too simple for type inference to have any advantage. The last one, with ...
Jean-Armand Moroni's user avatar
10 votes
Accepted

Why does ATTAPL's linear product introduction rule not delete the objects from the context?

Technically, the linear lambda calculus presented in ATTAPL does not include a let construct, so your hypothetical “bad program” is not even syntactically ...
Alexis King's user avatar
  • 8,731

Only top scored, non community-wiki answers of a minimum length are eligible