11
$\begingroup$

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 on page 7. In type checker. It's got these evaluations with empty environments. Eg. let v = eval↓ t []. Precisely when these are evaluated, could it crash to the d !! i in the Figure 4?

Dependently typed languages are related to implementation of proof assistants.

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ I'd like to see how you would connect the issue of type checking (in Haskell) to the site's focus on proof assistants. The Question in its present form is terse. $\endgroup$
    – hardmath
    Commented Feb 10, 2022 at 16:09
  • 3
    $\begingroup$ It's a dependently typed language being typechecked. It is related to implementation of proof assistants. $\endgroup$
    – Cheery
    Commented Feb 10, 2022 at 16:15
  • 1
    $\begingroup$ I vote to reopen since I think this question is on-topic. It is definitely relevant to anyone interested in dependently-typed proof assistants (including Coq, Lean, Agda, which dominate this SE already). $\endgroup$
    – Li-yao Xia
    Commented Feb 10, 2022 at 19:58
  • 1
    $\begingroup$ Specifically, figure 12 has $\mathtt{type}_{\uparrow}$ invoke $\mathtt{eval}_{\downarrow}~t~[]$, and you're worried that might throw errors or be buggy? $\endgroup$
    – Alex Nelson
    Commented Feb 10, 2022 at 20:41
  • 1
    $\begingroup$ Can someone from Glasgow please tell Conor McBride that he is needed over here? $\endgroup$
    – Andrej Bauer
    Commented Feb 10, 2022 at 20:52

1 Answer 1

Reset to default
8
$\begingroup$

All is well.

The implementation distinguishes between bound variables, represented as Bound i where i :: Int and free variables, represented as Par n where n :: Name. The evaluation function eval↑ in Figure 4 converts names to values using vpar and it replaces bound variables by looking them up in the environment (this is the line with d !! i).

In Figure 12 there are several calls of the form eval↓ τ []. These are valid because in all cases τ does not contain any "exposed" bound variables, therefore it is safe to evaluate it in the empty environment (τ may contain free variables, but those are not problematic). Indeed, the clause for typing an abstraction Lam e in the definition of type↓ typechecks e by first replacing the bound variable 0 with a free variable of the form Par (Bound i), where i counts the abstraction depth. This way we make sure that an "exposed" bound variable will never be encountered.

Improve this answer
$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.