Skip to main content

Questions tagged [type-checking]

Checking that types adhere to the tying rules.

Filter by
Sorted by
Tagged with
4 votes
2 answers
106 views

Can't infer type for lambda?

I am trying to understand the TinyIdris code for type-checking here. The main function checkTerm handles type inference for lambda abstractions by directing ...
tinlyx's user avatar
  • 2,034
3 votes
1 answer
82 views

How to read/understand the definition of the environment in type-checking?

I am trying to read the code for TinyIdris, but couldn't understand one of the first definitions about environments below (because of my lack of understanding about type-checking and/or dependent ...
tinlyx's user avatar
  • 2,034
5 votes
2 answers
223 views

What is a context mapping in dependent type checking?

I am reading a dissertation about dependent type programming language (Norell, 2007), and had much trouble understanding the definition of context mappings/substitutions as shown in the figure below . ...
tinlyx's user avatar
  • 2,034
1 vote
1 answer
96 views

confused about stlc from Programming Language Foundations

I have two related quetions. I made my way to STLC and Typechecking from Programming Lang Foundations, yet I am more or less mentally stuck at the STLC chapter, hence many things related to it are ...
noCrayCray's user avatar
2 votes
1 answer
105 views

Why does an internal term produced by Lean's equation compiler have holes in it?

Section 4.7 of the Lean reference manual (version 3.3) gives an example of a division function defined by well-founded recursion. I used the #print command to ...
ttbo's user avatar
  • 35
1 vote
1 answer
80 views

Code obtained from printing a definition from the Lean 3.46 equation compiler does not type check. Why doesn't it, and how can I fix it?

In the example below, the fibonacci function is defined via the Lean equation compiler. However, there seems to be a problem with the code that is obtained from running ...
ttbo's user avatar
  • 35
7 votes
1 answer
573 views

How do I convince the Lean 4 type checker that addition is commutative?

In order to get acquainted with Lean and programming with dependent types I am trying to implement basic operations for a Vector datatype defined following the ...
BackusNaur's user avatar
6 votes
1 answer
149 views

Does Coq's Module and Functor type-check incrementally?

I am trying to search the following questions online but I failed: When applying a functor (parametrized module), will the contents inside the functor be re-type-checked? Will Coq's command ...
Ende Jin's user avatar
  • 429
19 votes
2 answers
3k views

What is bidirectional type checking?

What is bidirectional type checking and why would I want to implement it? It feels like the name is a bit of a misnomer and the syntactic separation kind of resembles stuff like ANF, call by push ...
Ms. Molly Stewart-Gallus's user avatar
10 votes
1 answer
440 views

Type Checking Undecidable in Extensional Type Theory

What is the difference between intensional vs extensional type theories and how come the type checking is undecidable for extensional type theory? Also, how does it affect the expressiveness of ...
keep_learning's user avatar
11 votes
1 answer
182 views

In the "Simply Easy!" paper, why is it safe to evaluate types in the empty environment?

The paper in question: An Implementation of a Dependently Typed Lambda Calculus by Andres Löh, Conor McBride and Wouter Swierstra. I'm wondering whether it's correct in what's it is doing. Precisely ...
Cheery's user avatar
  • 721