Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [type-checking]

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

2
votes
0answers
15 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 ...
3
votes
1answer
136 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: ...
5
votes
2answers
107 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
16 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
19 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. ...
1
vote
0answers
29 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, ...
3
votes
0answers
37 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-...
0
votes
0answers
23 views

let-expression type-cheking in pure type systems

I asked before for references about pure type systems and let-expression, but I did not get any response with implementation details. Reading the literature I have concluded that this is the way to ...
1
vote
2answers
67 views

Symbolic Evaluation for Type Inference in a Dynamic Language

Say I have the following contrived example code: ...
2
votes
1answer
90 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
57 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
163 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 ...
7
votes
1answer
921 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
93 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
54 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
205 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
610 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 ...
7
votes
2answers
635 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 ...
7
votes
2answers
206 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
287 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
91 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
82 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
281 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
55 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
76 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
148 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 ...
4
votes
1answer
166 views

how type checking fails?

I was doing a type checking example in system f sub on paper to understand how it works. according to Pierce's book Types and Programming Languages, numbers and their types are following in system f ...
8
votes
1answer
159 views

Relation between Type Assignment system (TA) and Hindley-Milner system

Recently I started my studies in type theory/type systems and Lambda Calculus. I have already read about Simple Typed Lambda Calculus in Church and Curry style. The last one is also known as Type ...
6
votes
1answer
186 views

Safe way to explicitly define new types instead of using Algebraic data types for my functional language

Question: As I'm working on a Hindley-Milner typed lambda calculus, in order to make it usable I need to add some types such as list and pairs. The way I currently do it is, I have an ...
3
votes
2answers
109 views

Get term type during evaluation using Hindley-Milner type system

I've implemented a lambda calculus evaluator and use the Hindley-Milner algorithm to infer terms types and ensure type correctness without the user having to explicitly annotate types. But now I'd ...
5
votes
1answer
145 views

Does Damas-Milner still have principal types if existential type schemata are added?

In the Damas-Milner type system, type schemata can be formed in two ways: $T$ $\forall X. S$ Where $T$ ranges over monotypes and $S$ ranges over type schemata. The type-checking algorithm for this ...
4
votes
2answers
333 views

System f-sub, how to do type checking?

I was reading that system f-sub (polymorphic lambda calculus with sub-typing) and I was quite confused with its one checking rule called "T-TAPP". This rule as following (ctx denotes the typing ...
0
votes
0answers
321 views

Type inference and Type checking

I understand that adding the annotations (dependent typing) may cause the type checking of the programming language to become undecidable. What about type inference ? Whether type checking and type ...
5
votes
1answer
197 views

Proving preservation under substitution System F Omega

I am going over the proofs for the simply typed lambda calculus in the book "Types and Programming languages" by Benjamin Pierce. I am trying to find inspiration for the similar proofs for System F ...
6
votes
2answers
288 views

Decidability of dependent typing on primitive recursive languages

With a dependent type system in a normal functional language type checking may never halt. This is partially because dependent typing removes the isolation between types, and code. My question is this:...
2
votes
0answers
24 views

Where does the term “Amechanicity” for type-error generation come from

I've been looking at these slides about improving type error messages for programming languages. One of the things they describe, starting at Slide 8, is the concept of amechanicity. Anytime the ...
2
votes
1answer
62 views

Confusion about data types, compilers, hardware data representation and static vs dynamic typing

I am trying to understand static vs dynamic typing, but am really struggling to see how everything fits together. It all starts with data types. As far as I understand, data types are quite abstract ...
5
votes
1answer
165 views

Question about “Type checking a multithreaded functional language with session types” by Vasconcelos et al

I have been reading the paper[1] in the title. But there are some parts of it that are unclear to me, more specifically the way you typecheck a lambda. I have attached the typing rules below as images[...
3
votes
1answer
1k views

Creating arrays of object of abstract class in statically-typed object-oriented languages

In statically-typed object-oriented languages (like Java, C++, C#, ...), suppose I declare an abstract class: public abstract class myclass1 { ................. } ...
28
votes
8answers
11k views

How does a computer determine the data type of a byte?

For example, if the computer has 10111100 stored on one particular byte of RAM, how does the computer know to interpret this byte as an integer, ASCII character, or ...
6
votes
2answers
277 views

Can we prove that $1 + 2 + \dots + n = \frac{n(n+1)}{2}$ using a computer program?

Chapter 7 of The Haskell Road to Logic Math and Programming discusses induction and recursion. Haskell is strongly typed and we can define the natural numbers ...
6
votes
0answers
372 views

Is the strictly positive condition in Coq and Agda an aproximation?

Languages like Coq and Agda enforce that their inductive types occur "strictly positively" in their definitions. That is, the type should not occur to the left of an arrow of an argument of a ...
13
votes
0answers
171 views

Why do we have to forbid non-conforming lower and upper type bounds?

(it's a repost of my unanswered question from scala-user@googlegroups.com about Scala) In the Scala Language Specification, §4.4 Type Parameters, there is a requirement: The most general form of a ...
4
votes
2answers
168 views

Algorithmic type checking for Calculus of Inductive Constructions

So from reading "Advanced Topics in Types and Programming Languages" (ATTPL) I know of the calculus of constructions (CoC). It also presents the "algorithmic" type checking rules. Reading Coq's ...
1
vote
0answers
22 views

Importance of indexes in Type(i) in calculus of inductive constructions [duplicate]

So I am reading about the calculus of inductive constructions. And I see here and here that there hidden indexes that the user does not know about in the $Type$ sort. It says that they are ...
9
votes
1answer
252 views

What is a non-contrived example of static type-checking being too conservative?

In Concepts in Programming Languages, John Mitchell writes that static type checking is necessarily conservative (overly strict) because of the Halting Problem. He gives as an example: ...
4
votes
0answers
170 views

Updating types during type inference in a Hindley-Milner type system

I'm looking at implementing type inference for a Hindley-Milner type system, and before I have even started to implement the Damas-Milner algorithm, while working through some examples, I hit some ...
4
votes
2answers
84 views

Definition of a size of type

In B. Pierce's book "Types and Programming Languages", he talks about the size of types (see pictures below). I searched the book for a definition but could not find one. I only found a definition ...
12
votes
1answer
608 views

Why aren't we researching more towards compile time guarantees?

I love all that is compile time and I love the idea that once you compile a program a lot of guarantees are made about it's execution. Generally speaking a static type system (Haskell, C++, ...) seems ...
0
votes
1answer
67 views

Type checking relation to logic

I am learning logic and functional programming and there is a topic called Type checking and their relationship to logic , I am unable to find any source that can help me in understanding this topic. ...