私は、種類、タイプ、用語(または値、どちらが正しいかわからない)、およびそれらを操作するためのGHC拡張機能をよく理解しようとしています。TypeFamiliesを使用してTypesを使用して関数を記述できることを理解しています。また、DataKinds、PolyKindsなどを使用してKindsをある程度操作できるようになりました。まだ完全には理解していませんが、興味深いと思われるシングルトン型に関するこのペーパーを読みました。これはすべて私に疑問を投げかけました、用語または値レベルでの計算に基づいてリターンタイプを計算する関数を作成する方法はありますか?これは依存型が達成することですか?
これが私が考えていることの例です
data Type1
data Type2
f :: Type1 -> Type2 -> (Type1 or Type2)--not using Either or some "wrapper" ADT
- アップデート - - - -
ここでの多くの研究と助けに基づいて、私がいくつの拡張を有効にしても、Haskellの値レベルでの式に基づいて関数の戻り値を計算することはできないことが明らかになりました。ですから、誰かが私が前進するための最良の方法を決定するのを手伝ってくれることを期待して、実際のコードをもっと投稿しています。基本タイプとして円錐曲線と二次曲面を使用した小さなライブラリを作成しています。これらのタイプの操作には、それらの間の交点の計算が含まれます。2つのサーフェスの交点は、円錐曲線のタイプの1つであり、点のように縮退します(実際には、円錐曲線以外に別のタイプの曲線が必要ですが、点以外の曲線も必要です)。正確なカーブリターンタイプは、実行時の交差するサーフェスの値によってのみ決定できます。円柱-平面の交差は、Nothing、Line、Circle、またはEllipseになる可能性があります。私の最初の計画は、このようなADTを使用して曲線とサーフェスを構造化することでした...
data Curve = Point !Vec3
| Line !Vec3 !UVec3
| Circle !Vec3 !UVec3 !Double
| Ellipse !Vec3 !UVec3 !UVec3 !Double !Double
| Parabola !Vec3 !UVec3 !UVec3 !Double
| Hyperbola !Vec3 !UVec3 !UVec3 !Double !Double
deriving(Show,Eq)
data Surface = Plane !Vec3 !UVec3
| Sphere !Vec3 !Double
| Cylinder !Vec3 !UVec3 !Double
| Cone !Vec3 !UVec3 !Double
deriving(Show,Eq)
...これは最も簡単で、私が好きな閉じた代数型であるという利点があります。この表現では、交差点の戻りタイプは簡単で、カーブだけです。この表現の欠点は、これらのタイプのすべての関数が各タイプのパターンマッチを実行し、私には面倒に思えるすべての順列を処理する必要があることです。Surface-Surface交差関数には、一致する16のパターンがあります。
次のオプションは、各サーフェスとカーブタイプを個別に保持することです。そのようです、
data Point = Point !Vec3 deriving(Show,Eq)
data Line = Line !Vec3 !UVec3 deriving(Show,Eq)
data Circle = Circle !Vec3 !UVec3 !Double deriving(Show,Eq)
data Ellipse = Ellipse !Vec3 !UVec3 !UVec3 !Double !Double deriving(Show,Eq)
data Parabola = Parabola !Vec3 !UVec3 !UVec3 !Double deriving(Show,Eq)
data Hyperbola = Hyperbola !Vec3 !UVec3 !UVec3 !Double !Double deriving(Show,Eq)
data Plane = Plane !Vec3 !UVec3 deriving(Show,Eq)
data Sphere = Sphere !Vec3 !Double deriving(Show,Eq)
data Cylinder = Cylinder !Vec3 !UVec3 !Double deriving(Show,Eq)
data Cone = Cone !Vec3 !UVec3 !Double deriving(Show,Eq)
これは、長期的にはより柔軟で、きめ細かく優れているように見えますが、交差関数からの複数の戻りタイプを処理したり、一般的な「曲線」または「表面」のリストを作成したりするには、ラッパーADTが必要になります。それらの間に関係がないからです。型クラスと実存を使用してそれらをグループ化することはできますが、元の型が失われ、気に入らないのです。
これらの設計の妥協により、私はこれを試してみました。
---------------------------------------------------------------
-- Curve Types
---------------------------------------------------------------
type Pnte = Curve PNT
type Line = Curve LIN
type Circ = Curve CIR
type Elli = Curve ELL
type Para = Curve PAR
type Hype = Curve HYP
-----------------------------------------------
data CrvIdx = PNT
| LIN
| CIR
| ELL
| PAR
| HYP
-----------------------------------------------
data Curve :: CrvIdx → * where
Pnte :: !Vec3 → Curve PNT
Line :: !Vec3 → !UVec3 → Curve LIN
Circ :: !Vec3 → !UVec3 → !Double → Curve CIR
Elli :: !Vec3 → !UVec3 → !UVec3 → !Double → !Double → Curve ELL
Para :: !Vec3 → !UVec3 → !UVec3 → !Double → Curve PAR
Hype :: !Vec3 → !UVec3 → !UVec3 → !Double → !Double → Curve HYP
---------------------------------------------------------------
-- Surface Types
---------------------------------------------------------------
type Plne = Surface PLN
type Sphe = Surface SPH
type Cyln = Surface CYL
type Cone = Surface CNE
-----------------------------------------------
data SrfIdx = PLN
| SPH
| CYL
| CNE
-----------------------------------------------
data Surface :: SrfIdx → * where
Plne :: !Vec3 → !UVec3 → Surface PLN
Sphe :: !Vec3 → !Double → Surface SPH
Cyln :: !Vec3 → !UVec3 → !Double → Surface CYL
Cone :: !Vec3 → !UVec3 → !Double → Surface CNE
...最初は、「Curve」(リストや交差点の戻りタイプなど)で任意の曲線タイプを参照でき、完全なタイプも持つことができる、魔法のような、両方の世界で最も優れたシナリオを提供すると思いました。マルチパラメータ型クラスなどを使用して、きめ細かいスタイルで関数を記述できます(Curve CrvIdx)。すぐに、この質問に示されているように、これが期待したほどうまく機能しないことがわかりました。私は頑固に壁に頭をぶつけ続け、実行時の引数の幾何学的特性に基づいてGADTから戻り型を選択できる関数を作成する方法を見つけようとしましたが、これは起こらないことに気づきました。では、問題は、これらのタイプとそれらの間の相互作用を表すための効率的で柔軟な方法は何でしょうか?ありがとう。