Questions tagged [type-checking]

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

Filter by
Sorted by
Tagged with
1 vote
0 answers
57 views

How do you deal with Skolem functions which escape their scope in elimination rules?

If you have an elimination rule for tuples which introduce the left and right pair into the type checking context, what do you do if the type of one of the elements is quantified and has been ...
Jean-Baptiste's user avatar
2 votes
1 answer
53 views

Top type in JavaScript?

I am wondering, what is the top type, $\top$, in JavaScript? The diagrams at MDN make it look as if 'null' is a top type, but wikipedia's entry for top type indicate that it is Object in JS, which ...
Hank Igoe's user avatar
  • 179
0 votes
0 answers
55 views

Is type inference for arbitrary-rank types decidable when supplied type signatures?

I found following statements in 6.4.16. Arbitrary-rank polymorphism of ghc document. GHC uses an algorithm proposed by Odersky and Laufer (“Putting type annotations to work”, POPL‘96) to get a ...
ksrk's user avatar
  • 13
0 votes
1 answer
63 views

Are linked lists homogenious or heterogenious containers?

I have always assumed that "Linked List" is something in the lines of ...
Vorac's user avatar
  • 103
1 vote
1 answer
59 views

How does GHC insert type abstraction/application under the RankNTypes extension

I'm developing a functional programming language that offers Rank-n polymorphism. Like Haskell I don't want types to appear at the term level, but I have no idea to insert type abstraction and type ...
ksrk's user avatar
  • 13
0 votes
1 answer
86 views

How to think about typing inference rules when thinking about typechecking?

I am trying to build an imperative programming language with a type system that will allow for proofs. I just found kind lang, which implements all the ideas that I have been meaning to use (plus more)...
Lance's user avatar
  • 2,163
2 votes
2 answers
283 views

what are meta variables in this static analysis book's explanation about types?

At page 21 of this book: https://cs.au.dk/~amoeller/spa/spa.pdf I found this: I started reading everything and understanding it pretty well, until this. It's defining the possible types of a language....
Paprika's user avatar
  • 121
2 votes
0 answers
29 views

Data + data schema needs dependent types to be type-checked statically?

I will set this question in a very practical way. Let's say we have a web-form data received as JSON at the backend together with the schema (for instance, some version of JSON schema), something like:...
Roman Susi's user avatar
1 vote
0 answers
75 views

How do program types such as natural numbers figure into the Curry-Howard Isomorphism?

In Coq, the nat, the type of natural numbers, has type Set. By the Curry-Howard Isomorphism, all propositions of type ...
user3565552's user avatar
6 votes
2 answers
315 views

Does strong typing contribute to better performance optimization by compiler?

Do guarantees provided by the type systems enable better performance optimizations by the modern compilers? I found a 20+ year article suggesting that it would. Also, intuitively speaking, knowing ...
kolistivra's user avatar
4 votes
1 answer
317 views

Is occurrence typing (flow-sensitive typing) a form of dependent typing?

I take occurrence typing to be typing that "... allows the type system to ascribe more precise types based on whether a [check] succeeds or fails." (adapted from the Racket docs with "...
Max Heiber's user avatar
4 votes
1 answer
94 views

Which language is used to construct a type system?

Typically, OCaml and Scala seem to be used for designing any programming languages tool. But what features offer them an edge over other languages. A related question, is a type system for a language ...
mythbuster's user avatar
2 votes
1 answer
272 views

How does the undecidability of Extensional Martin-Löf Type Theory apply to real type-checking compilers?

It is claimed in many sources (for example, here) that adding a rule like "if Id(X,Y) then X really equals ...
Сергей Макеев's user avatar
2 votes
1 answer
105 views

Type-checking function calls with functional subtyping

I'm relatively new to the topic. Suppose that you want to type-check an expression of the form f(a), i.e. a function call. Assuming that all the declarations are ...
giofrida's user avatar
  • 183
1 vote
2 answers
386 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 ...
Tim's user avatar
  • 4,845
2 votes
1 answer
126 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 ...
Tim's user avatar
  • 4,845
0 votes
1 answer
55 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 ...
gifa's user avatar
  • 58
5 votes
2 answers
652 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 ...
Bharat Khatri's user avatar
2 votes
2 answers
217 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?
Suminda Sirinath S. Dharmasena's user avatar
3 votes
3 answers
945 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 (...
user56834's user avatar
  • 3,652
2 votes
1 answer
62 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 \;...
user1868607's user avatar
  • 2,184
9 votes
5 answers
1k 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 ...
A. Sallai's user avatar
  • 243
3 votes
0 answers
33 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 ...
YvesgereY's user avatar
  • 141
2 votes
0 answers
180 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 ...
TomC's user avatar
  • 21
2 votes
2 answers
87 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 ...
Charlie Parker's user avatar
2 votes
2 answers
218 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 ...
Charlie Parker's user avatar
5 votes
1 answer
119 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 ...
Charlie Parker's user avatar
11 votes
1 answer
2k 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 ...
Labbekak's user avatar
  • 565
8 votes
1 answer
592 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 ...
Foxy's user avatar
  • 255
2 votes
0 answers
46 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 ...
Tobias Marschall's user avatar
3 votes
0 answers
422 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 ...
Labbekak's user avatar
  • 565
12 votes
5 answers
2k 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 ...
bdsl's user avatar
  • 221
1 vote
1 answer
93 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 ...
eirikvaa's user avatar
  • 113
1 vote
1 answer
73 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 ...
Rui Liu's user avatar
  • 183
5 votes
2 answers
727 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\ ...
Gallaoui's user avatar
  • 153
5 votes
1 answer
312 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 ...
Logan R. Kearsley's user avatar
7 votes
1 answer
100 views

Type system with subtyping on abstract data types?

Consider this example on binary trees in some ML-like language: ...
soren-n's user avatar
  • 118
2 votes
0 answers
37 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 ...
Neel's user avatar
  • 131
2 votes
0 answers
30 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 ...
manu's user avatar
  • 121
5 votes
1 answer
333 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: ...
typesanitizer's user avatar
7 votes
2 answers
591 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 ...
Sean's user avatar
  • 570
3 votes
0 answers
76 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’...
user56834's user avatar
  • 3,652
3 votes
0 answers
205 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. ...
user56834's user avatar
  • 3,652
2 votes
0 answers
53 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, ...
denis631's user avatar
  • 133
5 votes
1 answer
142 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-...
Kazark's user avatar
  • 253
1 vote
2 answers
184 views

Symbolic Evaluation for Type Inference in a Dynamic Language

Say I have the following contrived example code: ...
Lance's user avatar
  • 2,163
3 votes
1 answer
261 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 ...
Frank Duckworth West's user avatar
2 votes
1 answer
107 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): ...
GlenPeterson's user avatar
12 votes
2 answers
309 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 ...
Jake's user avatar
  • 3,790
14 votes
1 answer
4k 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 ...
Ben Kushigian's user avatar