confused about types and Type

Stream: new members

[Nicolas Rouquette]

I noticed a similarity between:

(in Init/Control/State.lean)

universe u v w

def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
  σ → m (α × σ)

and:

(in Init/Prelude.lean)

universe u v w
...
/-- An implementation of [ReaderT](https://hackage.haskell.org/package/transformers-0.5.5.0/docs/Control-Monad-Trans-Reader.html#t:ReaderT) -/
def ReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
  ρ → m α

Based on https://leanprover.github.io/theorem_proving_in_lean4/dependent_type_theory.html, I read (α × σ) to be syntax for creating an instance of Prod; however, I can rewrite StateT` slightly differently like this:

universe u v w

def StateT' (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
  let p : Type u := α × σ
  σ → m p

Can someone explain how this use of product above differs from that in MonadStateOf.modifyGet:

(in Init/Prelude.lean)

class MonadStateOf (σ : Type u) (m : Type u → Type v) where
  /- Obtain the top-most State of a Monad stack. -/
  get : m σ
  /- Set the top-most State of a Monad stack. -/
  set : σ → m PUnit
  /- Map the top-most State of a Monad stack.

     Note: `modifyGet f` may be preferable to `do s <- get; let (a, s) := f s; put s; pure a`
     because the latter does not use the State linearly (without sufficient inlining). -/
  modifyGet {α : Type u} : (σ → Prod α σ) → m α

[Nicolas Rouquette]

Just to be clear, in the above, my brain fails to comprehend how the typechecker is OK with: let p : Type u := α × σ

[Kyle Miller]

It's ok because α × σ : Type u. Take a look at docs4#Prod, which says that given α : Type u and β : Type v then α × β : Type (max u v). For the particular example, there's a rule that Type (max u u) is Type u.

[Kyle Miller]

If you're wondering about Prod rather than using notation, by the way, it's because notation isn't introduced until here

[Kyle Miller]

When you say "I read (α × σ) to be syntax for creating an instance of Prod", it's not that it creating a Prod α σ, it's that it is Prod α σ. The notation to create a term of Prod α σ is (x, y). (The word "instance" isn't precise here.)

[Chris Bailey]

Nicolas Rouquette said:

Just to be clear, in the above, my brain fails to comprehend how the typechecker is OK with: let p : Type u := α × σ

This suggests you had a different type in mind, what were you expecting it to be?

[Nicolas Rouquette]

Thanks @Kyle Miller for your cogent explanation.

Chris Bailey said:

Nicolas Rouquette said:

Just to be clear, in the above, my brain fails to comprehend how the typechecker is OK with: let p : Type u := α × σ

This suggests you had a different type in mind, what were you expecting it to be?

Something like this:

def StateT'' (σ : Type u) (α : Type u) (m : (Prod σ α) → Type v) : Type (max u v) :=
  σ → m (α × σ)

This does not compute in Lean:

application type mismatch
  m (α × σ)
argument
  α × σ
has type
  Type u : Type (u + 1)
but is expected to have type
  σ × α : Type u

Although I understand @Kyle Miller 's explanation at a logical level, I have difficulty getting an intuitive understanding about the following:

• When different expressions that are structurally different yield the same type -- e..g. (α × σ) and α in the above have type Type u
• When structurally different expressions require a correspondingly specific type -- e.g. MonadStateOf.modifyGet argument must be a function of type σ → Prod α σ; it would be quite a different API if the argument where typed Prod α σ → σ.

[Chris Bailey]

Evergreen diagram: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20Prop.20.3A.3D.20Sort.200.20Motivation/near/252362723

[Nicolas Rouquette]

Kyle Miller said:

It's ok because α × σ : Type u. Take a look at docs4#Prod, which says that given α : Type u and β : Type v then α × β : Type (max u v). For the particular example, there's a rule that Type (max u u) is Type u.

Where is this rule?

Inspired by @Chris Bailey 's suggestion, I asked Lean for the type of various terms:

universe u v w

#check Type u → Type v
-- Type u → Type v : Type (max (u + 1) (v + 1))

#check Type u × Type u → Type v
-- Type u × Type u → Type v : Type (max (u + 1) (v + 1))

Although I couldn't find this rule; I hope we can use it show that these terms have the same type:

-- Can we prove that these two types are equivalent using the rule that Type (max u u) = Type u?
example : (Type u → Type v) = (Type u × Type u → Type v) := by
  sorry

[Kyle Miller]

With max u u, what you need to know is that u stands for a universe level variable, whose value is a natural number (not a Lean nat, but the natural numbers as part of the underlying theory), and like usual max u v is just the max of these two numbers. That's why max u u is u.

[Chris Bailey]

The rule about Type (max u u) is part of the type theory, for which people usually link Mario Carneiro's thesis as a reference. Said rule is on page 6. Definitional equality for elements of Sort is by antisymmetry on their universe level.

Your second example doesn't say what you think it does, it posits that (Type u → Type v) = (Type u × Type u → Type v) , not that their types are equal. What you're asking is basically this:

universe u v
#check (Type u → Type v) -- Type u → Type v : Type (max (u + 1) (v + 1))
#check (Type u × Type u → Type v) -- Type u × Type u → Type v : Type (max (u + 1) (v + 1))
example : Type (max (u + 1) (v + 1)) = Type (max (u + 1) (v + 1)) := by rfl

[Kyle Miller]

The statement (Type u → Type v) = (Type u × Type u → Type v) is not provable (so, as good as not being true), but since it typechecks it means the left-hand and right-hand sides have the exact same types.

[Nicolas Rouquette]

Hum.... let me try to explain the original problem differently.

In programming with Scala, it is very helpful to keep the Curry-Howard correspondence in mind: with reasonably-specified function signatures, one can focus on the types of the arguments and result to get an idea about what it can possibly do.

With Scala, CH might be perhaps simpler than with Lean because Scala has only types and terms whereas Lean4 has sorts, types and terms.

From this perspective, I am interested in understanding a small excerpt of functions defined in Lean's prelude and init library:

universe u v w

namespace confused

-- renamed the ρ argument to σ so as to emphasize the similarity with StateT.
def ReaderT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
  σ → m α

def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
  σ → m (α × σ)

end confused

First, I was really puzzled to see that ReaderT and StateT have the same kind of arguments yet their right-hand side terms are clearly different. Since these functions are defined over sorts, not types, it seems to suggest that it is more appropriate to compare their sort-based signatures. As @Kyle Miller explained: α × σ : Type u so both m α and m (α × σ) have the same sort Type v.

However, given that

#check Type u → Type v
-- Type u → Type v : Type (max (u + 1) (v + 1))

I would have expected the result to have type Type (max (u + 1) (v + 1)) instead of just Type (max u v). What am I missing here?

Second, it seems that it is crucial to appreciate the difference between sort and types when comparing α and α × σ.
Same sort: Type u; different types: α and α × σ.

Third, it seems that one can further constrain arguments/results in Lean4 as evidence in the difference between StateT.run and StateT.run':

universe u v w

namespace confused

def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
  σ → m (α × σ)

@[inline] def StateT.run {σ : Type u} {m : Type u → Type v} {α : Type u} (x : StateT σ m α) (s : σ) : m (α × σ) :=
  x s

@[inline] def StateT.run' {σ : Type u} {m : Type u → Type v} [Functor m] {α : Type u} (x : StateT σ m α) (s : σ) : m α :=
  (·.1) <$> x s

-- from Init/Control/Lawful.lean
@[simp] theorem run'_eq [Monad m] (x : StateT σ m α) (s : σ) : run' x s = (·.1) <$> run x s :=
  rfl

end confused

I am confused why StateT.run and StateT.run' have different types: m (α × σ) vs. m α.

I tried to copy the run'_eq theorem in this confused sandbox but I get errors that only increase my state of confusion:

-- about: run' x s
function expected at
  run'
term has type
  ?m.512

-- about: (·.1)
invalid field notation, type is not of the form (C ...) where C is a constant
  a✝
has type
  ?m.571

-- about: run x s
function expected at
  run
term has type
  ?m.546

Fourth, I managed to rewrite StateT.run' to make the functor explicit:

@[inline] def StateT.run'' {σ : Type u} {m : Type u → Type v} [F: Functor m] {α : Type u} (x : StateT σ m α) (s : σ) : m α :=
  let pair : m (α × σ) := x s
  F.map Prod.fst pair

I would have liked to make a variant of the run'_eq theorem for this but given that the mere copy/paste does not work; I am not sure how to proceed.

Fifth, assuming that StateT.run'' is equivalent to StateT.run', I would like to understand how it is possible that m appears in two different types:

• m α
• m (α × σ)

Is there a simple example of using StateT.run and StateT.run' that could help shed light on what kind of thing is m?

[Kyle Miller]

I would have expected the result to have type Type (max (u + 1) (v + 1)) instead of just Type (max u v). What am I missing here?

The definition of ReaderT has that σ → m α : Type (max u v), and your #check says that Type u → Type v : Type (max (u + 1) (v + 1)). There's nothing inconsistent here since in the first case you have the type of functions between types, and in the second you have the type of functions between universes (what you're calling sorts). (Universes are types, too, in Lean, so it makes sense to have functions between them.)

[Kyle Miller]

The difference between StateT.run and StateT.run' is that StateT.run' does fmap prod.fst (x s) rather than just x s (if I expanded out that notation correctly).

[Kyle Miller]

I tried to copy the run'_eq theorem

This doesn't work because the place you got it from was inside a namespace. Try changing run' and run to StateT.run and StateT.run', which hopefully is enough.

[Kyle Miller]

If you're getting really confused about type universes, I suggest that for now you just pretend that Type u is Type everywhere. The algorithm you were looking at earlier should still work under this assumption.

[Kyle Miller]

I believe that if you made your own copy of StateT and the rest with all the type universes replaced with Type it should all still work.

All this universe polymorphism isn't usually important when writing programs, but it's great that it's there when you need it.