一般化された代数データ型を利用するにはどうすればよいですか?
haskell wikibookに示されている例は短すぎて、GADT の実際の可能性についての洞察を得ることができません。
8592 次
5 に答える
54
GADT は、従属型付け言語からの帰納的ファミリの弱い近似です。代わりに、そこから始めましょう。
インダクティブ ファミリは、依存型付き言語のコア データ型導入方法です。たとえば、Agda では、次のように自然数を定義します。
data Nat : Set where
zero : Nat
succ : Nat -> Nat
これはあまり派手ではありませんが、基本的には Haskell の定義と同じです。
data Nat = Zero | Succ Nat
実際、GADT 構文では、Haskell 形式はさらに類似しています。
{-# LANGUAGE GADTs #-}
data Nat where
Zero :: Nat
Succ :: Nat -> Nat
そのため、一見すると、GADT は単なる特別な構文にすぎないと考えるかもしれません。しかし、それは氷山の一角にすぎません。
Agda には、Haskell プログラマーにとってなじみがなく、奇妙なあらゆる種類の型を表現する能力があります。単純なものは、有限集合のタイプです。この型は のように書かれ、数値Fin 3の集合{0, 1, 2}を表します。同様に、Fin 5は数値の集合を表します{0,1,2,3,4}。
これは、現時点では非常に奇妙です。まず、「型」パラメーターとして通常の数値を持つ型を参照しています。Fin n第二に、 set を表すことが何を意味するのかが明確ではありません{0,1...n}。contains実際の Agda では、もっと強力なことを行いますが、関数を定義できると言えば十分です。
contains : Nat -> Fin n -> Bool
contains i f = ?
containsの「自然な」定義は のようなものになるため、これはまた奇妙ですi < nがn、型にのみ存在する値であり、Fin nその分割を簡単に越えることはできないはずです。定義はそれほど単純ではないことがわかりますが、これはまさに帰納型ファミリが依存型付き言語で持つ力です。帰納族は、その型に依存する値と、その値に依存する型を導入します。
Finその定義を調べることで、その特性を与えるのは何であるかを調べることができます。
data Fin : Nat -> Set where
zerof : (n : Nat) -> Fin (succ n)
succf : (n : Nat) -> (i : Fin n) -> Fin (succ n)
これを理解するには少し手間がかかるので、例として type の値を作成してみましょうFin 2。これを行うにはいくつかの方法があります (実際には、正確に 2 つあることがわかります)。
zerof 1 : Fin 2
zerof 2 : Fin 3 -- nope!
zerof 0 : Fin 1 -- nope!
succf 1 (zerof 0) : Fin 2
これにより、2 つの居住者が存在し、型の計算がどのように行われるかを少し示すことができます。特に、 の型の(n : Nat)ビットはzerof、実際の値 を型に反映して、任意のnを形成できるようにします。その後、 を繰り返し適用して、値を正しい型ファミリ インデックス ( にインデックスを付ける自然数)までインクリメントします。Fin (n+1)n : NatsuccfFinFin
これらの能力を提供するものは何ですか？正直なところ、従属型の帰納的なファミリと通常の Haskell ADT の間には多くの違いがありますが、GADT を理解するのに最も関連する正確なものに焦点を当てることができます。
GADT と帰納的ファミリでは、コンストラクタの正確なタイプを指定する機会が得られます。これは退屈かもしれません
data Nat where
Zero :: Nat
Succ :: Nat -> Nat
または、より柔軟なインデックス付きの型がある場合は、別のより興味深い戻り値の型を選択できます
data Typed t where
TyInt :: Int -> Typed Int
TyChar :: Char -> Typed Char
TyUnit :: Typed ()
TyProd :: Typed a -> Typed b -> Typed (a, b)
...
特に、使用される特定の値コンストラクターに基づいて戻り値の型を変更する機能を悪用しています。これにより、一部の値情報を型に反映し、より細かく指定された (ファイバー化された) 型を生成できます。
では、それらに対して何ができるのでしょうか? まあ、少し手間をかければ、Haskell で生成Finできます。簡潔に言えば、自然型の概念を型で定義する必要があります。
data Z
data S a = S a
> undefined :: S (S (S Z)) -- 3
...次に、値をそれらの型に反映するGADT...
data Nat where
Zero :: Nat Z
Succ :: Nat n -> Nat (S n)
...その後、これらを使用Finして、Agda で行ったのと同じように構築できます...
data Fin n where
ZeroF :: Nat n -> Fin (S n)
SuccF :: Nat n -> Fin n -> Fin (S n)
そして最後に、正確に 2 つの値を構築できます。Fin (S (S Z))
*Fin> :t ZeroF (Succ Zero)
ZeroF (Succ Zero) :: Fin (S (S Z))
*Fin> :t SuccF (Succ Zero) (ZeroF Zero)
SuccF (Succ Zero) (ZeroF Zero) :: Fin (S (S Z))
しかし、帰納族よりも利便性が大幅に失われていることに注意してください。たとえば、型に通常の数値リテラルを使用することはできません (ただし、技術的には Agda のトリックにすぎません)。別の「type nat」と「value nat」を作成し、GADT を使用してそれらをリンクする必要があります。また、Agda では型レベルの数学は面倒ですが、それが可能であることがやがてわかります。Haskell では、それは信じられないほど苦痛であり、しばしば不可能です。
たとえばweaken、Agda のFin型で概念を定義することが可能です。
weaken : (n <= m) -> Fin n -> Fin m
weaken = ...
ここで、非常に興味深い最初の値を提供します。これは、「未満の値」のセットに「n <= m未満の値」を埋め込むことを可能にする証明です。技術的にはHaskellでも同じことができますが、型クラスのプロローグを酷使する必要があります。nm
したがって、GADT は、より弱くてぎこちない従属型言語の帰納的ファミリに似ています。そもそも、なぜ Haskell でそれらが必要なのですか?
基本的に、すべての型不変条件が帰納族のフルパワーを表現に必要とするわけではなく、GADT は表現力、Haskell での実装可能性、および型推論の間で特定の妥協点を選択するためです。
有用な GADT 式の例としては、Red-Black プロパティを無効化できない Red-Black Treesや、Haskell 型システムから離れた HOAS ピギーバックとして埋め込まれた単純型付けラムダ計算があります。
実際には、GADT が暗黙の存在コンテキストに使用されることもよくあります。たとえば、タイプ
data Foo where
Bar :: a -> Foo
a存在量化を使用して型変数を暗黙的に非表示にします
> :t Bar 4 :: Foo
時には便利な方法で。よく見ると、ウィキペディアの HOAS の例aでは、コンストラクターの型パラメーターにこれを使用していますApp。GADT なしでそのステートメントを表現することは、実存的なコンテキストの混乱になりますが、GADT 構文はそれを自然にします。
于 2014-01-17T15:31:58.777 に答える
26
GADT は、通常の ADT よりも強力な型強制保証を提供できます。たとえば、この2-3 ツリーの実装のように、バイナリ ツリーを型システム レベルで強制的にバランスさせることができます。
{-# LANGUAGE GADTs #-}
data Zero
data Succ s = Succ s
data Node s a where
Leaf2 :: a -> Node Zero a
Leaf3 :: a -> a -> Node Zero a
Node2 :: Node s a -> a -> Node s a -> Node (Succ s) a
Node3 :: Node s a -> a -> Node s a -> a -> Node s a -> Node (Succ s) a
各ノードには、すべてのリーフが存在するタイプ エンコードされた深度があります。ツリーは、空のツリー、シングルトン値、または深さが指定されていないノードのいずれかであり、これも GADT を使用します。
data BTree a where
Root0 :: BTree a
Root1 :: a -> BTree a
RootN :: Node s a -> BTree a
型システムは、バランスの取れたノードのみを構築できることを保証します。これは、そのようinsertなツリーでのような操作を実装する場合、結果が常にバランスの取れたツリーである場合にのみ、コードが型チェックを行うことを意味します。
于 2013-04-27T11:21:01.007 に答える
17
"Prompt" モナド ("MonadPrompt" パッケージから) がいくつかの場所で非常に便利なツールであることがわかりました ("operational" パッケージからの同等の "Program" モナドとともに)。Monad Reader 第 15 号に「Adventures in Three Monads」という非常に優れた記事があり、Prompt モナドといくつかの現実的な GADT についての良い紹介がありました。 .
于 2010-10-05T14:45:19.690 に答える
4
GHCマニュアルの例が好きです。これは、GADT の中核となるアイデアの簡単なデモです。つまり、操作している言語の型システムを Haskell の型システムに埋め込むことができます。これにより、Haskell 関数は、構文木が適切に型付けされたプログラムに対応していると想定し、強制的に保存することができます。
を定義するときTerm、どのタイプを選択するかは問題ではありません。書くことができます
data Term a where
...
IsZero :: Term Char -> Term Char
また
...
IsZero :: Term a -> Term b
そしての定義Termはまだ通過します。
型が重要になるのは、 の定義などでを計算し たいときだけです。私たちは持っている必要がありますTermeval
...
IsZero :: Term Int -> Term Bool
evalを返すには を再帰的に呼び出す必要があり、を返しIntたいからですBool。
于 2010-10-08T00:13:51.510 に答える
2
これは短い答えですが、Haskell Wikibook を参照してください。よく型付けされた式ツリーの GADT について説明します。これはかなり標準的な例です: http://en.wikibooks.org/wiki/Haskell/GADT
GADT は、型の等価性を実装するためにも使用されます: http://hackage.haskell.org/package/type-equality。このオフハンドについて参照する適切な論文が見つかりません。この手法は、今では民間伝承に浸透しています。ただし、Oleg の型付きタグなしのものでは非常によく使用されます。たとえば、GADT への型付きコンパイルに関するセクションを参照してください。http://okmij.org/ftp/tagless-final/#tc-GADT
于 2010-10-04T23:15:25.130 に答える