4
$\begingroup$

Is the LEAN type checker able to count the number of times a parameter is used in a function body?

In Idris2 for comparison I might use (1 x:Nat) which then makes sure my function uses x exactly once. Or I might write (0 pf: x < 5) to make sure the parameter gets erased. In LEAN can I force the type checker to counter uses?


Seems linear-type is not a tag yet and I haven't the points needed to create a tag, happy to have a power user edit that.

$\endgroup$
2
  • 1
    $\begingroup$ Done! You can edit the tag wiki if you like. $\endgroup$
    – Trebor
    Jun 10, 2023 at 16:15
  • 1
    $\begingroup$ I’m not aware of anything like that, so I think the answer is no, but I see here Leo mentioning that this is a planned future addition to Lean (leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/…). That was over a year ago, so I’ll let a more knowledgeable person answer. $\endgroup$
    – Jason Rute
    Jun 10, 2023 at 16:22

1 Answer 1

6
$\begingroup$

No, the type checker implements a theory that does not have any substructural types in it. You can implement this as an after-the-fact checker though, by analyzing the term to see where it has been used.

$\endgroup$
2
  • $\begingroup$ True, but I'd like to use it within proofs, to prove an algorithm uses resources according to plan. An after-the-fact checker won't interact with other proofs in LEAN I suspect. $\endgroup$
    – Algeboy
    Jun 11, 2023 at 14:06
  • 1
    $\begingroup$ It can, your after the fact checker can produce proofs of its own which interact with other proofs produced by the checker to get whole program correctness statements. It's a project, though, people usually write masters theses about this kind of thing. $\endgroup$ Jun 11, 2023 at 17:36

Your Answer

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

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