Questions tagged [type-checking]

verifying that a variable, expression or value has the declared type

Filter by
Sorted by
Tagged with
0
votes
0answers
52 views

Consistency of a set of bidirectional typing rules

Main Is there any way to algorithmically check the consistency of a set of bidirectional typing rules, e.g. the absence of cycles and the uniqueness of the derivation tree? This problem is naturally ...
0
votes
2answers
55 views

What is the single type in a dynamic typing language?

Regarding static typing and dynamic typing, Practical Foundation of Programming Languages by Harper says: There have been many attempts by advocates of dynamic typing to distinguish dynamic from ...
2
votes
1answer
47 views

Do dynamic/static languages associate types or classes to values or variables?

In Practical Foundation of Programming Languages by Harper There have been many attempts by advocates of dynamic typing to distinguish dynamic from static languages. It is useful to consider ...
0
votes
1answer
39 views

Doubts on the behavior of Unit Type in a type system

I have a doubt about the Unit Type in the context of Type Theory and its use in different case scenarios. To start with, a Unit Type can be seen as a nullary Product Type, namely Unit, with one only ...
5
votes
2answers
577 views

Does the underlying computational calculus in type theories affect decidability?

I'm looking for a high-level explanation although if that isn't possible or difficult, I'd prefer references to books/papers. I understand that modern type theory is inspired by Curry-Howard ...
2
votes
2answers
53 views

What is the differences and similarities between refinement type and liquid types?

Looking at the examples here and here both refinement type and liquid types look very similar. What are the differences and similarities?
0
votes
2answers
139 views

Is type-checking “syntactic” or “semantic”?

On the wikipedia page on compilers, it says: Semantic analysis adds semantic information to the parse tree and builds the symbol table. This phase performs semantic checks such as type checking (...
1
vote
1answer
47 views

Dynamic testing of down casts as explained in TAPL

On page 195 of Pierce's TAPL book, he states that one can replace a down-cast operator by some sort of dynamic type test. Then he gives the following rules: T-Typetest: $\dfrac{\Gamma \vdash t_1:S \;...
8
votes
3answers
255 views

Are assembly languages untyped?

I'm writing my Bsc thesis about type systems of various languages and I want to have a short section about assembly languages. Initially I thought I'll bring up assembly as a counter example to ...
3
votes
0answers
26 views

What the type of an overloaded function should be?

Anecdotally, Virgill III language forbids overloading since overloading resolution is at odds with the language support of functions as first-class citizen, when resolution can't happen at compile ...
2
votes
0answers
75 views

How could 'Complete and Easy Bidirectional Type Checking' handle invariant parameters on type constructors

The paper Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism provides examples for checking if one function type is a subtype of another, which I think demonstrates checking ...
2
votes
2answers
46 views

Are type variables really only used in mathematical conversation about types?

Are type variables really only used in mathematical conversation about types? i.e. are type variables (meta-variables that only contain the type classification label) only exist in proofs for types ...
1
vote
1answer
112 views

What is the difference between $ \alpha \to \alpha $ vs $ \forall \alpha. \alpha \to \alpha$?

I was studying polymorphic types and I was finding the distinction with monomorphic types difficult to pin down (context CS 421). From the course I linked the have the following (vague attempt) at a ...
5
votes
1answer
88 views

What does $ \forall \alpha_1, \dots , \alpha_n . \tau $ mean formally as a type?

I was learning about polymorphic types but I couldn't understand the notation, can someone explain it means (context cs421 UIUC): $$ \forall \alpha_1, \dots , \alpha_n . \tau $$ its supposed to be a ...
9
votes
1answer
1k views

Why does Coq include let-expressions in its core language

Coq includes let-expressions in its core language. We can translate let-expressions to applications like this: let x : t = v in b ~> (\(x:t). b) v I understand ...
8
votes
1answer
503 views

Representation of the concatenation at the type level

I would like to learn more about concatenative programming through the creation of a small simple language, based on the stack and following the concatenative paradigm. Unfortunately, I haven't found ...
2
votes
0answers
41 views

Real world example of contraction and weakening

Can you provide me a real world example of contraction and weakening in the type system of a popular language like Java, Kotlin, etc.? I heard that Rust has got explicit contraction but I don´t ...
3
votes
0answers
142 views

Type inference for System F-omega

There have been some nice papers about simple type inference for System F: "HMF: Simple Type Inference for First-Class Polymorphism", "Practical type inference for arbitrary-rank types", and "Complete ...
12
votes
5answers
1k views

Is there any use case for the bottom type as a function parameter type?

If a function has return type of ⊥ (bottom type), that means it never returns. It can for example exit or throw, both fairly ordinary situations. Presumably if a function had a parameter of type ⊥ it ...
1
vote
1answer
48 views

Add type checking/inference to my programming language

I am currently creating my own compiled programming language, and I have come to a point where I would like to start working on the type system and introduce some type checking. Ideally I would like ...
1
vote
1answer
61 views

How does C++'s type checking work when passing overloaded or templated functions as parameter

As I understand, C++ in general features 'one-way' type checking. That is checking the sub-expressions and get their types, and see if the types so far satisfy the constraints imposed by the current ...
4
votes
2answers
177 views

Check if a lambda constructor is well-typed

In basic type inference for 𝜆-calculus with parametric polymorphism à la Hindley–Milner, when can we say that we cannot give a type to a lambda constructor? For example $$(λx.λy.y(x\ ...
4
votes
1answer
81 views

Static type analysis with dynamic scoping?

Both in school and out, I have only ever encountered dynamic scoping paired with dynamic typing. Is there any published work (even if just academic, not yet implemented in a "real" programming ...
6
votes
1answer
78 views

Type system with subtyping on abstract data types?

Consider this example on binary trees in some ML-like language: ...
2
votes
0answers
34 views

Question about let syntax in type systems

I'm on the Wikipedia page for Hindley-Milner type systems, on the section about "let polymorphism": https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Let-polymorphism I'm a bit ...
2
votes
0answers
26 views

How does the free program identifiers (fpi) extend over constraints and type schemes in $HM(X)$?

Chapter 10 of Advanced Topics in Types and Programming Languages; gives a very comprehensive description of type inference by constraints solving. They introduce the free program indentifiers of an ...
4
votes
1answer
310 views

Drawbacks of adding type equality to 1ML

In the 1ML – Core and Modules United (F-ing First-Class Modules) paper, the author gives the following example for why module types do not form a lattice under subtyping: ...
6
votes
2answers
323 views

LET REC recursive expression static typing rule

I'm taking a programming languages course and had a question regarding the typing rules for a recursive let rec expression in a static typing system. To be more ...
1
vote
0answers
53 views

Propositional extentionality in the lean theorem prover?

Propositional extentionality in the lean theorem prover is stated as the following axiom: axiom proptext {a b : Prop} : (a $\iff$ b) \to a = b My confusion about this is as follows: Previously I’...
2
votes
0answers
99 views

Relation between “formal verification”, “formal proof”, and “type systems” for software verification?

I have a vague understanding what formal verification is about, a vague understanding of what the cutting edge is of type theory for programming languages, and a better understanding of formal proofs. ...
2
votes
0answers
40 views

What is the difference between ADTs and ASDLs?

ASDL stands for Abstract Syntax Description Language (ASDL), whereby ADT stands for Algebraic data type. By looking at Python.asdl it appears to me to be the same thingy, just with different names, ...
5
votes
1answer
93 views

Type system for Query DSL with only simple GADTs: what typing judgments are needed?

Background I have several F# codebases with reasonably high level of complexity of code. In order to convince myself that the code is solid I do whatever I can to write as much of it as possible type-...
1
vote
2answers
111 views

Symbolic Evaluation for Type Inference in a Dynamic Language

Say I have the following contrived example code: ...
2
votes
1answer
151 views

Assertion of Type Inference Rules/Type Checking

I have a problem in a book I am trying to accomplish. I understand the overall type of the expression is boolean and how it derives. (y * x) will be rule 4 (counting from top right). (y * x) + x when ...
2
votes
1answer
76 views

What is the type system (or class of type systems) that that ensures all your tree Branches end in Leaves?

I've come across this situation numerous times in the past few years where I have some classes like (pseudo-Java): ...
11
votes
2answers
222 views

Reducing products in HoTT to church/scott encodings

So I am currently going though the HoTT book with some people. I made the claim that most inductive types we will see can be reduced to types containing only dependent function types and universes by ...
9
votes
1answer
2k views

Is there a difference between type safety and type soundness?

I've been trying to tease apart the definitions of type safety and type soundness and I'm having a heck of a time of it. I asked a professor recently and after a bit of thought he said that there ...
4
votes
1answer
169 views

Linear/affine lifetimes without subtyping

Are there any type systems similar to rust that don't depend on subtyping ? Can we express that one value must be consumed or dropped before another? For instance if I had an array of huge values on ...
4
votes
1answer
122 views

What's the advantage of “value restriction” over its alternatives?

What is the motivation to pick "value restriction" over other candidates? Examples of alternatives: Enclosing pureness into the function type, for example: ...
8
votes
0answers
272 views

Type-classes for type inference

I'm creating a semantic analyzer with type inference. For the basics I've got a type variable and a type construct with name and a list of types. I want to support overloading and I know that Haskell ...
7
votes
2answers
684 views

Higher-ranked polymorphism without explicit application or subtyping?

So, I'm familiar with two main strategies of having higher-ranked polymorphism in a language: System-F style polymorphism, where functions are explicitly typed, and instantiation happens explicitly ...
8
votes
2answers
1k views

Relation between type-checking decidability, typability decidability and strong normalization

Yo! This is probably a stupid question, however I've never seen it written down explicitly if, for instance, decidability of type-checking is equivalent to the strong normalization property. Therefore ...
6
votes
2answers
459 views

What's the advantage of typed assembly?

I've seen scattered references to typed assembly in high assurance literature, but I don't really understand the advantage. If the compiler/runtime are capable of passing the types down to the CPU, ...
3
votes
2answers
291 views

Which type compilers report if they cannot infer a precise type?

In the presence of subtyping, a type checker can usually infer only some inequality constraints on the type rather than the exact type. Of course, internally it will store the full constraints. But ...
5
votes
1answer
106 views

Local type argument synthesis when type variable does not appear in arguments

I am implementing the techniques described in the classic Local Type Inference paper. Specifically, I am implementing the type argument synthesis algorithm from section 3. My algorithm seems to ...
2
votes
0answers
101 views

Dependent types as regular expressions

Would be possible to encode dependent types as regular expressions? if so, ¿is there some work about? It's common to represent restrictions for elements in a traversable data structure with them, ...
7
votes
1answer
288 views

Reference request: optimizing procedures on lists in dynamic languages by performing safety checks in advance

For my science fair project, I implemented an optimization to Python's sort routine. The idea is to move the safety checks that have to be carried out during each comparison, e.g. type checks and ...
3
votes
2answers
59 views

how to use type application rule (T-TAPP)?

In the following rule, $$\dfrac{ \Gamma \vdash t_1 : \forall X.T_{12} } { \Gamma \vdash t_1 \ [T_2] : [X \mapsto T_2]T_{12} } \textsf{ (T-TApp)}$$ whend doing type checking, how ...
4
votes
1answer
84 views

How to understand these exposure algorithm rules for System F sub?

The book "Types and Programming Languages" said System F sub type checking introduce exposure typing rules alongside algorithmic typing and sub-typing rules. ...
3
votes
1answer
277 views

Algebraic data types - unions

Are there any programming languages where algebraic data types can be expressed not only by using intersection and disjoint union but also a standard set union (intersection + disjoint union)? Do ...