append :: [a] %1 -> [a] %1 -> [a] append = fold f where f :: Maybe (a, [a] %1 -> [a]) %1 -> ([a] %1 -> [a]) f Nothing = \xs -> xs f (Just (x, g)) = \xs -> x : g xs

もちろん、こういう定義は可能だけれど。

Linear Haskell で foldr を (a %1 -> b %1 -> b) -> b %1 -> [a] %1 -> b という型で定義すれば、append :: [a] %1 -> [a] %1 -> [a] を foldr (:) ys xs で定義できるけど、 (Maybe (a, b) %1 -> b) -> [a] %1 -> b という型の fold からは、appendを同じようには定義できないんだなぁ。

投稿サイトがオープンしていた。 www.cril.univ-artois.fr/PB26/

x.com/__pandaman64...

一方で、最後の「_ = n + 1 := by rfl」(.succ n = n + 1 のステップ)を消してもエラーにならないのは何でだろう。 こちらも「definitionally equal だけど式の形は違う」という同じパターンに思えるが……

コード4.26： LeanBook/NatCommMonoid/Simp.lean 1 example (n : MyNat) : 1 + n = n + 1 := calc 2 _ = .succ 0 + n := by rfl -- 1 は定義から.succ 0 に等しい 3 _ = .succ (0 + n) := by rw [MyNat.succ_add] -- .succ を外に出す 4 _ = .succ n := by rw [MyNat.zero_add] -- 0 + n = n を使って単純化 5 _ = n + 1 := by rfl -- n + 1 は定義から.succ n に等しい

最初の「_ = .succ 0 + n := by rfl」(1 + n = .succ 0 + n のステップ)を消すとエラーになるのは何でだろう。

Agdaで等式推論する場合には、 definitionally equal な式は区別しない(できない)ので、それを変形するステップは書かなくても問題ない(分かりやすさのために書くことはある)けど、Leanだと tactic の観点からは区別されることがある?

ゼロから始めるLean言語入門 ― 手を動かして学ぶ形式数学ライブラリ開発 lambdanote.com/products/lea... p.74

Pathetic.
gift link
wapo.st/4ccudpF

コード4.25： LeanBook/NatCommMonoid/Simp.lean 1 example (m n : MyNat) : .succ m + n = .succ (m + n) := by 2 induction n with 3 | zero => rfl 4 -- n = n' のケースまで示せていたと仮定して、n = n'.succ のケースを示す 5 | succ n' ih => calc 6 _ = (m.succ + n').succ := by rw [MyNat.add_succ] -- 左辺を _ で省略すると、 7 -- ゴールの左辺だと認識される 8 _ = (m + n').succ.succ := by rw [MyNat.succ_add] -- 左辺は同じなので_ で省略できる 9 _ = (m + n'.succ).succ := by rw [MyNat.add_succ]

おお、 Lean でも Agda みたいに等式推論のスタイルで証明を書けるんだ。この証明自体は、帰納法の仮定を使わず、最終的なゴールと同じ命題が帰納法を使って既に証明済みで、それを使うという流れで草だけど。

ゼロから始めるLean言語入門 ― 手を動かして学ぶ形式数学ライブラリ開発 www.lambdanote.com/products/lea... p.74

CW2011 continuation workshop 2011 & tutorial session.

Togetter
posfie.com/@MoCo7/p/vIK...

Partake
web.archive.org/web/20111029...

自分は結局参加しなかったんだっけかなぁ…… #cw2011 #cont2011

そういえば、Control.Monad.Trans.Cont のドキュメントに「Delimited continuation operators are taken from Kenichi Asai and Oleg Kiselyov's tutorial at CW 2011, "Introduction to programming with shift and reset" (okmij.org/ftp/continua... ).」とか書いてあるじゃん。 #cw2011 #cont2011

record selector ではなく別の関数として定義すれば良いんだけどさぁ……

downloads.haskell.org/~ghc/9.14.1/... にも “The projection function for a record with a single linear field should be multiplicity-polymorphic; currently it’s unrestricted.” と書かれている。

Linear Haskell 、newtype State s a = State{ runState :: s %1 -> (a, s) } みたいなのを書いた時に record selector である runState の型が State s a %1 -> s %1 -> (a, s) ではなく State s a -> s %1 -> (a, s) になってしまうの、微妙に面倒くさい。 #Haskell

GitHub - itnef/smtx: My first SMT solver (only QF_UF) My first SMT solver (only QF_UF). Contribute to itnef/smtx development by creating an account on GitHub.

#Haskell で書かれた簡単なSMTソルバっぽい。 QF_UF のみをサポート。
github.com/itnef/smtx

Definition 7 We write ?A ("why not A") for (!A^⊥)^⊥. Computationally, we interpret the isomorphism (A^⊥)^⊥ ≅ A as "a continuation t accepting an A-accepting continuation k must eventually apply k to some A-typed value a." But ?A represents a continuation t that accepts a continuation k which it may freely discard or copy. Thus, evaluation of a ?A-typed term may never return, or it may return multiple times to the same point with different values.

上述のスレッドでも参照されていた Filinski の Linear continuations を読んだ。dualizing object ⊥があって、 A^⊥=A⊸⊥ を継続と解釈できる設定だと、 A≅(A⊸⊥)⊸⊥ は線形性から継続を必ず呼び出さないといけないけど、?A≅(!(A⊸⊥)⊸⊥) は継続の破棄や複製が許されるので、リターンしなかったり複数回リターンすることが許容される。
doi.org/10.1145/1431...

Claude Code Source Map Leak, What Was Exposed and What It Means Claude Code became a security story because public reports said a source map in its npm distribution was enough to reconstruct readable source. Here is what was likely exposed, what remains unconfirme...

Claude Code Source Map Leak, What Was Exposed and What It Means 👀
www.penligent.ai/hackinglabs/...

Mac 版です！
なぜかデンマークでだけ売れてます。

Meaning of the "why not" modality from linear type theory? In linear type theory there is a modality written ! where !T can be read as "infinite copies of T". According to ncatlab, there is a dual to this modality which is sometimes written ?T and referre...

Meaning of the "why not" modality from linear type theory?
cs.stackexchange.com/questions/10...

What is the intuition behind the "par" operator in linear logic? I'm $\DeclareMathOperator{\par}{\unicode{8523}}$ trying to wrap my mind around the $\par$ ("par") operator of linear logic. The other connectives have simple resource interpretations ($A\otimes B...

What is the intuition behind the "par" operator in linear logic?
math.stackexchange.com/questions/50...

sandbox/LinearLogic.hs at 54537bbadefafa23bc2590a08f560d968dad884d · msakai/sandbox My sandbox repository. Contribute to msakai/sandbox development by creating an account on GitHub.

線形論理の論理結合子を Linear Haskell で解釈しようとしてて、自分が ⅋ (par), ⊥ (bottom), ? (why not) の計算的な意味を直観的に理解できていないことに気が付いた。 特に、命題を資源として解釈する解釈で、これらを自然に解釈することって出来るの? #Haskell
github.com/msakai/sandb...

sandbox/LinearLogic.hs at 54537bbadefafa23bc2590a08f560d968dad884d · msakai/sandbox My sandbox repository. Contribute to msakai/sandbox development by creating an account on GitHub.

逆に、 & が欲しい場合には、 ⊕との双対性を使って定義することになる?
github.com/msakai/sandb...

Linear Haskell 、→ の代わりに ⊸ を考えた瞬間に、タプルが & ではなく ⊗ のように振る舞うの、データ構築子の矢印が → ではなく ⊸ で定義されていることの帰結だと思うんだけど、面白いな。 #Haskell

7.2 Extending Multiplicities For the sake of this article, we use only multiplicities 1 and ω. But in fact λ^q_→ can readily be extended to more, following Ghica and Smith [2014] and McBride [2016]. The general setting for λ^q_→ is an ordered-semiring of multiplicities (with a join operation for type inference). In particular, in order to support dependent types, McBride needs a 0 multiplicity. We may also want to add a multiplicity for affine arguments (i.e. arguments which can be used at most once).

Linear Haskell: practical linearity in a higher-order polymorphic language の FUTURE WORK に、 0 や affine への拡張の可能性について書いてあった。
doi.org/10.1145/3158...

LinearTypes: Spurious multiplicity error when wrapping an empty-case lambda in a data/newtype constructor (#27117) · Issues · Glasgow Haskell Compiler / GHC · GitLab Summary When using -XLinearTypes and -XEmptyCase, a lambda that eliminates Void via case void of {} type-checks...

Linear Haskell 使ってたら、早速変なコーナーケースを踏んだので、報告。 #haskell
gitlab.haskell.org/ghc/ghc/-/is...

data Normal a where Normal :: a %1 -> (a %1 -> ()) -> (a %1 -> (a, a)) -> Normal a data Linear a where Linear :: a %1 -> Linear a data Affine a where Affine :: a %1 -> (a %1 -> ()) -> Affine a data Relevant a where Relevant :: a %1 -> (a %1 -> (a, a)) -> Relevant a

Linear Haskell 面白いね。Multiplicity に One (1回消費) と Many (任意回消費) しかなくて、Affine (高々一回の消費) や Relevant (一回以上の消費) がなくて良いのかなと思ったけど、これは破棄や複製の関数を一緒にパッキングしてあげれば表現できるから？ #haskell
github.com/msakai/sandb...

また、 kan-extensions の Control.Monad.Codensity にも同様の実装がある。 ただ、これらは answer type modification がないので、表現力が限定されていると思うけど。
hackage-content.haskell.org/package/kan-...

Control.Monad.ContのMonadCont は call/cc を持つモナドという抽象化なので、call/ccによらず実装されている shift/resetは公開されていないのだろう。
hackage-content.haskell.org/package/mtl-...

そういえば、mtlのControl.Monad.Contを使っていると気づかないけど、transformersのControl.Monad.Trans.Contには限定継続のshift/resetが一応あるんだな。 #haskell
hackage-content.haskell.org/package/tran...

Microsoft Hasn’t Had a Coherent GUI Strategy Since Petzold A few years ago I was in a meeting with developers and someone asked a simple question: “What’s the right framework for a new Windows desktop app?” Dead silence. One person sugges…

かつてMSでPowerShellを生み出した方が、WindowsのGUI開発プラットフォームの方針が十数年にわたってころころ変わり続け、未だに混乱している内情について語っているこのblogが話題になっている。Windows開発チームと.NET開発チームの対立のような社内政治の要因が大きかったと。MSは社内の開発チーム同士の対立が激しいというのは結構有名な話やね。

ただ著者が.NET陣営だけにちょっとWPFやSilverlightに対して甘いかなとは思う。技術的な筋は良かったけど完成度が中々上がらなかったのは確かやしね。
www.jsnover.com/blog/2026/03...

そういえば、 SLACS 2003 で @ichirohasuo.bsky.social さんの Modal logics for coalgebras の話を聞いたのとかも、もう20年以上前なのか……
www.math.s.chiba-u.ac.jp/SLACS/slacs2...

この問題はどこに行き着くんだろうね。学生の指導はともかく、機材メンテとかは流石に専用の人雇う方が結果的に安上がりになるんじゃないかと、ずっと米国の現場でそう言う研究に関わる非研究者として見てきた人間として思うけど。

biomedcircus.com/research_02_...