0
$\begingroup$

Advanced Topics in Types and Programming Languages gives this rule section 2.2 gives this rule for dependent function application:

$$\frac{\Gamma \vdash t_1 : (\Pi x : S.T) \quad \Gamma \vdash t_2 : S}{\Gamma \vdash t_1 t_2 : [ x \mapsto t_2 ] }$$

In "Modules Matter Most" Bob Harper gives this rule for ML functor application:

$$\frac{\Gamma \vdash M : A \quad \Gamma, x : A \vdash N : B}{\Gamma \vdash [M / x ] N : B}$$

What are the similarities and differences between these judgments?

To give a concrete example of the kind of thing I'm looking for, I asked ChatGPT to compare the rules and it said (among other things):

  1. In the ML functor application rule, the argument $N$ is an expression that depends on $x$, whereas in the dependent function application rule, the argument $t_2$ is a simple value of type $S$.
  2. In the ML functor application rule, the result type $B$ does not depend on the value of the argument $M$, whereas in the dependent function application rule, the return type $T$ depends on the value of the argument $t_2$.

I suspect that the ChatGPT answer is misleading.

$\endgroup$
2
  • $\begingroup$ ChatGPT isn't really good with academics, and often gives believable but incorrect results - so I really recommend against asking it such questions :o $\endgroup$
    – nir shahar
    Commented Mar 31, 2023 at 21:31
  • $\begingroup$ The harm is in believing $\endgroup$
    – Max Heiber
    Commented Apr 1, 2023 at 7:30

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.