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?

Improve this question
$\endgroup$
8
  • 1
    $\begingroup$ Do hole/meta variables suit your need? $\endgroup$
    – Guest0x0
    Commented Jul 9, 2022 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$
    – Andrej Bauer
    Commented Jul 9, 2022 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$
    – Ms. Molly Stewart-Gallus
    Commented Jul 9, 2022 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
    Commented Jul 10, 2022 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
    Commented Jul 10, 2022 at 2:44

0

Reset to default

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.