Riyo ymdfield

context: https://x.com/tomjaguarpaw/status/1917938120277872935

Let me share my understanding...

According to the definitions in the article, I think it's correct to say that there's little difference between referential transparency and purity, and thus there's not much need to use the word "pure" separately. However, at least in the discussions I've seen, the word "pure" is used in a different sense from the one defined in the article. As noted, the article doesn't define purity in terms of programs (i.e., code fragments) outside of functions.

To say that a program is pure means that it has no side effects. That is the definition of program purity as I understand it—and presumably the one that people are actually using. Side effects mean that a program changes the state of the external world, which refers to something outside the computation model officially defined by the Haskell language, or that it observes the state of the external world and alte

https://gist.github.com/ymdryo/f049a13e81ee22e76efb177f98cfcf1b

これを厳密に形式化するには、通信ポートで接続された2つのチューリングマシンを考えればよさそうです。片方はInternalという名前で、もうひとつはExternalという名前です。InternalがHaskell、Externalが外界に対応しています。通信ポートというのは、テープのあるビット（ヘッド位置0としましょう）について、そこに書き込むともう片方に反映されるという形での双方向通信です。メモリマップドIOです。ここで、Internalがポートに書き込む、これが副作用です。 Internalがポートを読む、これは副作用ではありませんが、Internalが特定の言語の計算モデルであるとき、参照透過性が崩れるとしたらここです。そして、このInternal/Externalをどう割り振るか（分界点をどこで分割するか）が立場により違う。

文脈: https://x.com/tomjaguarpaw/status/1917938120277872935

私の理解について話させてください…
この記事の定義に従うと、参照透過性と純粋性に大した違いはなく、わざわざ純粋という言葉を使う必要性は薄いというのは正しいと思います。
ただ、少なくとも私が見てきた議論では、純粋という言葉はこの記事の定義とは異なる意味で使われていると思います。指摘の通り、この記事は関数以外の、プログラム（あるコード断片）の純粋性について定義していませんし。

プログラムが純粋であるとは、それに副作用がないということです。これが、人々が使っているはずだと私が理解している、プログラムの純粋性の定義です。副作用とは、それが外界（言語「Haskell」が公式に定義する計算モデルの外部）の状態を変化させる、または外界の状態を受け取りそれに応じて以降の計算の進行を変化させるようなものです。参照透過性に由来する概念ではありません。ここで外界・内界の境界のどこに置くか、つまり「どこまでがHaskellなのか？」が問題になります¹。まさにこれが問題なのです。

https://x.com/ymdfield/status/1917966251462476100 ↩

	#!/usr/bin/env -S cabal run -v1
	{- cabal:
	build-depends: base, heftia-effects ^>= 0.7, unliftio
	ghc-options: -Wall
	-}
	{-# LANGUAGE GHC2021 #-}
	{-# LANGUAGE AllowAmbiguousTypes #-}
	{-# LANGUAGE BlockArguments #-}
	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE LambdaCase #-}

	// This code demonstrates that the issue in [hasura/eff#12](https://github.com/hasura/eff/issues/12)
	// exists not only in the `eff` library but generally in algebraic effects
	// without higher-order effects.
	//
	// This issue can be resolved by extending algebraic effects to higher-order
	// effects and defining `catch` as a higher-order effect. By running `runCatch`
	// after `runSome`, the interpretation of `catch` is delayed, ensuring that
	// exceptions are caught as expected.
	//
	// Please refer to this as well: https://github.com/sayo-hs/heftia?tab=readme-ov-file#semantics-zoo

	effect counter
	ctl increment() : ()
	ctl decrement() : ()
	ctl cnt() : int

	fun print-increment-print()
	cnt().println
	increment()
	cnt().println

	use std;

	effect State {
	get() Int
	put(Int) ()
	}

	let hState = handler {
	return(x) {
	fn(s: Int) {

	-- This Source Code Form is subject to the terms of the Mozilla Public
	-- License, v. 2.0. If a copy of the MPL was not distributed with this
	-- file, You can obtain one at https://mozilla.org/MPL/2.0/.

	main :: IO ()
	main = do
	putStrLn "[elaborateLocalThenShift]"
	elaborateLocalThenShift

	putStrLn ""

	callCC :: forall r m a. (Shift r <<: m, Monad m) => ((a -> m r) -> m a) -> m a
	callCC f = shift @r \k -> k =<< f (k >=> exit)

	exit :: (Shift r <<: m, Applicative m) => r -> m a
	exit r = shift \_ -> pure r

	elaborateShift ::
	(MonadFreer c fr, Union u, c (Eff u fr eh ef), HFunctor (u eh)) =>
	Eff u fr (Shift ': eh) ef ~> Eff u fr eh ef
	elaborateShift a =
	a & interpretKAllH_ pure \k ->
	(\(Shift f) -> elaborateShift $ f (raiseH . k))
	\|+: (k <=< injectH . hfmap elaborateShift)

	data Shift m a where
	Shift :: (forall (r :: Type). (a -> m r) -> m r) -> Shift m a

Riyo ymdfield

Footnotes