Inverse of option.some

Stream: new members

[Bjørn Kjos-Hanssen]

Given ox:option X with ∃ x : X, ox = some x, is there a way to access x without the quantifier? Something like x=some_inverse ox?

[Kyle Miller]

Connecting up a couple things from mathlib, there's this:

import data.option.basic

def extract (X : Type*) (ox : option X) (h : ∃ x : X, ox = some x) : X :=
begin
  rw ←option.is_some_iff_exists at h,
  exact option.get h,
end

[Kyle Miller]

A direct definition is quick though:

def extract {X : Type*} : Π (ox : option X), (∃ x : X, ox = some x) → X
| (some x) _ := x
| none h := false.elim $ by { cases h, contradiction }

[Bjørn Kjos-Hanssen]

Thanks... of course the quantifier is still there as an input to extract, but maybe it doesn't make sense to avoid it completely.

[Patrick Johnson]

You can remove the quantifier if you add inhabited

import data.option.basic

def extract {α : Type*} [inhabited α] : option α → α
| none := default
| (some x) := x

[Mario Carneiro]

also known as docs#option.iget

[Jason Rute]

There is also docs#option.get_or_else if you want to be more explicit about how to handle the none case.

[Jason Rute]

And docs#option.get is the original version of the question where you supply a proof of the option being a some (same as Kyle's extract).

[Jason Rute]

Also, I don't know what you are doing, but the standard way to deal with options is to keep everything inside options (or other monads) until the end. So instead of removing a value from an option, performing an operation on it, and putting it back, you can use doc#option.map , doc#option.orelse , and similar operations. Or if you are in a tactic monad, doing x <- oxworks and the none case just get's mapped to failure. (This works because the option is implicitly casted to a tactic.)

[Jason Rute]

This one is a bad idea, but if you are in meta land you can "solve" this with recursion. :smiling_devil:

meta def unsafe_get {α : Type*} : option α → α
| (some x) := x
| ox := unsafe_get ox

[Bjørn Kjos-Hanssen]

OK thanks everyone. Also, hi @Jason Rute good to see you on here. Actually I'm writing something about partial computable functions in computability theory and I figured they should have the type ℕ → option ℕ... or even option ℕ → option ℕ, to be able to compose them.

[Mario Carneiro]

The mathlib computability library uses functions ℕ → part ℕ (aka ℕ →. ℕ), using >>= to compose them.

[Bjørn Kjos-Hanssen]

Oh cool @Mario Carneiro where can I read about part types?

[Mario Carneiro]

docs#part

[Bjørn Kjos-Hanssen]

Good you told me that before I started some big project using option!

[Bjørn Kjos-Hanssen]

So for example the identity function, restricted to positive input, is

def identity_part : ℕ → part ℕ := λ  x, ⟨ x>0, λ h:x>0, x ⟩

[Bjørn Kjos-Hanssen]

I'm not sure if using >>= for composition is always the right choice. Depending on machine model, we may have constant functions that completely ignore their input, i.e., they output their constant even if their input is missing. In that case we want to say that the composition

const_c ∘ none = const_c

And there is another constant function const_c' that first looks at its input, satisfying

const_c' ∘ none = none

This distinction, if I understand >>= right, you can't make with just >>=?

[Bjørn Kjos-Hanssen]

This might not seem like a big deal since constant functions are computable... but the issue also arises for function f(x,y,z) such that for some inputs x_0, f(x_0,y,z) is a function of y only and ignores z, while for other inputs x_1, f(x_1,y,z) depends on z as well.

[Reid Barton]

This leads to domain theory, since for a more complicated type T the possible partial values may be more than just option T

[Bjørn Kjos-Hanssen]

Thanks @Reid Barton too bad I lost/sold my copy of Stoltenberg-Hansen's book

[Mario Carneiro]

The use of part is for computational models like turing machines or partial recursive functions where the input is always given explicitly, and the function represents the transformation from input to (maybe halting and) output. In order to have a function like part ℕ -> part ℕ (which you need to express functions like your ignoring-input constant function), the input has to be something more complicated than just a value, it has to come with some computational properties of its own such that "evaluation" to a value is a nontrivial operation that can possibly fail to halt. In a partial recursive function you would probably represent such an input as "code-as-data", i.e. a code that can be evaluated to get a value, in which case your (higher order) program has a type like code -> part ℕ instead

[Bjørn Kjos-Hanssen]

An example where the input need not be given explicitly to a Turing machine is when you prove that the composition of two partial recursive functions is partial recursive. Then in the computation of f(g(x)) we may wait for the computation of g(x) to finish before looking at it as input to f. And if f is a constant function, we may (depending on the TM model used) choose to not look at the output tape containing g(x) at all.

[Patrick Johnson]

too bad I lost/sold my copy of Stoltenberg-Hansen's book

You're talking about "Mathematical Theory of Domains"? Why don't you just download it from the internet?

[Bjørn Kjos-Hanssen]

@Patrick Johnson I only get "We recognised you are associated with one or more institutions that don’t have access to this content."

[Patrick Johnson]

@Bjørn Kjos-Hanssen I can give you PDF for free if you want.

@Mario Carneiro I remember we were discussing about this and the conclusion was that we are not allowed to post proprietary PDFs to public streams. Are we allowed to send PDFs in private messages?

[Mario Carneiro]

that should be fine, the rules there are the same as for e.g. emailing it

[Bjørn Kjos-Hanssen]

Thanks @Patrick Johnson Haven't looked at this for decades but I guess option ℕ is the same as the flat cpo ℕ_⊥ in example 1.11...

[Mario Carneiro]

Bjørn Kjos-Hanssen said:

An example where the input need not be given explicitly to a Turing machine is when you prove that the composition of two partial recursive functions is partial recursive. Then in the computation of f(g(x)) we may wait for the computation of g(x) to finish before looking at it as input to f. And if f is a constant function, we may (depending on the TM model used) choose to not look at the output tape containing g(x) at all.

I'm not sure I follow. The composition of partial functions is defined using >>= so it seems not to hit any issues with f skipping g

[Mario Carneiro]

That is, a partial recursive function is by definition an element of nat -> part nat, and composition of partial recursive functions f and g is by definition \lam x, g x >>= f, so the nature of the question has already excluded the possibility of g not getting evaluated

[Bjørn Kjos-Hanssen]

What I mean is that if we use option types, we are permitted to have f none = 5 say... and that may be desirable for the constant function 5. But with part we cannot have such behavior, right?

[Patrick Johnson]

Why do you think we cannot have such behavior with part? The only difference between option and part is that determining whether an option is none or some is always decidable. Note that (>>=) is a monadic operator. It "lifts" operations on values to operations on option/part types. But you don't need to use it to compose functions, you can work with monads directly.

def f₁ (p : option ℕ) : option ℕ := p >>= λ n, option.some 5
example : f₁ option.none = option.none := by simp [f₁]

def f₂ (p : option ℕ) : option ℕ := option.some 5
example : f₂ option.none = option.some 5 := rfl

def g₁ (p : part ℕ) : part ℕ := p >>= λ n, part.some 5
example : g₁ part.none = part.none := by simp [g₁]

def g₂ (p : part ℕ) : part ℕ := part.some 5
example : g₂ part.none = part.some 5 := rfl

[Patrick Johnson]

Whether it is desirable depends on your model of computable functions, I guess.

[Mario Carneiro]

Bjørn Kjos-Hanssen said:

What I mean is that if we use option types, we are permitted to have f none = 5 say... and that may be desirable for the constant function 5. But with part we cannot have such behavior, right?

The constant function 5 would be defined as f := \lam _, part.some 5. This is a function nat -> part nat, which always ignores its argument and returns 5. If we compose this with the function g := \lam _, part.nonerepresenting a computation that always diverges, we get (g x >>= f) = (none >>= f) = none, that is, the computation diverges, because we evaluate g first and pass the result to f, and since g never returns f never gets to run.

As Patrick says this has nothing to do with part vs option. You can say exactly the same thing if you replace part with option in the above. The key point is that partial functions have the type nat -> part nat and not part nat -> part nat. Functions in this latter form can choose not to evaluate their arguments, and they also compose (by regular function composition), but they aren't partial functions in the traditional sense.

[Reid Barton]

They can also do weird things like be defined exactly when their input isn't defined.

[Mario Carneiro]

That is actually one difference between part and option. With part, you can't define a computable function that is not monotonic w.r.t the part order, but with option you can

[Reid Barton]

You can still do something like f x := { dom := not x.dom, get := \lam _, 1 }

[Mario Carneiro]

ah right, I take it back. You can maybe salvage a statement like that if you stick to the combinators but that's a much weaker statement

[Mario Carneiro]

there is a subset of part consisting of dom predicates that are Sigma_1, which is more relevant to use in partial computable functions, which should have the expected property, but defining this correctly in lean is tricky

[Bjørn Kjos-Hanssen]

Mario Carneiro said:

That is actually one difference between part and option. With part, you can't define a computable function that is not monotonic w.r.t the part order, but with option you can

OK great, this makes me want to use part after all... (even if there's a caveat as @Reid Barton said)