Questions tagged [type-checking]

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

21 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
13 votes
0 answers
220 views

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

(it's a repost of my unanswered question from [email protected] about Scala) In the Scala Language Specification, §4.4 Type Parameters, there is a requirement: The most general form of a ...
Vladimir Reshetnikov's user avatar
8 votes
0 answers
344 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 ...
Peter Lenkefi's user avatar
6 votes
0 answers
706 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 ...
Jake's user avatar
  • 3,800
4 votes
0 answers
228 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 ...
beta's user avatar
  • 141
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
3 votes
0 answers
487 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
3 votes
0 answers
78 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,692
3 votes
0 answers
223 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,692
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
2 votes
0 answers
191 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
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
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
  • 141
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
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
2 votes
0 answers
121 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, ...
jneira's user avatar
  • 129
2 votes
0 answers
32 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 ...
Joey Eremondi's user avatar
1 vote
0 answers
58 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
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
1 vote
0 answers
527 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 ...
Pushpa's user avatar
  • 933
0 votes
0 answers
61 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
0 answers
79 views

Type inference example?

In my programming languages course we are reviewing type inference, i didnt get very well how to make this task. I all ready search at the bibliography of my course (PLAI by Shriram krishnamurthi) ...
newWithPython's user avatar