2

私は、種類、タイプ、用語(または値、どちらが正しいかわからない)、およびそれらを操作するための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から戻り型を選択できる関数を作成する方法を見つけようとしましたが、これは起こらないことに気づきました。では、問題は、これらのタイプとそれらの間の相互作用を表すための効率的で柔軟な方法は何でしょうか?ありがとう。

4

1 に答える 1

2

短い答え:いいえ。Data.Dynamicラッパー ADT、またはtype-family/associated typeを使用する必要があります。

型ファミリはおそらくあなたが望むものに最も近いものですが、繰り返しになりますが、型はコンパイル時に決定できる必要があります。例えば:

{-# LANGUAGE TypeFamilies #-}

data Red
data Green
data Blue

data Yellow
data Cyan
data Violet

type family MixedColor a b
type instance MixedColor Red Red      = Red
type instance MixedColor Red Green    = Yellow
type instance MixedColor Red Blue     = Violet
type instance MixedColor Green Red    = Yellow
type instance MixedColor Green Green  = Green
type instance MixedColor Green Blue   = Cyan
-- etc ..

mixColors :: c1 -> c2 -> MixedColor c1 c2
mixColors = undefined

ここで、関数は基本的に任意の型の値を返すことができます が、コンパイラが引数の型に基づいて実際の戻り値の型を推測できるように、mixColors戻り値の型は型ファミリのインスタンスである必要があります。MixedColor

型ファミリと型クラスを使用して、比較的複雑な型関数を構築し、依存型の機能にますます近づけることができますが、それは、必要な型を作成するのに十分な型レベルの情報でデータを装飾する必要があることを意味します。計算。

最近導入された型レベルの自然数は、型で数値計算をエンコードする必要がある場合に役立ちます。

編集: また、ADT の使用に消極的である理由がわかりません (おそらく、ユースケースをより詳細に説明する必要がありますか? )Type1。ADT は非常に自然にエンコードされ、慣用的に使用されます。Type2

于 2013-02-19T07:38:50.880 に答える