## Stream: general

#### Kenny Lau (Feb 18 2019 at 23:07):

the init.category library has Type u instead of Sort u everywhere: I did some experiments and literally just changed Type to Sort and no problems were found:

/-
Authors: Luke Nelson, Jared Roesch, Sebastian Ullrich, Leonardo de Moura
-/
prelude
import init.core init.function init.meta.name
open function
universes u v

class functor (f : Sort u → Sort v) : Sort (max (u+1) v) :=
(map : Π {α β : Sort u}, (α → β) → f α → f β)
(map_const : Π {α β : Sort u}, α → f β → f α := λ α β, map ∘ const β)

infixr  <$> :100 := functor.map infixr  <$ :100  := functor.map_const

@[reducible] def functor.map_const_rev {f : Sort u → Sort v} [functor f] {α β : Sort u} : f β → α → f α :=
λ a b, b <$a infixr $> :100  := functor.map_const_rev

class has_pure (f : Sort u → Sort v) :=
(pure {} {α : Sort u} : α → f α)

export has_pure (pure)

class has_seq (f : Sort u → Sort v) : Sort (max (u+1) v) :=
(seq  : Π {α β : Sort u}, f (α → β) → f α → f β)

infixl  <*> :60 := has_seq.seq

class has_seq_left (f : Sort u → Sort v) : Sort (max (u+1) v) :=
(seq_left : Π {α β : Sort u}, f α → f β → f α)

infixl  <* :60  := has_seq_left.seq_left

class has_seq_right (f : Sort u → Sort v) : Sort (max (u+1) v) :=
(seq_right : Π {α β : Sort u}, f α → f β → f β)

infixl  *> :60  := has_seq_right.seq_right

class applicative (f : Sort u → Sort v) extends functor f, has_pure f, has_seq f, has_seq_left f, has_seq_right f :=
(map       := λ _ _ x y, pure x <*> y)
(seq_left  := λ α β a b, const β <$> a <*> b) (seq_right := λ α β a b, const α id <$> a <*> b)

class has_bind (m : Sort u → Sort v) :=
(bind : Π {α β : Sort u}, m α → (α → m β) → m β)

export has_bind (bind)

@[inline] def has_bind.and_then {α β : Sort u} {m : Sort u → Sort v} [has_bind m] (x : m α) (y : m β) : m β :=
do x, y

infixl  >>= :55 := bind
infixl  >> :55  := has_bind.and_then

class monad (m : Sort u → Sort v) extends applicative m, has_bind m : Sort (max (u+1) v) :=
(map := λ α β f x, x >>= pure ∘ f)
(seq := λ α β f x, f >>= (<\$> x))

@[reducible, inline] def return {m : Sort u → Sort v} [monad m] {α : Sort u} : α → m α :=
pure

/- Identical to has_bind.and_then, but it is not inlined. -/
def has_bind.seq {α β : Sort u} {m : Sort u → Sort v} [has_bind m] (x : m α) (y : m β) : m β :=
do x, y


#### Kenny Lau (Feb 18 2019 at 23:07):

So why was everything defined only over Type u?

#### Simon Hudon (Feb 18 2019 at 23:22):

@Sebastian Ullrich Maybe you'd be able to enlighten us. My guess is that Sort* can make things more complicated when eliminating into Type*. It might have been necessary at some point and the decision was never reverted.

#### Sebastian Ullrich (Feb 18 2019 at 23:28):

I think most types in Sort* started in Type* until someone was able to come up with an example usage in Prop

#### Sebastian Ullrich (Feb 18 2019 at 23:29):

Also this file may be older than Sort. Not sure.

#### Kenny Lau (Feb 18 2019 at 23:29):

what about nonempty being a monad?

#### Kenny Lau (Feb 18 2019 at 23:31):

instance : monad nonempty.{u} :=
{ pure := @nonempty.intro,
bind := λ α β ⟨x⟩ f, f x }


#### Kenny Lau (Feb 18 2019 at 23:32):

it works under my code

#### Kenny Lau (Feb 18 2019 at 23:32):

yay, another PR to core

Last updated: May 12 2021 at 04:19 UTC