# Zulip Chat Archive

## Stream: new members

### Topic: confused about types and Type

#### Nicolas Rouquette (Jul 18 2022 at 23:19):

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 (Jul 18 2022 at 23:21):

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

#### Kyle Miller (Jul 18 2022 at 23:27):

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 (Jul 18 2022 at 23:28):

If you're wondering about `Prod`

rather than using notation, by the way, it's because notation isn't introduced until here

#### Kyle Miller (Jul 18 2022 at 23:30):

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 (Jul 18 2022 at 23:43):

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 (Jul 19 2022 at 00:01):

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 (Jul 19 2022 at 00:19):

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 (Jul 19 2022 at 18:18):

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 (Jul 19 2022 at 18:45):

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 (Jul 19 2022 at 18:47):

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 (Jul 19 2022 at 18:47):

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 (Jul 20 2022 at 22:19):

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 (Jul 20 2022 at 22:23):

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 (Jul 20 2022 at 22:27):

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 (Jul 20 2022 at 22:28):

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 (Jul 20 2022 at 22:30):

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 (Jul 20 2022 at 22:32):

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.

Last updated: Dec 20 2023 at 11:08 UTC