Zulip Chat Archive

Stream: general

Topic: monad for Sort?


view this post on Zulip 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:

/-
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

view this post on Zulip Kenny Lau (Feb 18 2019 at 23:07):

So why was everything defined only over Type u?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Sebastian Ullrich (Feb 18 2019 at 23:29):

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

view this post on Zulip Kenny Lau (Feb 18 2019 at 23:29):

what about nonempty being a monad?

view this post on Zulip Kenny Lau (Feb 18 2019 at 23:31):

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

view this post on Zulip Kenny Lau (Feb 18 2019 at 23:32):

it works under my code

view this post on Zulip Kenny Lau (Feb 18 2019 at 23:32):

yay, another PR to core


Last updated: May 12 2021 at 04:19 UTC