Making a function's output type dependant on its input

Stream: new members

[VayusElytra]

Hi, I am curious how one can write functions which output things of completely different types depending on their input. Something of the sort, for instance:

def exampleFun (x : ℝ) :=
  if x ≤ 0 then
    ℕ
  else
    x

this expectedly throws a type mismatch error, since it is expecting to get something of type Type 0 but instead is given a real number. How do you deal with this?

[Henrik Böving]

You would return a custom inductive with cases for each usually.

Though this might be #xy

[VayusElytra]

Certainly, I can explain. I am trying to define a functor between two categories - the interval functor defined in section 4.1 of this paper by Bubenik and Scott.
This functor depends on a number of parameters (an interval I and real numbers a, b), which the type of the output depends on.

[Kyle Miller]

One almost-option is def exampleFun (x : ℝ) : if x ≤ 0 then Type else ℝ := ..., but this doesn't work because Type and ℝ are in different universes. (Even if it worked here, this is a pain to work with.)

[Kyle Miller]

I'm looking at section 4.1, and I'm not seeing what could need what you're doing with exampleFun. Could you explain your design so far and what definition you're working on formalizing?

[VayusElytra]

Sure, this was just a toy example to ask about the topic without introducing a ton of cumbersome notation (which I'd already written down in another thread, and I did not want to ask similar questions 20 times).

For a division ring F, these two definitions give the objects in ModuleCat F with carriers F and the 0-module, respectively:

def ZeroSubmod (F : Type u) [DivisionRing F] : ModuleCat.{u} F where
  carrier := PUnit.{u+1}

def SelfSubmod (F : Type u) [DivisionRing F] : ModuleCat.{u} F where
  carrier := F

This is the "object" part of the interval module defined in 4.1:

noncomputable def IntervalModuleObject (a b x : ℝ) (F : Type*) [DivisionRing F] : (ModuleCat F) :=
  if (a ≤ x ∧ x ≤ b) then
    (SelfSubmod F)
  else
    (ZeroSubmod F)

No issues here since both F itself and the trivial module are seen as objects of a single type, ModuleCat F.

This is what I am working with for the morphisms:

noncomputable def IntervalModuleMorphism (a b x y : ℝ) (h : x ≤ y) (F : Type)
  [DivisionRing F] :=
  if (a ≤ x ∧ y ≤ b) then
    𝟙 (SelfSubmod F)
  else if (y < a ∨ x > b) then
    𝟙 (ZeroSubmod F)
  else
    -- some other stuff that I will take care of after this issue is resolved.

Lean comes up with a type mismatch error here since 𝟙 (SelfSubmod F) and 𝟙 (ZeroSubmod F), the identity morphisms of the 0-module and F seen as elements of the category of modules over F, have different types. So if I understand right, I just need to define my own new type, which would correspond to "morphisms between F modules", and construct elements of that type corresponding to these morphisms in order for them to live in the same type, and so for Lean to accept my definition.

[Kyle Miller]

So if I understand right, I just need to define my own new type, which would correspond to "morphisms between F modules"

I don't think that's right. You're trying to make a morphism here in a pre-existing category (ModuleCat F), right? Wouldn't it be something like the following then?

noncomputable def IntervalModuleMorphism (a b x y : ℝ) (h : x ≤ y) (F : Type)
    [DivisionRing F] : IntervalModuleObject a b x F ⟶ IntervalModuleObject a b y F where
  ...

[VayusElytra]

Oh, that is a really good idea. I don't know why I didn't think of it :upside_down: thank you! I'll try it.