0
$\begingroup$

For the kernel of a proof assistant free variables/universal quantification may be sufficient. In higher level languages such as Coq's tactic language indeterminate variables (not sure of the wording here)/existential variables may be useful.

Also personally I'm interested in languages lacking the full power of dependent product/functions so good use of dependent sum/products is really important.

How do you implement indeterminate/existential variables in type theory?

$\endgroup$
6
  • 1
    $\begingroup$ Do hole/meta variables suit your need? $\endgroup$
    – Guest0x0
    Jul 9 at 4:44
  • 2
    $\begingroup$ Generally they are implemented as metavariables – a concept that is swept under the rug, done badly by mixing object and meta levels, and generally not paid due attention. (If we behaved like this in algebra, we wouldn't teach the fact that polynomials form a ring.) $\endgroup$ Jul 9 at 11:51
  • $\begingroup$ @Guest0x0 I think holes/metavariables might work ? I was partially inspired after reading cs.uwaterloo.ca/~plragde/flane/LACI/… to ask this question anyhow. I just don't know enough about holes to know if they are the right construct here. $\endgroup$ Jul 9 at 17:20
  • 1
    $\begingroup$ @MolossusSpondee Holes/Meta variables behave like existential variables because they can be instantiated exactly once, substituted to exactly one type. However, this process is controlled by the type checker not the user, also you usually cannot quantify over meta variables directly. $\endgroup$
    – Guest0x0
    Jul 10 at 0:01
  • 1
    $\begingroup$ @MolossusSpondee I think no. Actually I think meta variables should not be considered part of the object language, otherwise you just account for type checking and elaboration in metatheory $\endgroup$
    – Guest0x0
    Jul 10 at 2:44

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.