functions that call partial functions not have to be partial

Stream: new members

[Asei Inoue]

Why do functions that call partial functions not have to be partial?

partial def foo (x : Nat) : Nat := foo x

-- `bar` does not have to be marked as `partial`
def bar (x : Nat) := foo x

[Asei Inoue]

Functions that call unsafe function have to be marked as unsafe. What is the reason for this difference in behaviour between partial and unsafe?

/-
(kernel) invalid declaration, it uses unsafe declaration 'ptrAddrUnsafe'
-/
def fibonacci (n : Nat) : Array Nat := Id.run do
  let mut fib : Array Nat := Array.mkEmpty n
  fib := fib.push 0
  fib := fib.push 1
  for i in [2:n] do
    dbg_trace ptrAddrUnsafe fib
    fib := fib.push (fib[i-1]! + fib[i-2]!)
  return fib

Intuitively, functions that call partial functions should be marked as partial because they cannot be guaranteed to terminate.

[Mario Carneiro]

The name is a bit of a misnomer, it is not a viral marker for partiality (as you have observed). Rather, it is a special variant of opaque for compiling general recursive functions. When you see partial def foo, this means that foo cannot be unfolded to the thing on the other side of the :=.

[Asei Inoue]

Thank you.

this means that foo cannot be unfolded to the thing on the other side of the :=.

What this means? Definitions marked as partial can be reduced as following: (opaque marked definition can't be reduced)

partial def foo : Nat := 123

/-- info: 123 -/
#guard_msgs in #eval foo

/-- info: 123 -/
#guard_msgs in #reduce foo

opaque bar : String := "hello"

/-- info: bar -/
#guard_msgs in #reduce bar

[Mario Carneiro]

It seems lean ignores partial on definitions that are not recursive. I guess that muddies the mental model a bit...

[Asei Inoue]

It might be better to make an error if you mark a non-recursive function as partial...

[Damiano Testa]

Maybe there is the need for an unused partial linter. :smile:

[Asei Inoue]

Is it difficult to express information about whether a function stops or not at type level, which I hear is possible in the language such as koka?

[Asei Inoue]

I think this is related to algebraic effect... I think algebraic effect enables total/partial check in type theory...

[Asei Inoue]

Among other theorem proving support systems, F star seems to support algebraic effect; is it difficult to implement in Lean?

[Henrik Böving]

Having an efficient implementation of algebraic effects requires lots of investment in the compiler and runtime that we are most likely not going to undertake in the near future (potentially never).

Tracking non termination globally is not an issue, we can make partial viral, it was merely decided not to do this. This does have a nice benefit which is that you can still prove things about functions that call partial functions but are not themselves marked as partial.

[Henrik Böving]

Note that partial is also not a primitive of the system, it is a feature that comes from the combination of unsafe, opaque and implemented_by, so even if we were to make partial viral you do still not have a guarantee that your functions terminate, simply because people can imitate partial on their own.

[Kyle Miller]

Asei Inoue said:

Functions that call unsafe function have to be marked as unsafe.

Note that it's possible to call unsafe functions indirectly using opaque/@[implemented_by] to "launder" the fact that it's unsafe. You have to be very careful with doing this though because then the burden is on you to convince yourself that what you're doing is actually safe.

The unsafe ... term is a way to do this whole thing automatically:

def fibonacci (n : Nat) : Array Nat := Id.run do
  let mut fib : Array Nat := Array.mkEmpty n
  fib := fib.push 0
  fib := fib.push 1
  for i in [2:n] do
    dbg_trace unsafe ptrAddrUnsafe fib
    fib := fib.push (fib[i-1]! + fib[i-2]!)
  return fib

This is more-or-less safe here because dbg_trace unsafe ptrAddrUnsafe fib doesn't functionally affect what fibonacci does.

[Kyle Miller]

You can even prove things about this fibonacci function. Here's an indirect proof of that claim:

def fibonacci (n : Nat) : Array Nat := Id.run do
  let mut fib : Array Nat := Array.mkEmpty n
  fib := fib.push 0
  fib := fib.push 1
  for i in [2:n] do
    dbg_trace unsafe ptrAddrUnsafe fib
    fib := fib.push (fib[i-1]! + fib[i-2]!)
  return fib

def fibonacci' (n : Nat) : Array Nat := Id.run do
  let mut fib : Array Nat := Array.mkEmpty n
  fib := fib.push 0
  fib := fib.push 1
  for i in [2:n] do
    fib := fib.push (fib[i-1]! + fib[i-2]!)
  return fib

example : fibonacci = fibonacci' := rfl