yingtai

歴史

こうしてみると，関数型を集合論的な「関数全体の集合」としてみなすのはかなり問題がありそうです．いったん Haskell に寄り添って型が何を表しているか考えてみなければならないようです．Haskellを数学的に扱う際はこうした部分にトリックがあるわけです．

論理には飛躍はないけど、説明の飛躍があると思う。「トリック」があることを示唆するのなら、もう少し具体的に書くべきでは。あるいはこの段落を後ろに移すとか。

関数型についてはどうでしょうか？よく考えると，Double → Int がInt → Double の部分型になってくれたらうれしいです．

第 3 章、11-18ページまで。

Haskell は実用言語ですから利便性の問題がいろいろあります．そういうことを取っ払って，一番基本的な所にもどって考えると，関数型と代数的データ型さえあればかなり十分な気がします．

言いたいことはわかるけどもうちょっとこなれた表現にできそう。例えば:

Haskell は実用言語ですから、言語設計には利便性の問題が関わっています。とはいえ、そういう問題を一旦取っ払って、関数型と代数的データ型という一番基本的な所だけを考えても、十分さまざまな型を扱えます。

型なしラムダ計算の実装を第一回の宿題とします.
変数名付きのラムダ項が String で与えられるので, 評価した上で名無し項を String で返す eval 関数を実装してください.
具体的には次のような関数になります:

eval "(\\x. \\y. x) (\\x. x)" -- -> "(\\ (\\ 0))"

ひな形は Eval.hs です. Test.hs を実行することでテストできます.
成功した場合次のようになります:

hoge
import Data.List

main = do
  x <- getContents

print x

兼日題:

	import Eval (eval)
	results = [eval "(\\x. x) (\\x. x)" == "(\\ 0)",
	eval "(\\x. x x) (\\x. \\y. x)" == "(\\ (\\ (\\ 1)))",
	eval "(\\p. p (\\t. \\f. t)) ((\\f. \\s. \\b. b f s) (\\x. x) (\\x. \\y. x))" == "(\\ 0)",
	eval "(\\x. \\y. \\z. x z (y z)) (\\x. \\y. x) (\\x. \\y. x) (\\x. \\y. x)" == "(\\ (\\ 1))",
	eval "(\\m. m (\\x. \\t. \\f. f) (\\t. \\f. t)) ((\\n. \\s. \\z. s (n s z)) (\\s. \\z. s z))" == "(\\ (\\ 0))"]

	main = do
	let xs = filter (not . snd) $ zip [0..] results :: [(Int, Bool)]
	if null xs then putStrLn "OK"

	{-# LANGUAGE TemplateHaskell, DeriveFunctor, DeriveFoldable #-}

	import Prelude hiding (foldr)
	import Data.Foldable
	import Data.Thorn

	data Rose a = Leaf \| Rose a (Forest a)
	deriving (Functor, Show, Foldable)

	data Forest a = Forest [Rose a]