型の値を制限した型、どうやって作りますか？
Q&A
Closed
具体型の制限としての型って、直接作れなくない？
・ここで言う制限とは定義域の制限(数学)のきもちです
・今は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)
のようにしてみています。型パラメータとしての利用を見据えているわけですが、どのように型パラメータを関数レベルの記述に取り出して利用できるのかいまいちわかっておらず、現在は各種拡張の文法やその意義を理解していく作業の真っ最中です。
息がつまってきたのでそもそも論の質問をしました。プログラミングの実力は...お察しください。低いです。
何より情報科学の基礎知識がほとんどありません。キーワードがあれば自力で調べますから、まずは大枠の論理展開をなるだけ簡潔に述べるところから(できれば易しく)おねがいします。
お礼
結局求めていたものに最も近いのは篩型の概念でした。
しかし、回答全体を通して理解できた感覚もあって、とくに、型を利用する意義についてはだいぶ理解が深まりました。ありがとうございました。
