Name名無し21/06/27(日)06:43:43No.115402+
22年5月頃消えます 型ってなに？
集合とは違うの？

…No.115403+コンピュータは通常、整数しか扱えない。その整数もどれだけの大きさの整数を扱うかでメモリーを使う量が変わる。 その形式は色々考えられるが、形式ごとに変数が表せる範囲や、精度が変わるってこと。 その形式のことを型とか言うわけだ。

…No.115405+もっと数学的に More mathematically

…No.115406+例えば、同じ整数型でも0か1の組み合わせ（ビット）の数で型が分けられている。 int16 なら16ビット符号あり整数。 int32 なら32ビット符号あり整数。 int64 なら64ビット符号あり整数。 それぞれ扱える整数の範囲が違い、ビット数が多くなれば扱える範囲が広がるが、メモリーを食う。 今のCPUは64ビットか32ビット。32ビットマシンで64ビット整数を扱うにはちょっとした工夫が必要となる。 unsigned int という型もあり、これは正の数だけを扱うことにした整数型。これを使うと扱える数の範囲が２倍になるが負数は扱えない。 float , double というのは、数を実数部×指数部という２つの数に分け小数を扱えるようにしたもの。doubleはfloatの２倍の容量を使い、２倍の精度で計算できる。 ちなみに、実際にはどのようなビット構成になっているかは機種ごとに違っているが…今は IEEE754 の構成になっているはず。これが結構複雑というか、なんでこう定義したのかーというか。まあ、今は機械で計算させるんだけどね。

…No.115407+ いやそういう実装上の話では無くて型の公理と集合の公理の違いが知りたい そもそも型理論にZF公理みたいなのってあるの？

…No.115408+型なんてコンピュータの実装上の都合じゃないの？ チューリングのいうマシンに型なんて概念ないでしょ 深くは調べてないけど

…No.115409+いや型自体はコンピュータの前からあるよ プログラミングに応用されてるってだけでコンピュータ特有の概念じゃない

…No.115410+でも、コンピュータ上に実装される型って加法ですら全単射じゃないしなあ。桁あふれとか、切り捨て・四捨五入とかあるし。 そんなんでZF公理系と言っても…

…No.115411+とりあえずコンピュータの話は忘れてもらって…

…No.115412+スレ画が良くなかったのかもしれない

…No.115413+>コンピュータ上に実装される型って加法ですら全単射じゃないしなあ。 そもそも加法は全単射じゃないのでは

…No.115414+型は集合とだいたい同じなんじゃないの だから部分型とか直和とか直積とか型の関数とか型の型とかを考えることができる

…No.115415+集合を包含してる感じだろうけど型にあって集合に無いのってなんだろ

…No.115416+コンピュータの実装なしの型の定義って…わからんｗ 型の型？コンピュータだと、機械語のその型へのポインターみたいなヤツ？ｗ 型の関数？指定した型を返す関数？ 数学だとどうなるんだ？ 実数や整数だと加法の関数を定義すると、全単射なんじゃ？

…No.115417そうだねx11+3も2+2も4になるのにどこが全単射なんじゃ……

…No.115418+>型の型？コンピュータだと、機械語のその型へのポインターみたいなヤツ？ｗ 例えば 123 : Int だけど Int : Number みたいなのがあっても良いって事かと プログラミングで言うと型クラスに相当する感じかな？

…No.115419+どっちかと言うとカインドのことなのかな？

…No.115420+>型の関数？指定した型を返す関数？ これはここに乗ってる奴かな？ https://qiita.com/HirotoShioi/items/39fc492401e4dcbc8cba Zero型とSucc Zero型, Succ(Succ Zero)型, ... と作って行って型で"自然数"を作ったり出来るらしい で更にその"自然数"同士を足すAdd型族というのが定義できるとか

…No.115424+俺の理解が間違ってるのかもしれんが 「集合の集合」のことじゃなかったっけ 「全ての集合の集まり」をふつうの集合のように扱うと矛盾するとRussellが証明して 当のRussellが「集合の集合」「集合の集合の集合」以下略を使いまくれば これを解決できるのではないかと対策案として提示したやつ 応用上いろいろと便利な方法ではあったが 「全ての集合の集まり」対策としては失敗したとか何とか その後Quineの系譜がこの路線で（原子的元urelementsを追加して） 「全ての集合の集まり」対策に成功したZFC公理系とほぼ遜色なく 数学諸概念を構成できるNFU公理系を作ったとか何とか（詳しくねえ）

…No.115425+>「集合の集合」のことじゃなかったっけ これは真のクラスって奴だと思う んでパラドックス発見したのはカントールじゃなかったかな ラッセルのパラドックスはR={x| x∉x}に関する奴 型は何か値の右側に注釈として付いてる感じのイメージ 123 : 自然数 みたいな この"自然数"が型

…No.115426+>これは真のクラスって奴だと思う >んでパラドックス発見したのはカントールじゃなかったかな >ラッセルのパラドックスはR={x| x��x}に関する奴 あっしまった 独学だとこういうところがうろ覚えになっちゃう >型は何か値の右側に注釈として付いてる感じのイメージ >123 : 自然数 >みたいな >この"自然数"が型 確かにそういう使われ方してるね 「これらはこれの型の例であり他の型の例ではない」 「この型とはこれこれの条件を満たす集合である （条件のない単なるラベルの貼り付けられた集合のこともある）」 こうか？

…No.115427+『圏論の歩き方』という教科書というよりも大学講義のカタログみたいな本あるけど 第4章『プログラム意味論と圏論』の要約を発掘したら 「Curry-Howard対応というやつで型は命題のようなものと見なせる」という記述があった 別のプログラム系の人の書いた名前の通り『型理論』って本だと 変数や変数の（ラムダ計算の）式としての「項」は「型」を「持ち」 実際には型とはまた別の変数や変数の右結合で出来ている （例えば整数型や二値真理値型や「整数型（の項）を入力したら二値真理値型（の項）を出力するなんか型」等） ということで集合というよりは式と関係のある命題として考えた方がいいのだそうな どういう関係かはちょっと分からない（部分集合とは考えにくいから順序対か対応だと思う）

…No.115428+だから>>18はナシ 書いといて何だがごめんなさい

…No.115429+Curry-Howard対応ってのは例えば型付き計算の 「x : double, f : double -> int と言うデータから f(x) : int を計算するプログラムが作れます」 と言う事実の型の部分だけ見ると, 「double, double -> int から int が計算できます」 となって, これが論理学の 「A, A -> B を仮定すると B が導かれる」 （モーダス・ポネンス） となんか似てるねってなる奴だね すごく抽象的な関係だから型（ここで言うdouble, int）と命題（A, B）が同じですよって言われても「？」ってなるだけな気もする 集合{1,2,3}と{りんご,みかん,バナナ}が同型ですよって言われても1=りんご,3=バナナだったんだ！とはならないのと同じ感じで

…No.115430+ただ集合には結構似てる気がして, 例えば x : double, f: double -> int っていうのも, x ∈ double, f ∈ Map(double, int) （Map(A,B)は集合Aから集合Bへの関数の集合） と言い換えて違和感ないし

…No.115431+命題は真偽値が付かなきゃいけないという制約付きだけど型と集合はそういうのないのが大きな違いか