## Stream: new members

### Topic: Inverse of option.some

#### Bjørn Kjos-Hanssen (Jan 27 2022 at 05:17):

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 (Jan 27 2022 at 05:30):

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 (Jan 27 2022 at 05:33):

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 (Jan 30 2022 at 03:52):

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 (Jan 30 2022 at 04:07):

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 (Jan 30 2022 at 04:08):

also known as docs#option.iget

#### Jason Rute (Jan 30 2022 at 04:23):

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

#### Jason Rute (Jan 30 2022 at 04:25):

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 (Jan 30 2022 at 04:43):

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 (Jan 30 2022 at 04:50):

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 (Jan 30 2022 at 05:42):

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 (Jan 30 2022 at 06:08):

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

#### Bjørn Kjos-Hanssen (Jan 30 2022 at 06:21):

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

docs#part

#### Bjørn Kjos-Hanssen (Jan 30 2022 at 06:23):

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

#### Bjørn Kjos-Hanssen (Jan 30 2022 at 07:02):

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 (Jan 30 2022 at 17:34):

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 (Jan 30 2022 at 18:09):

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 (Jan 30 2022 at 18:33):

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 (Jan 30 2022 at 18:46):

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

#### Mario Carneiro (Jan 30 2022 at 20:37):

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 (Jan 30 2022 at 20:48):

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 (Jan 31 2022 at 03:50):

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

#### Bjørn Kjos-Hanssen (Jan 31 2022 at 04:10):

@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 (Jan 31 2022 at 04:18):

@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 (Jan 31 2022 at 04:30):

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

#### Bjørn Kjos-Hanssen (Jan 31 2022 at 06:04):

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 (Jan 31 2022 at 06:21):

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 (Jan 31 2022 at 06:24):

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 (Jan 31 2022 at 19:55):

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 (Jan 31 2022 at 20:47):

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 (Jan 31 2022 at 20:47):

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

#### Mario Carneiro (Jan 31 2022 at 21:29):

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 (Jan 31 2022 at 21:41):

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

#### Mario Carneiro (Jan 31 2022 at 21:53):

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 (Jan 31 2022 at 21:56):

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

#### Mario Carneiro (Jan 31 2022 at 22:00):

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 (Jan 31 2022 at 22:01):

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 (Jan 31 2022 at 22:33):

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)

Last updated: Dec 20 2023 at 11:08 UTC