Questions tagged [type-checking]

Checking that types adhere to the tying rules.

Filter by
Sorted by
Tagged with
5 votes
1 answer
97 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 ...
user avatar
6 votes
1 answer
97 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 ...
user avatar
  • 419
15 votes
2 answers
843 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 ...
user avatar
8 votes
1 answer
150 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 ...
user avatar
11 votes
1 answer
138 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 ...
user avatar
  • 651