9

「リロードされたボイラープレートのスクラップ」では、著者は、オリジナルと同等であると思われる「ボイラープレートのスクラップ」の新しいプレゼンテーションについて説明しています。

ただし、1つの違いは、GADTでエンコードされた「ベース」タイプの有限の閉集合を想定していることです。

data Type :: * -> * where
  Int :: Type Int
  List :: Type a -> Type [a]
  ...

元のSYBでは、型セーフキャストが使用され、Typeableクラスを使用して実装されます。

私の質問は次のとおりです。

  • これら2つのアプローチの関係は何ですか？
  • 「SYBリローデッド」プレゼンテーションにGADT表現が選択されたのはなぜですか？
4

2 に答える 2

5

まあ、明らかにTypeable使用はオープンです-新しいバリアントは事後に、元の定義を変更せずに追加できます。

ただし、重要な変更は、その中で型指定されていないことTypeRepです。つまり、ランタイムタイプTypeRep、、とそれがエンコードする静的タイプの間に関係はありません。GADTアプローチを使用すると、GADTで指定された、型aとその型の間のマッピングをエンコードできます。TypeType a

したがって、型repがその元の型に静的にリンクされていることのType a証拠を焼き付け、ランタイムがあることの証拠として使用して、静的に型付けされた動的アプリケーションを作成できます（たとえば） a。

古いTypeRepの場合、そのような証拠はなく、実行時の文字列の同等性、およびを介して最善を強制し、期待することになりますfromDynamic。

署名を比較します。

toDyn :: Typeable a => a -> TypeRep -> Dynamic

対GADTスタイル：

toDyn :: Type a => a -> Type a -> Dynamic

型の証拠を偽造することはできません。後でそれを再構築するときに使用できます。たとえば、型クラスのインスタンスを検索して、a持っているのが。だけの場合などですType a。

于 2013-03-01T15:33:11.873 に答える
5

[私は「SYBリローデッド」論文の著者の一人です。]

TL; DR私たちにとってはもっと美しいように見えたので、私たちは本当にそれを使用しました。クラスベースのTypeableアプローチの方が実用的です。ビューはクラスとSpine組み合わせることができ、 GADTTypeableに依存しません。Type

論文はその結論の中でこれを述べています：

私たちの実装は、元のSYBペーパーとは異なる方法でジェネリックプログラミングの2つの中心的な要素を処理します。タイプセーフキャスト1またはクラスベースの拡張可能なスキームに基づくオーバーロードされた関数の代わりに、明示的なタイプ引数を持つオーバーロードされた関数を使用します[20]。また、コンビネータベースのアプローチではなく、明示的なスパインビューを使用します。両方の変更は互いに独立しており、明確さを念頭に置いて行われました。SYBアプローチの構造は私たちの設定でより明確になり、PolyPおよびGenericHaskellとの関係がより明確になると思います。スパインビューは、記述できるジェネリック関数のクラスに制限されていますが、GADTを含む非常に大きなクラスのデータ型に適用できることを明らかにしました。

明示的な型引数を使用してオーバーロードされた関数をエンコードするには、Typeデータ型とtoSpineなどの関数の拡張性が必要なため、このアプローチをライブラリとして簡単に使用することはできません。ただし、SYBペーパーの手法を使用してオーバーロードされた関数をエンコードしながら、SpineをSYBライブラリに組み込むことができます。

したがって、タイプ表現にGADTを使用するという選択は、主に明確にするために行ったものです。ドンが彼の答えで述べているように、この表現にはいくつかの明らかな利点があります。つまり、型表現がどのタイプであるかに関する静的な情報を維持し、それ以上の魔法なしで、特に使用せずにキャストを実装できることです。のunsafeCoerce。タイプインデックス関数は、タイプのパターンマッチングを使用して直接実装することもでき、やなどのさまざまなコンビネータにフォールバックすることもありませmkQんextQ。

事実、私（そして共著者）は単にTypeableクラスがあまり好きではなかったと思います。（実際、私はまだそうではありませんが、GHCが自動派生を追加し、種類を多形にし、最終的に独自のインスタンスを定義する可能性を排除するという点で、最終的にもう少し規律が増しTypeableています。）さらには、Typeableおそらく現在ほど確立されておらず、広く知られていなかったため、GADTエンコーディングを使用して「説明」することは魅力的であるように思われました。さらに、これは、Haskellにオープンデータ型を追加することも考えていた時期であり、それによってGADTが閉じられるという制限が緩和されました。

unsafeCoerceつまり、要約すると、閉じたユニバースに対してのみ動的な型情報が実際に必要な場合は、パターンマッチングを使用して型インデックス関数を定義でき、依存したり高度なものにする必要がないため、常にGADTを使用します。コンパイラの魔法。ただし、一般的なプログラミング設定では確かに一般的である宇宙が開いている場合、GADTアプローチは有益かもしれませんが、実用的ではなく、使用Typeableすることが道です。

ただし、このペーパーの結論でも述べているように、Typeオーバーの選択Typeableは、私たちが行っている他の選択の前提条件ではありません。つまり、Spineビューを使用することです。これは、より重要であり、実際にはペーパーのコアであると思います。 。

紙自体は（セクション8で） 「クラスでボイラープレートをスクラップする」紙に触発されたバリエーションを示しています。これは、Spine代わりにクラス制約のあるビューを使用します。しかし、より直接的な開発を行うこともできます。これを以下に示します。このために、Typeablefromを使用しますが、簡単にするために、メソッドを含むData.Typeable独自のクラスを定義します。DatatoSpine

class Typeable a => Data a where
  toSpine :: a -> Spine a

Spineデータ型は現在、制約を使用していますData。

data Spine :: * -> * where
  Constr  :: a -> Spine a
  (:<>:)  :: (Data a) => Spine (a -> b) -> a -> Spine b

この関数fromSpineは、他の表現と同じくらい簡単です。

fromSpine :: Spine a -> a
fromSpine (Constr x) = x
fromSpine (c :<>: x) = fromSpine c x

のインスタンスは、Data次のようなフラットタイプでは簡単ですInt。

instance Data Int where
  toSpine = Constr

そして、それらは二分木などの構造化されたタイプに対してはまだ完全に簡単です。

data Tree a = Empty | Node (Tree a) a (Tree a)

instance Data a => Data (Tree a) where
  toSpine Empty        = Constr Empty
  toSpine (Node l x r) = Constr Node :<>: l :<>: x :<>: r

次に、このペーパーでは、などのさまざまなジェネリック関数を定義しmapQます。これらの定義はほとんど変わりません。Data a =>論文に次の関数の引数がある場合にのみ、クラス制約を取得しますType a ->。

mapQ :: Query r -> Query [r]
mapQ q = mapQ' q . toSpine

mapQ' :: Query r -> (forall a. Spine a -> [r])
mapQ' q (Constr c) = []
mapQ' q (f :<>: x) = mapQ' q f ++ [q x]

次のような高レベルの関数everythingも、明示的な型引数を失うだけです（実際には、元のSYBとまったく同じように見えます）。

everything :: (r -> r -> r) -> Query r -> Query r
everything op q x = foldl op (q x) (mapQ (everything op q) x)

上で述べたように、すべてのInt出現を合計する一般的な合計関数を定義する場合、パターンマッチはできなくなりますが、にフォールバックする必要がありますがmkQ、mkQ純粋に定義されTypeable、完全に独立していSpineます。

mkQ :: (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
(r `mkQ` br) a = maybe r br (cast a)

そして（これも元のSYBとまったく同じです）：

sum :: Query Int
sum = everything (+) sumQ

sumQ :: Query Int
sumQ = mkQ 0 id

このホワイトペーパーの後半にあるもの（コンストラクター情報の追加など）については、もう少し作業が必要ですが、すべて実行できます。したがって、Spine実際に使用することは、使用することにまったく依存しませんType。

于 2013-03-01T17:30:13.147 に答える