partial functions inside of non-partial -> why no error?

Stream: general

[Serhii Khoma (srghma)]

why lean allows to write

partial def infiniteLoop (n : Nat) : Nat :=
  infiniteLoop (n + 1)

def tryUsePartial (n : Nat) : Nat :=
  infiniteLoop n

#eval tryUsePartial 4

why it doesnt throw error You should make "tryUsePartial" partial too ?

Idris2 doesnt allow to use non-total functions inside of total, thus forcing user to keep track of safe and not-safe functions

[Aaron Liu]

All I can say is that Lean is not Idris2 and it does allow this. If you want to make it infectious you should use unsafe def infiniteLoop.

[Robin Arnez]

infiniteLoop is "total" but it just has a bunch of garbage values you can't prove anything about

[Niklas Halonen]

I'm not an expert, but afaik this is sound in type theory as the function type is inhabited as opposed to e.g.

partial def loop : α := loop

which has type {α : Type*} →α.

If the above would type check, it would allow the existence of a bottom element. Instead it fails with a useful error message:

failed to compile 'partial' definition 'loop', could not prove that the type {α : Sort u_1} → α is nonempty.

[Serhii Khoma (srghma)]

Niklas Halonen

But it will compile with this

partial def loop [Nonempty α] : α := loop

[Mirek Olšák]

Recently, I tried to figure out a reasonable interpretation for partial functions here: #general > possible semantics for partial functions @ 💬
Just a few basic notes:

• If we don't want to trust the compiler with native_decide, then

def loop [Nonempty α] : α := Classical.choice (inferInstance : Nonempty α)

is a logically consistent interpretation of any partial function. The kernel cannot see inside a partial definition.

• If we want to trust the compiler (which I believe should be in principle consistent without unsafe [implemented_by]), then a partial function can be interpreted as a function that runs for at most 10^100 (any number bigger than any feasible computation) steps, and if doesn't terminate by then, it returns again arbitrary value given by the choice axiom.
• I believe better interpretations are plausible too, I ponder about it in the entire linked thread.

[Serhii Khoma (srghma)]

Robin Arnez said:

infiniteLoop is "total" but it just has a bunch of garbage values you can't prove anything about

Hm

https://kowainik.github.io/posts/totality

The terminology of totality is a bit ambiguous in programming due to the different use-cases. In some places, total functions are required to terminate, while others require only to handle all inputs’ values.

Ok, ok, seems like in lean "total" didn't imply "terminates"
Though In idris2 "total" does imply "terminates", "covering" doesn't

---

Therefore:

IIUC patritial def and def in lean == "covering" from Idris2. "partial" from Idris2 (some inputs are not mapped) is possible only in unsafe.

Therefore
Me :flag_ukraine:: I completely don't understand what is partial in partial def.
Achilles:foot:: "partial def doesn't cover all inputs(?) :thinking:"?
Tortoise:turtle:: No, it does. :stop:
Achilles:foot:: "partial def doesn't terminate!:light_bulb:".
Tortoise:turtle:: But def doesn't terminate too if partial def is used inside of def! :laughing:
Achilles:foot:: Then why we don't mark defs that use partial defs inside with partial too? :thinking:
Tortoise:turtle:: Indeed! That's what I talk about!
Achilles:foot:: So why no?
Tortoise:turtle:: because "lean is not Idris" (?)
Achilles:foot:: that is not an answer!
Tortoise:turtle:: yes. Ok. I assume lean developers (when they were implementing lean) have found that half of lean code depends on functions that are partial def. So they were just lazy to mark all of them with partial too like this is done in lean
Achilles:foot:: ok, seems like explanation. But anyway, they could implement it as annotation (like@[unsafe_disable_termination_check]) instead of partial def, bc in my understanding annotations should be something that doesn't propagate and declaration modifiers should be something that propagates
Tortoise:turtle:: Indeed! Look

-- 1. safe / total
def safe_id {α} (x : α) : α := x

-- 2. noncomputable
noncomputable def noncomp_id {α} [Nonempty α] : α :=
  Classical.choice ‹_›

-- 3. unsafe
unsafe def unsafe_id {α} (x : α) : α := x

-- 4. partial
partial def partial_loop {α} [Nonempty α] : α :=
  partial_loop   -- diverges

-- 5. nonrec
nonrec def nonrec_id {α} (x : α) : α := x

nonrec def nr_calls_def : Nat := safe_id 5  -- ❗ can use def inside of nonrec def, but I think should not allow
--nonrec def nr_calls_noncomp [Nonempty Nat] : Nat := noncomp_id -- cannot use noncomputable def inside of nonrec def, good 👍
--nonrec def nr_calls_unsafe : Nat := unsafe_id 5 -- same
nonrec def nr_calls_partial : Nat := partial_loop -- ❗ can use partial def inside of nonrec def, but I think should not allow
nonrec def nr_calls_nonrec : Nat := nonrec_id 5

def def_calls_def : Nat := safe_id 5
def def_calls_nonrec : Nat := nonrec_id 5 -- can use nonrec def inside of def, good, nonrec is subset of def , good 👍
--def def_calls_noncomp : Nat := noncomp_id   -- ERROR: uses noncomputable 👍
--def def_calls_unsafe : Nat := unsafe_id 5   -- ERROR: uses unsafe 👍
def def_calls_partial : Nat := partial_loop -- ❗can use partial def inside of def, bad 😞, def should be a subset of partial def , not vice versa

partial def part_calls_def : Nat := safe_id 5
--partial def part_calls_noncomp [Nonempty Nat] : Nat := noncomp_id -- error 👍
--partial def part_calls_unsafe : Nat := unsafe_id 5 -- error 👍
partial def part_calls_partial [Nonempty Nat] : Nat := partial_loop
partial def part_calls_nonrec : Nat := nonrec_id 5

unsafe def us_calls_def : Nat := safe_id 5
--unsafe def us_calls_nc [Nonempty Nat] : Nat := noncomp_id -- error 👍
unsafe def us_calls_unsafe : Nat := unsafe_id 5
unsafe def us_calls_nonrec : Nat := nonrec_id 5
unsafe def us_calls_partial : Nat := partial_loop

noncomputable def nc_calls_def : Nat := safe_id 5
noncomputable def nc_calls_noncomp [Nonempty Nat] : Nat := noncomp_id
noncomputable def nc_calls_nonrec : Nat := nonrec_id 5
--noncomputable def nc_calls_unsafe : Nat := unsafe_id 5 -- error 👍 yes, better not to make unsafe a subset of noncomputable, better leave them parallel as is 👍
noncomputable def nc_calls_partial : Nat := partial_loop

unsafe and uncomputable do propagate, and nonrec and partial do not. Really inconsistent!
Achilles:foot:: also would be good to add terminates def modifier?
Tortoise:turtle:: no, if proposal above was implemented ("all modifiers should propagate"), then ordinary def would mean "terminates"
Achilles:foot:: oh, right:+1: thnx

---

Piramid of modifiers , top - more constraints, bottom - less

        /   nonrec def     \  -- no recursion is allowed, all inputs map to outputs, of course terminates
     /         def            \ -- recursion is allowed, all inputs map to outputs, terminates
  /     partial def             \ -- recursion is allowed, all inputs map to outputs, may not terminate for some inputs
/     unsafe    | noncomputable     \

[Aaron Liu]

there are two different ways a function is used here

[Aaron Liu]

there's what the function does from the type theory's point of view and there's what the function does from the compiler's point of view

[Aaron Liu]

from the compiler's point of view the function is compiled into something that will do exactly what you wrote in the code, and this may include calling itself recursively in an infinite loop

[Aaron Liu]

from the type theory's point of view the function immediately halts with an arbitrary value, and this is why you need to prove Nonempty (so we know an arbitrary value exists, and adding the function as a constant to the type theory is sound).

[Aaron Liu]

partial is a marker that tells the elaborator to handle the function in this special way, where the kernel sees an opaque containing an arbitrary value and the compiler sees the actual code

[Aaron Liu]

so it's not infectious because even if you use a partial function inside another function that doesn't mean that this new function should be handled in the same way, where it becomes an opaque constant to the typechecker but the compiler compiles it normally

[Aaron Liu]

Serhii Khoma (srghma) said:

unsafe and uncomputable do propagate, and nonrec and partial do not. Really inconsistent!

The nonrec modifier just means that if you mention the name of the declaration inside itself it will not try to resolve it as a recursive call, and instead will looks for other declarations in the environment that could fit. I don't really associate it with termination.

[Aaron Liu]

by the way you can also combine modifiers and get stuff like

open Classical
-- since we use the axiom `Classical.choice` to construct data, this must be marked noncomputable
noncomputable nonrec def Foo.choice {X : Type u} (h : Nonempty X) : X :=
  -- since this is `nonrec`, `choice` resolves to `Classical.choice`
  -- instead of a recursive call to `Foo.choice`
  choice h

[Aaron Liu]

Serhii Khoma (srghma) said:

unsafe and uncomputable do propagate, and nonrec and partial do not. Really inconsistent!

There is a reason for this! The nonrec defs do not propagate because they both check in the kernel and generate code in the compiler. The partial defs also do not propagate for the same reason, even though the kernel is getting some opaque junk values it still typechecks. But noncomputable def has to propagate because that means the compiler won't generate code for it, so if you call it somewhere else the compiler won't be able to generate code for that call either. And unsafe def also propagates because the kernel doesn't check those declarations, so if you use it in a new declaration then if you try to get the kernel check that new declaration it will not know about it and throw an "unknown constant".

[Aaron Liu]

Also, termination checking is only really relevant for compiling functions for the kernel. The compiler just calls the function recursively. But when you send a term to the kernel, you can't do that, because then it will be a circular proof. So the termination checker has to eliminate out all the recursive calls, and sometimes it's not smart enough to do that automatically so you get an error.

[Matt Diamond]

Here's an example of how the type theory point of view and compiler point of view can come apart:

import Mathlib.Data.Nat.Basic

partial def loop (n : ℕ) : ℕ := loop n

def foo : ℕ := (loop 37) - (loop 37) + 37

-- we can prove foo is 37
example : foo = 37 := by simp [foo]

-- but we can't evaluate it
-- #eval foo

[Matt Diamond]

behavior like this is why the partial keyword can be confusing for some people, I think... it can seem a bit unintuitive

but it also illustrates why it wouldn't make sense for partial to propagate: loop doesn't halt and we can't prove anything about the value, but we can prove something about the value of foo even though it calls loop

[Violeta Hernández]

Aaron Liu said:

Serhii Khoma (srghma) said:

unsafe and uncomputable do propagate, and nonrec and partial do not. Really inconsistent!

The nonrec modifier just means that if you mention the name of the declaration inside itself it will not try to resolve it as a recursive call, and instead will looks for other declarations in the environment that could fit. I don't really associate it with termination.

Really wish we could do away with nonrec, causes more confusion than it solves

[Serhii Khoma (srghma)]

Violeta Hernández said:

Really wish we could do away with nonrec, causes more confusion than it solves

In book Godel Escher Bach there is distinction between Bloop (bounded loop, can use only for i from 0 to 100 for example) and Floop (free loop, can use recursion)

Basically iiuc bloop is same as "my function doesn't use .rec axiom inside"

Therefore I think nonrec is useful

---

Is nonrec == "Bloop"

1. Can use recursivity? No :+1:
2. Can use .rec?

inductive Foo | a | b
noncomputable nonrec def fooToNat (x : Foo) : Nat := Foo.rec 1 2 x

This type checks but this is not a recursive program. So, ok?

inductive Foo
| a
| b
| next : Foo → Foo

nonrec def fooDepth : Foo → Nat
| Foo.a => 0
| Foo.b => 0
| Foo.next x => fooDepth x + 1 -- correctly doesn't type check

noncomputable nonrec def fooDepth' (x : Foo) : Nat :=
  Foo.rec
  (motive := fun _ => Nat)
  0
  0
  (fun _ n => n + 1) -- type checks, though this is a recursive program. Maybe in future this will be disallowed?
  x

3. Only nonrec/bloop can be called inside of nonrec/bloop

No, this is allowed

inductive Foo
| a
| b
| next : Foo → Foo

def fooDepth : Foo → Nat
| Foo.a => 0
| Foo.b => 0
| Foo.next x => fooDepth x + 1

nonrec def fooDepth2 : Foo → Nat
| Foo.a => 0
| Foo.b => 0
| Foo.next x => fooDepth x + 1

Summary: ok, I am confused about usefulness of nonrec myself. It's not the "only Bloop axioms are here".

Is it for kernel? "Kernel cannot accept circular proofs"? Then why can use def inside of nonrec def?

[Matt Diamond]

I can't say for sure but I thought that nonrec was sometimes used to prevent variable shadowing, where the name of the function is potentially shadowing another function with the same name

for example:

import Mathlib.Data.Nat.Basic

def foo (n : ℕ) := n * 2

-- removing `nonrec` causes a "fail to show termination" error
nonrec def Bar.foo (n : ℕ) := foo n + 1

[Aaron Liu]

Serhii Khoma (srghma) said:

Summary: ok, I am confused about usefulness of nonrec myself. It's not the "only Bloop axioms are here".

The only thing that nonrec does it that it removes the ability for that definition to reference itself. Then, for example, if you use the name of the definition inside its own body it will not try to interpret that as a recursive call. It does not however prevent you from doing recursion in a different way, for example calling another function which is itself recursive.

[Aaron Liu]

Serhii Khoma (srghma) said:

Basically iiuc bloop is same as "my function doesn't use .rec axiom inside"

Without the recursor you can't really define any nontrivial functions though

[Trebor Huang]

There are very similar differences between let and letrec in other languages, where let doesn't allow recursion (but you can still call other recursive functions, and in particular you can use functions defined by letrec). This keyword has nothing to do with restricting the program, but rather to prevent accidental recursion due to having the same name.

[Serhii Khoma (srghma)]

Matt Diamond said:

Here's an example of how the type theory point of view and compiler point of view can come apart:

import Mathlib.Data.Nat.Basic

partial def loop (n : ℕ) : ℕ := loop n

def foo : ℕ := (loop 37) - (loop 37) + 37

-- we can prove foo is 37
example : foo = 37 := by simp [foo]

-- but we can't evaluate it
-- #eval foo

Your example is superb. (And sad. Because aren't we lying? As Aaron Liu said "from the type theory's point of view the function immediately halts with an arbitrary value")

How to fix it? Are there known or emerging advances in programming language theory which could help to join "type theory point of view and compiler point of view"

Maybe monadic/effect-based tracking of partiality? Cannot have partial def loop : N but only partial def loop : Partial N?

[Matt Diamond]

What behavior would you like to see in this case? Would you prefer that we can't prove foo = 37?

[Matt Diamond]

I'm not sure why you say we're lying... Aaron Liu didn't say that the function halts with a different arbitrary value each time, even when called with the same arguments

[Aaron Liu]

Serhii Khoma (srghma) said:

(And sad. Because aren't we lying? As Aaron Liu said "from the type theory's point of view the function immediately halts with an arbitrary value")

From the type theory point of view, loop is an arbitrary value of type ℕ → ℕ. And then foo is defined as loop 37 - loop 37 + 37. We can't show what value loop 37 is, but that doesn't matter here, because no matter what value it has loop 37 - loop 37 will be 0, and this is a property of subtraction on the natural numbers. Then foo = loop 37 - loop 37 + 37 = 0 + 37 = 37. So I'm not sure where you think the lying is.

[Serhii Khoma (srghma)]

Matt Diamond said:

What behavior would you like to see in this case? Would you prefer that we can't prove foo = 37?

No, it should prove.

Small infinity - same small infinity + 37 equals 37

[Matt Diamond]

I don't know what you mean by "small infinity" but loop 37 is not infinite (at least not in the type-theoretical sense)

[Matt Diamond]

perhaps what you're saying is that you'd like it to be infinite because it appears to be the "output" of an infinite loop?

[Aaron Liu]

you can't even prove loop 37 ≠ 0

[Aaron Liu]

it's completely arbitrary

[Aaron Liu]

but it's definitely a finite number

[Serhii Khoma (srghma)]

Aaron Liu said:

but it's definitely a finite number

Infinite loop results in finite number? In math? In our universe? Or just in lean? Wow, that should be deep insight about our universe. Could You tell more?

[Matt Diamond]

I see why you might think that, but it's not like the output of an infinite loop must be the number of times it ran.

What if the code was loop n = -loop n? Would that output positive infinity or negative infinity?
What if the code was loop n = 1 / loop n? Would that output zero? (Zero isn't infinite!)

[Matt Diamond]

Consider that the sum of 1 / n! as n goes to infinity (an infinite process of addition) is ultimately a finite number: the constant $e$

[Matt Diamond]

math is filled with instances where infinite processes have finite results when the result is evaluated "at the limit", so "infinite loop results in finite number" does happen often in math

[Aaron Liu]

Serhii Khoma (srghma) said:

Aaron Liu said:

but it's definitely a finite number

Infinite loop results in finite number? In math? In our universe? Or just in lean? Wow, that should be deep insight about our universe. Could You tell more?

It's not anything deep. It's just that the function is ℕ → ℕ, so when you plug in 37 : ℕ the output has to be a ℕ, and all ℕs are finite. There's no infinite processes going on here.

[Aaron Liu]

and it's definitely not evaluating any kind of infinite loop, or any loop at all

[Robin Arnez]

I think the fact that partial propagates also has to do with convenience. Usually, when writing partial functions, you'd expect the function to indeed terminate but you don't want to go through the work of adding termination proofs and preconditions and everything. So if you have some larger codebase and you've avoided calling partial functions until now but now you added a new function that you don't want to prove terminates and just use partial, you don't want to need to go through the entire codebase again adding partial to every function. So the compromise was just to make partial definitions opaque to proofs so you can't prove contradictory things with it, but also still make them exist as regular definitions so you can use them without needing to use partial.

[Serhii Khoma (srghma)]

Robin Arnez said:

I think the fact that partial propagates

You probably meant "doesn't propagate"

you don't want to need to go through the entire codebase again adding partial to every function

I want. I do want to separate wheat from chaff. Totally safe from maybe unsafe. Idris does this.

Aaron Liu said:

It's just that the function is ℕ → ℕ, so when you plug in 37 : ℕ the output has to be a ℕ, and all ℕs are finite.

So it's a lie. A lie that exists in lean only because our civilization is not developed enough and doesn't know how to type "infinitely looping functions". A lie that "loop returns number". If anything, it's more similar that it returns Partial Nat instead of Nat (inductive Partial a = DidntTermate | DidTerminate a; def loop (n : Nat) : Partial Nat := loop (n + 1)). This encoding too preserves the required loop n should not be equal to -loop n etc. But I don't know solution. I'm an amature.

[Matt Diamond]

personally I don't think the way Lean handles partial functions is related at all to the development of our civilization

[Matt Diamond]

though I'm sorry if the behavior of this software is causing you frustration... perhaps it's not ideal for your purposes

[Aaron Liu]

well that's just how partial works

Aaron Liu said:

from the type theory's point of view the function immediately halts with an arbitrary value, and this is why you need to prove Nonempty (so we know an arbitrary value exists, and adding the function as a constant to the type theory is sound).

[Aaron Liu]

sort of a compromise where it's not unsafe but you can't prove anything nontrivial about it

[Trebor Huang]

I think you're implicitly expecting partial to be keeping track of the side effects (which should be infective unless handled explicitly) instead of a keyword for the logical soundness. We know using partial functions is logically sound, so it doesn't need to be infective. Using axioms though are not, so we have commands to print the axioms a definition uses, which is indeed infective.

[Robin Arnez]

To be fair, it's not too hard to find out whether a function depends on a partial function, you can use #print opaques for this purpose:

import Batteries.Tactic.PrintOpaques

partial def ohNo (n : Nat) : Nat := ohNo n

def badDefinition (a : Nat) : Nat :=
  ohNo a + 2

/-- info: 'badDefinition' depends on opaque or partial definitions: [ohNo] -/
#guard_msgs in
#print opaques badDefinition

And if you wanted, you could also add attributes and linters and whatnot for yourself that provide errors when you use a partial function

[Mario Carneiro]

I think the better way to think of partial is not as a viral marker indicating a nontermination effect, as mentioned, but rather as a special kind of opaque. It is indicating that the body of the function is not provably equal to the function itself, and this property (of not equaling your body) is non-viral.

In fact, now that I say it, I think it might actually make sense to make partial def an error and force people to write partial opaque instead, to make this explicit.