monad for Sort?

Stream: general

[Kenny Lau]

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:

/-
Copyright (c) Luke Nelson and Jared Roesch. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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]

So why was everything defined only over Type u?

[Simon Hudon]

@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]

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

[Sebastian Ullrich]

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

[Kenny Lau]

what about nonempty being a monad?

[Kenny Lau]

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

[Kenny Lau]

it works under my code

[Kenny Lau]

yay, another PR to core