Default type arguments?

Stream: new members

[Adomas Baliuka]

I'm trying to use the Interval package and write functions/equations that can be interpreted as handling e.g. ℝ, or Interval as desired.

import Mathlib

-- this works.
variable {α : Type _} [Add α] [OfScientific α]
def f1 (a b : α) : α := a + b

#check f1 (1 : ℚ) (2 : ℚ) --  f1 1 2 : ℚ
#check f1 (1 : ℝ) (2 : ℝ) --  f1 1 2 : ℝ
#eval f1 1e0 2e0 --  3.000000 (of type `Float`)
-- one can force coercions to correct type by specifying output parameter
#check (f1 1e0 2e0 : ℚ) --  f1 1e0 2e0 : ℚ, where inputs are also rationals

I need lots of instances (Add, Mul, etc., but also e.g. Log, Exp, which I define myself).
I then compose compose a lot of functions like this.
Finally, I want to be able to easily change all occurrences of α at once in some final computation without explicitly changing the type of all inputs. My output type need not necessarily equal α, so the trick in the last line is not sufficient.

I tried to give the type argument a default value but it doesn't seem to work. Is there a way to achieve what I want? Ideally, I would not give explicit types to the input arguments at all, as in the last #check above.

-- this does not work. Can something similar work?
def f2 (β : Type _ := ℚ) [Add β] [OfScientific β] (a b : β) : β := a + b
#check f2 (1 : ℚ) (2 : ℚ)
-- application type mismatch
--   @f2 1
-- argument
--   1
-- has type
--   ℚ : Type
-- but is expected to have type
--   optParam Type ℚ : Type 1

#check f2 1e0 2e0
-- failed to synthesize
--   OfScientific Type
-- Additional diagnostic information may be available using the `set_option diagnostics true` command.

[Michal Wallace (tangentstorm)]

This seems to work:

def f2 {β} [Add β] [OfScientific β] (a b : β) : β := a + b
#check f2 (1 : ℚ) (2 : ℚ)
#check f2 1e0 2e0

[Eric Wieser]

I think the point was that Adomas Baliuka wants the second one to also mean ℚ

[Eric Wieser]

The reason default arguments don't work here is that they have to be last, I think

[Eric Wieser]

This works, but isn't the spelling you want:

import Mathlib

def f2 (β : Type _ := ℚ) [Add β] (a b : β) : β := a + b
#check f2 _ (1 : ℚ) (2 : ℚ)
#check f2 (a := 1) (b := 2)
#check f2 (a := 1e0) (b := 2e0)

[Adomas Baliuka]

Thanks! However, I'm confused. Why does this work but my version does not? The default argument in that example isn't last...

[Eric Wieser]

I guess I meant "last positionally-passed argument"