https://x.com/rizkubo/status/2013122492244611503
↑ のポストへの返信を、読みやすいようにマークアップしたものです。
こちらも妥当な質問だと思います。まず主張をもう少し明確にさせてください。
まず、「for/doは[...]脱糖してるだけ」はその通りです。しかし、「プログラムの実行をある程度許して」というのは、for/doがプログラムの実行をする、と言いたかったのではなく、「自由でない >>= 演算が、一般に、なんらかの意味で部分的にプログラムを実行しており」「そういう、プログラムを部分的に実行するような >>= 演算についても合成を書きやすくするのが for/do という構文だ」「だから、for/do はそういう意味で .replaceExits の一般化になっている」という立場があり得るというのが僕の主張でした。
| enum Executable[Instr[_], ExitCode]: | |
| case Exit[I[_], EC]( | |
| code: EC | |
| ) extends Executable[I, EC] | |
| case NonEmpty[I[_], BranchIndex, EC]( | |
| headInstruction: I[BranchIndex], | |
| branches: BranchIndex => Executable[I, EC] | |
| ) extends Executable[I, EC] | |
| import Executable.* |
| -- Adapted encodings from https://dl.acm.org/doi/pdf/10.1145/3571255 | |
| structure EffectSet (AbstractState : Type) : Type 1 where | |
| Ops : (precondition : AbstractState → Prop) → Type | |
| Ret : (precondition : AbstractState → Prop) → Ops precondition → Type | |
| Transition : (precondition : AbstractState → Prop) → Ops precondition → (AbstractState → Prop) | |
| inductive HoareFreer (AbstractState : Type) (es : EffectSet AbstractState) : | |
| (precondition : AbstractState → Prop) → (postcondition : AbstractState → Prop) → (result : Type) → Type 1 where | |
| | End : {result : Type} → {condition : AbstractState → Prop} → | |
| (res : result) → HoareFreer AbstractState es condition condition result |
| structure ApApplicative (F : Type u → Type v) where | |
| ---- 型クラスが提供する演算 | |
| pure : a → F a | |
| ap : F (a → b) → F a → F b | |
| ---- 拡張関数 | |
| map : (a → b) → F a → F b | |
| mapDefn : map f fa = ap (pure f) fa | |
| ---- 則 |
| type Not[A] = A => Nothing | |
| type ~[A] = Not[A] | |
| infix type ×[A, B] = (A, B) | |
| infix type +[A, B] = Either[A, B] | |
| infix type ↔[A, B] = (A => B) × (B => A) | |
| def a_i[P]: ~[P × ~[P]] = p_np => { | |
| val (p, np) = p_np | |
| np(p) | |
| } |
| //> using options -deprecation -feature -unchecked -Xfatal-warnings -no-indent -Xkind-projector:underscores | |
| //> using dep "org.typelevel::cats-core::2.12.0" | |
| import cats.data.NonEmptyVector | |
| import cats.syntax.all.* | |
| import cats.instances.string | |
| import cats.kernel.Semigroup | |
| case class XZInt2(x: Int, z: Int) | |
| case class Int3(x: Int, y: Int, z: Int) |
| //--- | |
| // laws defined in cats typeclasses | |
| // typeclasses: https://github.com/typelevel/cats/tree/29dd05a0282f51fda2e0f7d936250d6c0275bcf2/core/src/main/scala/cats | |
| // laws: https://github.com/typelevel/cats/tree/29dd05a0282f51fda2e0f7d936250d6c0275bcf2/laws/src/main/scala/cats/laws | |
| Functor => FunctorLaws#covariantIdentity := | |
| fa.map(identity) | |
| <-> fa | |
| Functor => FunctorLaws#covariantComposition := |
| package io.github.kory33.tracing_instrument.example | |
| import io.github.kory33.tracing_instrument.otel4s.methodSpan | |
| import io.github.kory33.tracing_instrument.experimental.otel4s.instrumentF | |
| import scala.annotation.experimental | |
| object example { | |
| import cats.Monad | |
| import cats.effect.Ref | |
| import cats.syntax.flatMap._ |
| // TODO! | |
| @main def main(): Unit = ??? |
