Questions tagged [static-typing]
For questions relating to languages whose variables' data types are known at compile time, and type systems supporting this.
25 questions
6
votes
0
answers
135
views
What algorithms/approaches are known for type inference with subtyping (i.e. semiunification) of non-Turing-complete languages?
What are some options for integrating subtyping with Damas-Hindley-Milner inference? gets into this tangentially at the end of Jon Purdy's post ("Placing various restrictions on recursion (...
11
votes
1
answer
479
views
What's the current state of the art for inferring/checking integer range types?
I'm putting together a small language, and I'd like its type system to include bounded integer types, where for any expression e and integer literals $l,h$, the ...
6
votes
5
answers
3k
views
What is the term for types that are not type variables?
In a language, some types are actually type variables. I am aware of three kinds of type variables:
Generic Parameter Types: In the declaration of Foo<T>, ...
7
votes
2
answers
401
views
How do typing rules look if most types are user-defined?
Answer #2693 introduces the notation of typing rules. That answer shows typing rules for a simple language in which all types are primitive, i.e., built into the language. Other similarly beginner-...
- 303
7
votes
1
answer
217
views
Understanding the "operational" reading of typing judgements in PFPL by Robert Harper, Chapter 4 Statics
I'm reading Practical Foundations for Programming Languages by Robert Harper and am confused by the exercises in Chapter 4, "Statics", where he discusses a (monomorphic) type system.
The ...
- 232
1
vote
1
answer
951
views
Type-checking Python vs Typescript
mypy is very slow, pyright is fast but not quick enough in a large codebase, and tsc gives an immediate intellisense and type errors.
I do not know whether it is because Python has more complex type ...
- 113
15
votes
6
answers
5k
views
"Testing" that something does not compile in metaprogramming
Use case
Some languages offer techniques to ensure certain requirements at compile time. For example, rust has the NonZeroU32 type that will ensure at compile time ...
- 9,627
9
votes
1
answer
2k
views
Is Epic Games' Verse gradually typed?
I've just watched an interview on YouTube with Simon Peyton Jones where they talk about Epic's Verse language. Here (at roughly 51:30) they start talking about the type system.
Simon mentions that ...
- 193
11
votes
5
answers
1k
views
How to make logical operators that return operands consistent in a statically typed language?
In C++, 3 || 4 returns true. But in Python, 3 or 4 returns 3 instead. That's a logical operator that returns its operand. I don'...
- 3,314
21
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 ...
- 313
4
votes
2
answers
615
views
What are the possible variations of the type of "this" or "self"?
In the class definitions of an object oriented language, this refers to the object instance the code is about to work upon. Naturally, it should have the same type ...
- 3,314
8
votes
1
answer
587
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 ...
- 303
29
votes
6
answers
2k
views
Why don't many languages have integer range types?
An integer range type like 0..100 means that a value can be any integer in that range. Arithmetic operations on range types produce other range types, for example ...
- 22.4k
19
votes
2
answers
1k
views
What are some options for integrating subtyping with Damas-Hindley-Milner inference?
Type inference in a Damas-Hindley-Milner type system with subtyping is known to be undecidable in general.
What makes it so difficult? What options are there to get around undecidability which could ...
- 5,716
4
votes
1
answer
193
views
Supporting a statically-typed language in an IDE?
I'm almost finishing my open-source language's verifier. It performs parsing and verification, which ensures a set of programs are valid both syntatically and semantically at compile-time. To start ...
- 1,047