狠狠撸

Clean の機能遅延評価自動カリー化型クラス代数的データ構造 Milner/Mycroft に基づく型システムマクロ一意型総称型ダイナミック

だいたい Haskell と一緒

一意型副作用を実現しつつ参照透明性を保証するため

参照透明性って関数と引数の組み合わせが一緒なら結果は常に同じ！ f x = x + 1 なら <f,x=2> なら必ず 2 をかえす a = 3 なら必ず a は 3 a = 3;a = a+1; 結果が同じじゃなくなる！参照透明性が保証されない！

シャドーイング + 再束縛ならおｋ ? let a = 3 in ? let a = a + 1 ならおｋじゃね？

問題 let a1 = fread f ?:: String let f = fwrite 'a' f :: File let a2 = fread f ?:: String a1 == a2 <false> 一行目と三行目の結果が違う！参照透明性が壊れる！ ?

? ファルス ! ※ フォールスです

? a1 が参照できなけばおｋそれが一意型

一意型のアイディア破壊的更新をしても観察できなければおｋ破壊的更新をした後に前の参照を持たなければおｋ

一意型をつかった例 WriteAB :: *File -> File? WriteAB file = fileAB? where fileA = fwritec 'a' file? ? fileAB = fwritec 'b' fileA

一意型の例 AppendAB :: *File -> (File, File)? AppendAB file = (fileA, fileB)? where fileA = fwritec 'a' file? ? fileB = fwritec 'b' file < エラーになる > Uniqueness error [tak.icl,23,AppendAB]:?"file" demanded attribute cannot be offered by shared object

なぜエラーになったか file に対する参照が二つ一意型は object に対する参照が一つでないといけない

最初のれどのように簡約されるのか

次の例 file に対して参照が二つあるのダメ

こういう風にも書ける WriteAB :: *File -> File? WriteAB file? ? # file = fwritec 'a' file? ? # file = fwritec 'b'? file = file 命令型みたいにこういう風にもかけます。

なにが言いたいか命令型のプログラマは同じ事を頭の中でやっている !

GUI module hello import StdEnv, StdIO Start :: *World -> *World Start world = startIO NDI Void (snd o openDialog undef hello) [] world where hello = Dialog "" (TextControl "Hello world!" [])? ? ? ? ? ? ? ? ? [WindowClose (noLS closeProcess)]

全称量化子 :: T2 b = C2 (b: b -> b) 　　　　 --?×? :: T2 b = C2 (A.b: b -> b) ? ? ? ? ? ?-- ? f2:: (T2 b) -> (Int,Char) f2 (C2 g) = (g 1, g 'a') たぶん Haskell と同じなので言うことは特にない…

存在量化子 :: List = E.a: Cons a List | Nil newlist = Cons 1 Nil Hd :: List -> ? // 静的に型付けできない Hd (Cons x xs) = x // コンパイルエラーになる Tl :: List -> List //OK Tl (Cons x xs) = xs 取り出す方法がない隠蔽された状態を表現可能

配列リストと配列の変換 NewArray = {elem elem <- ListA}NewList = {elem elem <-: ArrayA} 配列の更新 {Array5 & [i]=2*i+1 i <- [0..4]} // 配列の更新 {1,3,5,7,9} を出力する配列のパターン CopyFirst j a=:{[0]=a0} = {a & [j] = a0}

マクロ　 :: Color :== Int 　 Black :== 1 　 White :== 0 　 invert :: Color -> Color 　 invert Black = White 　 invert White = Black

総称プログラミングめんどくさいんで記事

項グラフ書き換 Clean の意味論は項グラフ書き換 Clean のプログラムは Start から始まるグラフ関数はグラフ書き換え規則グラフに対してグラフ書き換え規則を適用するのが計算グラフ書き換えが出来なくなったものを正規形

? Start :: Int? Start = Length [3,4]? ? Length :: [x] -> Int? Length [a:x] = 1 + Length x? Length [] = 0

? Start ||a: ? ? ? ? ? ? ? ? これは唯一の可約式であり、 Start 規則を適用する ->? Length [3,4] ||b: ? ? ? このグラフは、全体として新しい可約式である ->? 1 + Length [4] ||c: ? ? ? 加算演算子 + は、２番目の引数の評価を強制する ->? 1 + 1 + Length [] ||d: ? また + の２番目の引数 ->? 1 + 1 + 0 ||e: ? ? ? ? ? ? ２番目の + の２番目の引数は、 (r)nf に書換えられる ->? 1 + 1 ||f: ? ? ? ? ? ? ? ? グラフは、全体として新しい可約式である ->? 2 ||g: ? ? ? ? ? ? ? ? ? ? ? ? グラフは、 (r)nf の中にある

グラフと書き換え規則 GRS = {Rule} ; Rule = RedexPattern '->' ContractumPattern [',' Redirection] ? ? ? ? ? | RedexPattern '->' Redirection ; RedexPattern ? ? ? ? = Graph ; ContractumPattern = Graph ; Graph ? ? ? ? ? ? ? = [Nodeid ':'] Node {',' NodeDef} ; Nodeid ? ? ? ? ? ? ?= NodeIdVariable | NodeIdConstant ; Node ? ? ? ? ? ? ? ?= Symbol {Arg} | EmptyNode ; Symbol ? ? ? ? ? ?= Constant ; Arg ? ? ? ? ? ? ? ? ?= Nodeid | [Nodeid ':'] Symbol ? ? ? ? ? ? ? ? ? ? ? ? | [Nodeid ':'] '(' Node ')' ; EmptyNode ? ?= '_|_'; NodeDef ? ? ? ? = Nodeid ':' Node ; Redirection ? ? = Nodeid ':=' Nodeid | Nodeid ;

狠狠撸

Clean

More Related Content

Clean

Editor's Notes