pythonで申し訳ないです。
一般的なプログラム言語の基数は、２，８，１０，１６でしょうか?
例えば,3進数の整数型をclass定義して、内部でmax制限しては？どうでしょうか?
アクセサメソッドを持ちて(x.value = 210 )もよいでしょうし、rubyのメタプログラミングで、int型のように、trd型(x trd = 210)を作成できそうです。
尚、有効桁数が異常に長い値の計算にはlinuxにｂｃコマンド、ｂｃ言語がありますのでご参考下さい。
Like!
型の値を制限した型、どうやって作りますか？
Q&AClosed
具体型の制限としての型って、直接作れなくない？
・ここで言う制限とは定義域の制限(数学)のきもちです
・今はhaskell でコーディングを試みていますが、c++とfortranも少し触りました
現在
様々な基数での位取り記数と、基数を固定したうえでの整数内での四則演算を行えるような実験場を創ろうとしています。
ここでそもそも基数として、数学的には負の数もとれるのですが、簡単のために、自然数のみをとる事を考えています。しかし、単位的可換環で基数にできるのは零因子でも単元でもない元に限りますから、自然数であっても、0と1は基数としてとれません。
また、桁部(仮数部といってもいいでしょう)については、基数nに依存して、0以上n未満の整数のみを取りたいという要求があります。
さて、これらの要求を満たす為に、仮に、具体型Xを集合とみなして、その真部分集合Sが内包的に論理式
A(x)=True
A(x)=False
の何れかで定義されるときに、S⊂Xに相当する
SinX型
を定義するような機能があれば、これを用いて、少なくとも
基数型 :: 2以上のInteger
が作れますし、定義式のAに型パラメータを持ち込めれば、
桁(n)型 :: 0以上n未満のInteger
というのも作れるわけです。ここをクリアすればあとはフィールドラベルなりタプルなり、基数型を型パラメータに取るような桁リスト型なりで目的の物は作れるでしょう。
ところが前述したどの言語でも、このような、
既存の型を制限して新たな型とする機能
は見つけられませんでした（それでも最も型を弄りやすそうな言語だから、いまhaskellなわけです）。
部分集合をとる操作の基本っぷりに反してプログラミングにおいて制限型の作成機能がこうも”無い”となると、「わざわざそんなことしなくても、機械の論理的には同じことが可能である」というような、
定石のようなものがあるのかもしれないということに思い至りました。
そこで、制限型の作成が直接的に実装されていない理論的背景や、制限型に相当する仕組みの作成方法、その定石について、存在するならば解説をお願いしたく存じます。
一応、現時点で基数型については
基数(仮)
data Radix = Radix Nat deriving (Show, Read, Eq)
-- Radix n is equivalant to 2+n by the function "proper" and "reporp"
proper :: Radix -> Nat
proper (Radix x) = 2 + x
-- reporp has "*** Exception: arithmetic underflow" at 0 and 1
reporp :: Nat -> Radix
reporp x = Radix (x - 2)
のようにしてみています。型パラメータとしての利用を見据えているわけですが、どのように型パラメータを関数レベルの記述に取り出して利用できるのかいまいちわかっておらず、現在は各種拡張の文法やその意義を理解していく作業の真っ最中です。
息がつまってきたのでそもそも論の質問をしました。プログラミングの実力は...お察しください。低いです。
何より情報科学の基礎知識がほとんどありません。キーワードがあれば自力で調べますから、まずは大枠の論理展開をなるだけ簡潔に述べるところから(できれば易しく)おねがいします。
お礼
結局求めていたものに最も近いのは篩型の概念でした。
しかし、回答全体を通して理解できた感覚もあって、とくに、型を利用する意義についてはだいぶ理解が深まりました。ありがとうございました。
0
4Answer
1
Comments
@AliasK
Questioner個別の基数にもとづいて型を一つづつ定義したいわけではないのです。例えば、十進のカプレカ数は、2進のカプレカ操作に対して何らかの特徴を示すのか？5進ではどうか？一般に、n進とnの約数進とにカプレカ操作を通した興味深い関係はありそうか…みたいなことを、実際に観察してみて、「ナンセンスな予想だな」とか「何か起こってるぞ！」とかやりたいよね！
という話です。
一方で、bcについての情報提供はありがたいです。また一つ世界観が広がりました。@AliasK
Questionerいえ、失礼、読み直してみるとむしろ前半について詳しく知りたいです。
n進数の整数型をclass定義して、内部でmax制限
というのは、具体的にどのような値を持たせるのでしょうか。たぶん、x.value = 210 とかx trd = 210の意味するところが判らないで困ってます。あと、max制限とはどういう行為ですか？
ご紹介のリンクで解決しました！まさか型=クラスとは！
haskell脳で読んでしまいました。プログラミング系のツールって本当にいろいろな思想で実装されてるんですね
定義域を制限しても定義域からはずれた値が渡されうるのであれば、その状況に対処するプログラムも書かなければなりません。 (その対処法が単に停止するという内容なこともあるかもしれませんが、回復のための処理が必要なこともあるかもしれません。) 汎用プログラミング言語では定義域を型レベルで表現する意味があまりなく、式や文で判定処理を書けばそれで足ります。
処理の内容とは別に定義域を明示して書くような考え方で契約プログラミングと呼ばれるものがあり、そのための文法を備えた言語はあります。
様々な制限を型レベルで表現・検証することを指向したプログラミング言語は定理証明器と呼ばれるジャンルが確立しているので数学寄りの考え方で型を取り扱いたいのであればそれらの使用を検討してはいかがでしょうか。
Like!
Comments
@AliasK
Questionerありがとうございます。なるほど...定理証明器という名前に引っ張られて、「最終的には数値計算をさせたいから汎用の方がいいのかな」と早合点していました。契約プログラミングという概念は初見で、興味深いです。
汎用言語では結局エラーを自分で定義すればいいということに落ち着くんですね。
気持ちとしては、「誰も不正な値をその関数に放り込めないような注釈を書く準備として、型レベルで手軽に制限できたらいいのに」という事だったんですが、このばあい契約プログラミングか定理証明器、どっちが向いてるんでしょう？定理証明器は全ての情報が事前にわかる、閉じた世界でないと完璧には検証できません。 現実的なプログラムは外部とのやり取りが全くないなんてことはありません。 なんらかの入出力はあります。
プログラムの内部は完璧に検証することが出来たとしても外の世界から与えられる情報が制限を満たしているかどうか事前に検証するのは不可能なわけです。 どうあがいてもそれは実行するときに検証する必要がありますので定理証明器では扱いにくいと思います。
契約プログラミングの考え方は「その契約通りに使う」ということが前提としてあります。 契約通りになっていないならばそれはバグです。 バグであることが (実行時に) わかる仕組みであって、事前に論理的な検証が充分に出来るわけではありません。 動かしてみるまで正しいかどうかはわかりません。
結論としては現実的な計算と型レベルでの論理的な検証は両立しづらく、定理証明器と契約プログラミングはどちらにも一長一短があります。 メリットもデメリットもある中で程度を見極めて選択するしか仕方なく、どちらが良いとは言えない感じだと思います。
定理証明器を現実的なプログラムにある程度に適用しようとする試みはあるようなのですが、私自身は定理証明器に明るいというわけではありませんので具体的な提案はできません。
@AliasK
Questionerありがとうございます！
まさに質問の本質について解説頂けて誠に勉強になりました。
これから目的のコーディングとは別に、証明＝プログラム という対応の話を勉強しなくてはならなそうです...(笑)
まだイメージが曖昧なので完璧におっしゃることを共有できている感じはありませんが、これから先の研究や開発において役立ついい手掛かりがもらえた感じがしています。ありがとうございました。追:woxtuさんの回答にあった篩型を調べてliquid haskellにたどり着いてチュートリアル記事を読んでいたところ、制限を表す内包式で、”検証する”という表現がなされていてわかってきました。
要するに、関数に入力される値がコンパイル時にわかっていれば型のエラーとして教えてくれるが、実行して初めて得られる謎の値を関数が受け取るとき、その値が不正かどうかは、コンパイル時にわかるわけないし、「不正ならもう一回入力を求める」とかいう仕様にしたければ、もともとの関数のふるまいとして分岐させとけよという話なんですね。それでMaybeとかが出てくると...。
で、コンパイル時にわかる不正を教えてくれるほうの型検査を、検証というわけですか。
This answer has been deleted for violation of our Terms of Service.
求めているものかはわかりませんが篩型や依存型のことでしょうか。
Like!
Comments
@AliasK
Questionerドンぴしゃかもしれません
引用始め"
foo :: { x:a | P x } -> { y:b | Q y } a 型のうち条件 P を満たす値から b 型のうち条件 Q を満たす値への関数
"引用終わり.https://qiita.com/Afo_guard_enthusiast/items/ffd89cd43a2ea81fdb17より。この機能があれば、型を定義しなくても、関数の定義域は制限できますね…。
当初の構想とは少しシステムの構造が変わりますが、いまのところ一番しっくり理解できています。こういう関数をメソッドに持つクラスを定義することで、不正な入力値を組み込みのコンパイルエラーではじけるのはすごく魅力的です。ここではじめて@ryukumalさんにご紹介いただいたインターフェイス的な考え方をするわけですよね……よさげっすね。