matzにも解るよう、禅問答的に #ATS2 の型理論を説明してみたよ

@masterq_mogumog いや、そういう意味ではなくて、Haskell で幽霊型を使って newtype すると、プログラマが値に型を割り当てることができて、この話で説明しているのと同じことができるように見えるという話です。

2014-12-03 08:45:55

@khibino あーそうなんですね。この説明を想起して、あたまが飛んでしまいました。 / Phantom Type（幽霊型）入門ですー＞ω＜ | Moon? Shadow! kagamilove0707.github.io/programming/20…

2014-12-03 08:47:33

@masterq_mogumog newtype Assign 値の型割り当てたい型 = Assign 値の型みたいにやればできそうに見えます。

2014-12-03 08:53:25

@khibino なるほど。。。むつかしいです。。。なんかこうややこしいです。。。

2014-12-03 08:54:36

@masterq_mogumog ああ、なんか伝わりやすくしようとしてかえって変なことを書いてしまったか? 単に newtype Assign v t = Assign v と定義して、 Assign 値の型割り当てたい型のような型表現を使います。

2014-12-03 08:57:31

@khibino えっと、vがtに依存していることになるのでしょうか？

2014-12-03 08:58:25

@khibino 逆か。tが値vに依存していることになる？

2014-12-03 09:00:10

@masterq_mogumog この定義だけでは依存はしません。割り当て方法を定義しているようなイメージです。

2014-12-03 09:00:15

@khibino ということは依存ルールはアトミックに定義できなくて、ズレた場所に書く必要があるということですよね。依存を定義するにはかなりの量のコードが必要になるのでは。。。

2014-12-03 09:01:54

@khibino あーでも幽霊型でも型検査は正常に行なわれますね。線がひかれているので。

2014-12-03 09:02:27

@masterq_mogumog 方向というよりは組み合わせですね。依存させる方が良いのなら、そのような定義もできるんじゃないかとは思います。

2014-12-03 09:03:03

@khibino でもそもそも根本から違うんですよ。newtypeだと結局はコンストラクタが必要になっちゃうじゃないですか。

2014-12-03 09:03:16

@masterq_mogumog コンストラクタを書くのが面倒だいうのはその通りだと思います。

2014-12-03 09:04:24

@khibino リテラルはコンストラクタを使ってはいけません。すでにあるメモリ領域に型をApplyしたいんですよ。

2014-12-03 09:05:29

@masterq_mogumog すでにメモリにある値をコンストラクタで包むと Apply できると考えたらどんなもんでしょう?

2014-12-03 09:24:36

@khibino あー、わかった気がします。コンストラクタが機械的に生成されず、手作りになるのであれば、似ていると思います。

2014-12-03 09:24:46

@masterq_mogumog そう見えます。プログラマがライブラリとして newtype を定義できる

2014-12-03 09:26:07

@khibino えっと、、、それ順序が逆だと思うのですが、Haskellの性質上、コンストラクタなしには語れないので、リテラルは作れない。けれども値の扱いは同じ、ということなんじゃないかと思います。 #幽霊型

2014-12-03 09:26:08

@khibino そういう意味ではハイブリッドな言語というのがユーザ空間では使いやすいんだと思います。型=>値と値=>型

2014-12-03 09:27:21

@khibino #ATS2 の場合にはデフォルトが値=>型なので、型=>値を作るには参照を手作りする必要があります。Haskellの場合にはデフォルトが型=>値なので、値=>型を作るには幽霊型で手作りする必要があるんじゃないでしょうか。

2014-12-03 09:29:49

やりたいことは理解したがそれが本当に出来るということに驚く / “禅問答的に #ATS2 の型理論を説明してみたよ - Togetterまとめ” htn.to/LbKtVb #ats

2014-12-03 10:57:22

確かにこれは外延的に型を付けるということぽい

2014-12-03 11:01:52

いやどうだろう

2014-12-03 11:04:48

ある言語の意味論上に（恐らくそれを超えない範囲で）任意の整合した意味論を載せることが出来るということだと理解した、JS上に単純型付きλ計算載っけたら、それを超える範囲をJSで書こうとするとATSが型エラーを出す

2014-12-03 11:23:42