-
masterq_mogumog
- 1430
- 0
- 0
- 0
-
- いいね！0
I moved to Mastodon.
@masterq_mogumog
さぁ静的な関数で作られたじゃんけんライブラリをちゃんと理解しよう。。。 / ATS-Postiats-test/test25.dats at master · githwxi/ATS-Postiats-test github.com/githwxi/ATS-Po…
2015-10-30 17:32:13
I moved to Mastodon.
@masterq_mogumog
fun rps_even {r1,r2:rps | rps_win(r1, r2)} (x1: rps (r1), x2: rps (r2)): [r3:rps | rps_win(r3, r1)] (rps (r3)) = rps_win (x1) これでいいらしい
2015-10-30 18:36:22
I moved to Mastodon.
@masterq_mogumog
静的な関数のシグニチャはstacstで導入される。これは問題ない。誰もが馴染みの関数型プログラミング
2015-10-30 18:37:04
I moved to Mastodon.
@masterq_mogumog
じゃあ静的な関数の本体はどこで実装するか、というと実装はいらない。なぜならその本体は制約ソルバによって解決されるから。これもまぁ納得したとしよう。でもその制約を課すためのヒントのようなものはプログラマが作る必要があるよね。
2015-10-30 18:40:06
I moved to Mastodon.
@masterq_mogumog
で、ここでHongwei作の静的な関数を使ったじゃんけんプログラムを見てみる。 / ATS-Postiats-test/test25.dats at master · githwxi/ATS-Postiats-test github.com/githwxi/ATS-Po…
2015-10-30 18:40:56
I moved to Mastodon.
@masterq_mogumog
件のじゃんけんプログラムではrpsという名前で種を導入している。これは静的な式の型として使われる。これもいいだろう。マニュアルの通り datasort rps = r | p | s / github.com/githwxi/ATS-Po…
2015-10-30 18:51:16
I moved to Mastodon.
@masterq_mogumog
さらにrpsという名前で種rpsに依存したデータ型を導入する。これはrps -> typeのような静的な関数を導入していることでもあるということだった / datatype rps(rps) = r(r) | p(p) | s(s) github.com/githwxi/ATS-Po…
2015-10-30 18:54:52
I moved to Mastodon.
@masterq_mogumog
型の別名を導入する。この別名は種に依存しない型で、つまりは静的な関数ではなく、種typeの値なのだった。 / typedef rps = [x: rps] rps (x) github.com/githwxi/ATS-Po…
2015-10-30 18:56:41
I moved to Mastodon.
@masterq_mogumog
種の機能を使わず、型としてrpsを使うには、単にcaseで場合分けすればいい。注意したいのは、型名の指定には r() のように()を付ける必要があること。先のdatatypeの型を指定するには () が必要 / github.com/githwxi/ATS-Po…
2015-10-30 18:59:09
I moved to Mastodon.
@masterq_mogumog
やっと出てくる静的な関数のシグニチャ。このときのrpsは種で、関数の返り値がboolで終わっているのは静的な式の中でガードとして使うから / stacst rps_win : (rps, rps) -> bool github.com/githwxi/ATS-Po…
2015-10-30 19:01:04
I moved to Mastodon.
@masterq_mogumog
そーゆー意味では、この部分はRefinement Typeと似たような機能を持っているとも言えるんじゃないか。
2015-10-30 19:02:04
I moved to Mastodon.
@masterq_mogumog
で、静的な関数のシグニチャは無事導入された。問題は定義がないから静的なrps_win関数の第一引数と第二引数、どっちが勝つという条件でこの関数シグニチャが導入されているのかわからないということ。だから、なんらかのヒント(もしくは制約)をどっかで導入しないと辻褄があわない
2015-10-30 19:04:02
I moved to Mastodon.
@masterq_mogumog
無条件に静的な関数を導入してしまう証明関数を作る。この関数が呼ばれれば、静的な関数に対するヒントが関数コンテキストに導入されるんだと思う / praxi rps_win_r_s(): [rps_win(r, s)] void ... github.com/githwxi/ATS-Po…
2015-10-30 19:08:11
I moved to Mastodon.
@masterq_mogumog
例えばこの動的な関数rps_winでは先の証明関数を呼び出して、静的な関数に対するヒントを導入してから、存在量化に依存した返り値rpsを作る。 github.com/githwxi/ATS-Po…
2015-10-30 19:10:44
I moved to Mastodon.
@masterq_mogumog
もしこのヒントの導入しないと / unsolved constraint: C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(rps_win); S2EVar(4423->S2Eapp(S2Ecst(p); )), S2Evar(x1(7907))))
2015-10-30 19:12:23
I moved to Mastodon.
@masterq_mogumog
毎度エラーが読みにくいけど、これはrps_win(p, x1)という制約を解決できないと言ってるんだと思う。関数本体の実装はわからないけど、その静的な関数の制約を解決するにはヒントが足りない。
2015-10-30 19:23:22
I moved to Mastodon.
@masterq_mogumog
例えば、このcase+をcaseに変えて、さらにprval () = rps_win_r_s()と| s() => r()の行を削除してしまえばコンパイルエラーは回避できる。もちろんランタイムエラーが発生する github.com/githwxi/ATS-Po…
2015-10-30 19:25:36
I moved to Mastodon.
@masterq_mogumog
常にあいこになる関数 fun rps_even {r1,r2:rps | rps_win(r1, r2)} (x1: rps (r1), x2: rps (r2)): [r3:rps | rps_win(r3, r1)] (rps (r3)) = rps_win (x1)
2015-10-30 19:29:07
I moved to Mastodon.
@masterq_mogumog
も定義できる。この関数rps_evenをcase+で定義する、またヒントの注入が必要になるが、rps_winには既に導入されているので、rps_win関数の返り値だけは制約が常に解決している。後はrps_evenを呼ぶ段でr1がr2に勝つという関係をrps_winで注入すればいい
2015-10-30 19:32:03
I moved to Mastodon.
@masterq_mogumog
こんな感じにすればあいこを出す関数は呼び出せる / gist.github.com/master-q/a590d…
2015-10-30 19:38:14