14

メタプログラミングを行う場合、Haskell の型システムに、プログラムで認識されているが Hindley-Milner では推論できない型に関する情報を渡すことが役立つ (または必要になる) 場合があります。Haskell でこれを行うための機能 (つまり、プログラムによる型注釈) を提供するライブラリ (または言語拡張など) はありますか?

異種リスト (たとえば、ライブラリまたは存在量化を使用して実装されたData.Dynamic) を操作していて、そのリストをボグ標準の同種型 Haskell リストに絞り込みたい状況を考えてみましょう。次のような関数を書くことができます

import Data.Dynamic
import Data.Typeable

dynListToList :: (Typeable a) => [Dynamic] -> [a]
dynListToList = (map fromJust) . (filter isJust) . (map fromDynamic)

手動の型注釈を付けて呼び出します。例えば、

foo :: [Int]
foo = dynListToList [ toDyn (1 :: Int)
                    , toDyn (2 :: Int)
                    , toDyn ("foo" :: String) ]

ここfooにリストがあります[1, 2] :: [Int]。これで問題なく動作し、Haskell の型システムが本来の機能を発揮できる強固な基盤に戻りました。

ここで、ほとんど同じことをしたいと想像してみてください。しかし、(a) コードを書いた時点では、 の呼び出しによって生成されるリストの型がどのようなものであるdynListToList必要があるかわかりませんが、(b) プログラムにはこれを理解するために必要な情報のみ (c) 型システムにアクセス可能な形式ではありません。

たとえば、異種のリストからランダムにアイテムを選択し、そのタイプでリストを絞り込みたいとします。によって提供される型チェック機能を使用するData.Typeableと、プログラムはこれを行うために必要なすべての情報を取得しますが、私が知る限り、これが質問の本質です。それを型システムに渡す方法はありません。ここに、私が何を意味するかを示す疑似 Haskell を示します。

import Data.Dynamic
import Data.Typeable

randList :: (Typeable a) => [Dynamic] -> IO [a]
randList dl = do
    tr <- randItem $ map dynTypeRep dl
    return (dynListToList dl :: [<tr>])  -- This thing should have the type
                                         -- represented by `tr`

randItem(リストからランダムな項目を選択すると仮定します。)

の引数に型注釈returnがない場合、コンパイラは「あいまいな型」を持っていることを通知し、それを提供するように求めます。ただし、タイプは書き込み時に不明である (そして異なる可能性がある) ため、手動のタイプ アノテーションを提供することはできません。ただし、型システムが使用できない形式ではあるものの、型は実行時に認識されます (ここでは、必要な型は値traで表されます。詳細については、を参照してください)。TypeRepData.Typeable

疑似コード:: [<tr>]は、私が起こしたい魔法です。型システムに型情報をプログラムで提供する方法はありますか? つまり、プログラムの値に型情報が含まれていますか?

基本的に、私は??? -> TypeRep -> aHaskell の型システムに未知の型の値を取りTypeRep、「私を信じてください、コンパイラー、私は自分が何をしているのか知っています。このことは値を持っています。これで表されますTypeRep。」（これは何をするものではないことにunsafeCoerce注意してください。）

それとも、私を同じ場所に連れて行くのにまったく違う何かがありますか? たとえば、型変数への割り当てを許可する言語拡張機能を想像できます。たとえば、スコープ型変数を有効にする拡張機能の強化バージョンなどです。

(これが不可能または非常に非現実的である場合、たとえば、GHCi に似た完全なインタプリタを実行可能ファイルにパックする必要がある場合は、その理由を説明してください。)

4

3 に答える 3

18

いいえ、できません。要するに、依存型付けされた関数を作成しようとしているということであり、Haskell は依存型付けされた言語ではありません。値を真の型に持ち上げることはできないためTypeRep、目的の関数の型を書き留める方法はありません。これをもう少し詳しく説明するために、まず、タイプの言い回しがrandList実際には意味をなさない理由を示します。次に、やりたいことができない理由を説明します。最後に、実際に何をすべきかについていくつかの考えを簡単に述べます。

存在論

あなたの型シグネチャは、あなたrandListが意味したいことを意味することはできません。Haskell のすべての型変数は普遍的に量化されていることを思い出すと、次のようになります。

randList :: forall a. Typeable a => [Dynamic] -> IO [a]

したがって、私はそれを好きなように呼び出す権利がrandList dyns :: IO [Int]あります。一部のだけでなく、すべて の に対して戻り値を提供できなければなりません。これをゲームと考えると、関数自体ではなく、呼び出し元が を選択できるゲームです。あなたが言いたいこと (これは有効な Haskell 構文ではありませんが、存在データ型1を使用して有効な Haskell に変換できます) は、より似たようなものですa aa

randList :: [Dynamic] -> (exists a. Typeable a => IO [a])

これは、リストの要素がのインスタンスである何らかのタイプであることを約束しますが、必ずしもそのようなタイプであるとは限りません。しかし、これでも問題が 2 つあります。まず、そのようなリストを作成できたとしても、それで何ができるでしょうか? そして第二に、そもそもそれを構築することさえできないことが判明しました。aTypeable

存在リストの要素について知っていることは、それらが のインスタンスでTypeableあるということだけなので、それらで何ができるでしょうか? ドキュメントを見ると、 のインスタンスを取る関数2が2 つしかないことがわかりTypeableます。

したがって、リスト内の要素の型について知っていることは、それらに対してtypeOfandcastを呼び出すことができるということだけです。私たちはそれらを使って他のことを有益に行うことは決してできないので、私たちの存在は（これも有効な Haskell ではありません）同様に良いかもしれません。

randList :: [Dynamic] -> IO [(TypeRep, forall b. Typeable b => Maybe b)]

これは、リストのすべての要素に適用typeOfしcast、結果を保存し、現在は役に立たない存在型の元の値を破棄すると得られるものです。明らかに、TypeRepこのリストの一部は役に立ちません。リストの後半もそうではありません。普遍的に量化された型に戻ったので、 の呼び出し元は、選択した任意の (型付け可能な) に対してa 、 a 、または arandListを取得するよう要求する権利が再び与えられます。（実際、リストのさまざまな要素をさまざまな型にインスタンス化できるため、以前よりもわずかに強力です。）しかし、変換元の型がわかっている場合を除き、変換元の型を理解することはできません。保持しようとしていた型情報が失われました。Maybe IntMaybe BoolMaybe bb

そして、それらが役に立たないという事実を脇に置いても、ここで目的の存在型を構築することはできません。存在型リスト ( ) を返そうとすると、エラーが発生しますreturn $ dynListToList dl。どの特定のタイプで呼び出していdynListToListますか? 思い出してくださいdynListToList :: forall a. Typeable a => [Dynamic] -> [a]。したがって、使用するものを選択するrandList責任があり a dynListToListます。aしかし、どれを選択すればよいかわかりません。繰り返しますが、それが質問のソースです。したがって、返そうとしている型は指定されていないため、あいまいです。3

依存タイプ

では、この存在を有用 (かつ可能)にするものは何でしょうか? 実際にはもう少し多くの情報があり aますTypeRep。それで、それをパッケージ化できるかもしれません：

randList :: [Dynamic] -> (exists a. Typeable a => IO (TypeRep,[a]))

ただし、これでは十分ではありません。とTypeRepは[a]まったくリンクされていません。TypeRepとをリンクする方法aです。

基本的に、あなたの目標は次のようなものを書くことです

toType :: TypeRep -> *

ここで*は、すべてのタイプの種類です。前に種類を見たことがない場合は、それらは型に対するものであり、型は値に対するものです。 *型の* -> *分類、引数が 1 つの型コンストラクタの分類など (たとえば、Int :: *、Maybe :: * -> *、Either :: * -> * -> *、およびMaybe Int :: *.)

これを使用して、次のように記述できます (繰り返しますが、このコードは有効な Haskell ではありません。実際には、Haskell の型システム内でこのようなコードを記述することはできないため、実際には Haskell に似ているだけです):

randList :: [Dynamic] -> (exists (tr :: TypeRep).
                           Typeable (toType tr) => IO (tr, [toType tr]))
randList dl = do
  tr <- randItem $ map dynTypeRep dl
  return (tr, dynListToList dl :: [toType tr])
    -- In fact, in an ideal world, the `:: [toType tr]` signature would be
    -- inferable.

さて、あなたは正しいことを約束しています: リストの要素を分類する型が存在するのではなくTypeRep、対応する型がリストの要素を分類する型が存在するということです。これさえできれば、準備万端です。しかしtoType :: TypeRep -> *、Haskell で書くことは完全に不可能toType trです。これを行うには、値に依存する型であるため、従属型言語が必要です。

これは何を意味するのでしょうか？Haskell では、値が他の値に依存することは完全に許容されます。これが関数です。head "abc"たとえば、値は値に依存します"abc"。同様に、型コンストラクターがあるため、型が他の型に依存することは許容されます。を考慮Maybe Intし、それがどのように依存するかInt。型に依存する値を持つことさえできます! を検討してくださいid :: a -> a。id_Int :: Int -> Intこれは、 、 などの関数のファミリーですid_Bool :: Bool -> Bool。どの関数を使用するかは、 のタイプによって異なりaます。(本当に、id = \(a :: *) (x :: a) -> x; Haskell でこれを書くことはできませんが、できる言語はあります。)

ただし、重要なのは、値に依存する型を持つことはできません。次のようなものが必要になるかもしれません:Vec 7 Int整数の長さ 7 のリストの型である Imagine 。ここで、Vec :: Nat -> * -> *: 最初の引数が type の値でなければならない型Nat。しかし、Haskell ではこのようなことは書けません。4 これをサポートする言語は、依存型付けと呼ばれます (そして、上記のように書くidことができます)。例にはCoqとAgdaが含まれます。(そのような言語はしばしば証明アシスタントとしても機能し、実際のコードを書くのではなく、一般的に研究作業に使用されます。依存型は難しく、日常のプログラミングに役立つようにすることは活発な研究分野です。)

したがって、Haskell では、最初に型に関するすべてをチェックし、そのすべての情報を破棄してから、値のみを参照するものをコンパイルできます。実際、これはまさに GHC が行っていることです。Haskell では実行時に型をチェックできないため、GHC はプログラムの実行時の動作を変更することなく、コンパイル時にすべての型を消去します。これが、(操作上) 実装が簡単で、完全に安全ではない理由unsafeCoerceです。実行時には何もしませんが、型システムに問題があります。したがって、toTypeHaskell 型システムでのようなものを実装することは完全に不可能です。

実際、お気づきのように、目的の型を書き留めて使用することさえできませんunsafeCoerce。いくつかの問題については、これで解決できます。関数の型を書き留めることはできますが、チートによって実装するだけです。それがまさにそのfromDynamic仕組みです。しかし、上で見たように、Haskell 内からこの問題に与える適切な型さえありません。虚数toType関数を使用すると、プログラムに型を与えることができますが、 の型を書き留めることさえできませんtoType!

今何？

だから、あなたはこれを行うことはできません。あなたは何をすべきですか？私の推測では、あなたの全体的なアーキテクチャは Haskell には理想的ではありませんが、私はそれを見たことがありません。実際、Haskell プログラムではあまり表示されませんTypeable。Dynamic(おそらく、彼らが言うように、「Python のアクセントで Haskell を話している」のかもしれません。) 処理するデータ型のセットが限られている場合は、代わりに単純な古い代数データ型にまとめることができる場合があります。

data MyType = MTInt Int | MTBool Bool | MTString String

次に、 を書き、 , またはisMTIntを使用します。filter isMTIntfilter (isSameMTAs randomMT)

それが何であるかはわかりませんが、おそらくこの問題を解決する方法があるでしょう。 unsafeCoerceしかし、率直に言って、自分が何をしているのかを本当に、本当に、本当に、本当に、本当に、本当に理解していない限り、それは良い考えではありません. それでも、おそらくそうではありません。が必要な場合unsafeCoerceは、便利なだけではないことがわかります。

私はDaniel Wagner のコメントに本当に同意します。おそらく、アプローチを最初から考え直したくなるでしょう。繰り返しになりますが、私はあなたのアーキテクチャを見たことがないので、それが何を意味するのかはわかりません。具体的な問題を抽出できれば、スタック オーバーフローに関する別の質問があるかもしれません。

1次のようになります。

{-# LANGUAGE ExistentialQuantification #-}
data TypeableList = forall a. Typeable a => TypeableList [a]
randList :: [Dynamic] -> IO TypeableList

ただし、このコードはいずれもコンパイルされないため、 で記述したexists方がわかりやすいと思います。

2技術的には、 や など、関連すると思われる他の関数がいくつかありtoDyn :: Typeable a => a -> DynamicますfromDyn :: Typeable a => Dynamic -> a -> a。しかし、Dynamic多かれ少なかれ s の周りに存在するラッパーであり、 and sTypeableに依存していつ実行するかを判断します (GHC はいくつかの実装固有の型 and を使用しますが、 /の可能性のある例外を除いて、この方法で実行できます)。新しいことをする。そして、タイプの引数を実際には期待していません; それはただのラッパーです。これらの関数、および他の同様の関数は、 と だけでは利用できない追加の機能を提供しません。(たとえば、typeOfTypeRepunsafeCoerceunsafeCoercedynApplydynApptoDynfromDynacasttypeOfcastDynamicあなたの問題にはあまり役に立ちません!)

3エラーの動作を確認するには、次の完全な Haskell プログラムをコンパイルしてみてください。

{-# LANGUAGE ExistentialQuantification #-}
import Data.Dynamic
import Data.Typeable
import Data.Maybe

randItem :: [a] -> IO a
randItem = return . head -- Good enough for a short and non-compiling example

dynListToList :: Typeable a => [Dynamic] -> [a]
dynListToList = mapMaybe fromDynamic

data TypeableList = forall a. Typeable a => TypeableList [a]

randList :: [Dynamic] -> IO TypeableList
randList dl = do
  tr <- randItem $ map dynTypeRep dl
  return . TypeableList $ dynListToList dl -- Error!  Ambiguous type variable.

案の定、これをコンパイルしようとすると、次のエラーが発生します。

SO12273982.hs:17:27:
    Ambiguous type variable `a0' in the constraint:
      (Typeable a0) arising from a use of `dynListToList'
    Probable fix: add a type signature that fixes these type variable(s)
    In the second argument of `($)', namely `dynListToList dl'
    In a stmt of a 'do' block: return . TypeableList $ dynListToList dl
    In the expression:
      do { tr <- randItem $ map dynTypeRep dl;
           return . TypeableList $ dynListToList dl }

しかし、質問の要点と同様に、必要な型がわからないため、「これらの型変数を修正する型シグネチャを追加する」ことはできません。

4ほとんど。GHC 7.4 は、型をカインドにリフティングし、カインド ポリモーフィズムをサポートしています。GHC 7.4 ユーザーマニュアル のセクション 7.8「種類の多型と昇格」を参照してください。これは Haskell を依存型付けするわけではありません — TypeRep -> *example のようなものはまだ5ではありません — しかし、値のように見えるVec非常に表現力豊かな型を使って書くことができます。

5技術的には、目的のタイプを持っているように見えるものを書き留めることができますtype family ToType :: TypeRep -> *。ただし、これはtypeの値ではなく、昇格したkindの 型を取ります。その上、まだそれを実装することはできません。(少なくとも私はそうは思いませんし、あなたがどう思うかはわかりませんが、私はこの分野の専門家ではありません。) しかし、現時点では、私たちはかなりかけ離れています。TypeRep TypeRep

于 2012-09-05T06:20:57.723 に答える
13

あなたが観察しているのは、型TypeRepが実際には型レベルの情報を持っていないことです。用語レベルの情報のみ。これは残念ですが、関心のあるすべての型コンストラクターを知っていれば、もっとうまくやることができます。たとえば、Ints、リスト、および関数型のみを気にするとします。

{-# LANGUAGE GADTs, TypeOperators #-}

import Control.Monad

data a :=: b where Refl :: a :=: a
data Dynamic where Dynamic :: TypeRep a -> a -> Dynamic
data TypeRep a where
    Int   :: TypeRep Int
    List  :: TypeRep a -> TypeRep [a]
    Arrow :: TypeRep a -> TypeRep b -> TypeRep (a -> b)

class Typeable a where typeOf :: TypeRep a
instance Typeable Int where typeOf = Int
instance Typeable a => Typeable [a] where typeOf = List typeOf
instance (Typeable a, Typeable b) => Typeable (a -> b) where
    typeOf = Arrow typeOf typeOf

congArrow :: from :=: from' -> to :=: to' -> (from -> to) :=: (from' -> to')
congArrow Refl Refl = Refl

congList :: a :=: b -> [a] :=: [b]
congList Refl = Refl

eq :: TypeRep a -> TypeRep b -> Maybe (a :=: b)
eq Int Int = Just Refl
eq (Arrow from to) (Arrow from' to') = liftM2 congArrow (eq from from') (eq to to')
eq (List t) (List t') = liftM congList (eq t t')
eq _ _ = Nothing

eqTypeable :: (Typeable a, Typeable b) => Maybe (a :=: b)
eqTypeable = eq typeOf typeOf

toDynamic :: Typeable a => a -> Dynamic
toDynamic a = Dynamic typeOf a

-- look ma, no unsafeCoerce!
fromDynamic_ :: TypeRep a -> Dynamic -> Maybe a
fromDynamic_ rep (Dynamic rep' a) = case eq rep rep' of
    Just Refl -> Just a
    Nothing   -> Nothing

fromDynamic :: Typeable a => Dynamic -> Maybe a
fromDynamic = fromDynamic_ typeOf

上記のすべてはかなり標準的です。設計戦略の詳細については、GADT とシングルトン タイプについてお読みください。ここで、書きたい関数は次のとおりです。タイプは少しばかげているように見えますが、ご了承ください。

-- extract only the elements of the list whose type match the head
firstOnly :: [Dynamic] -> Dynamic
firstOnly [] = Dynamic (List Int) []
firstOnly (Dynamic rep v:xs) = Dynamic (List rep) (v:go xs) where
    go [] = []
    go (Dynamic rep' v:xs) = case eq rep rep' of
        Just Refl -> v : go xs
        Nothing   ->     go xs

ここでは、ランダムな要素を選択し (サイコロを振ったところ、1 が出ました)、動的な値のリストから一致する型を持つ要素のみを抽出しました。さて、標準ライブラリの通常の退屈な古いもので同じことを行うことができました。Dynamicしかし、私たちができなかっTypeRepたことは、 を意味のある方法で使用することです。でパターン マッチを実行し、TypeRepが示す特定の型で囲まれた値を使用しますTypeRep。

use :: Dynamic -> [Int]
use (Dynamic (List (Arrow Int Int)) fs) = zipWith ($) fs [1..]
use (Dynamic (List Int) vs) = vs
use (Dynamic Int v) = [v]
use (Dynamic (Arrow (List Int) (List (List Int))) f) = concat (f [0..5])
use _ = []

これらの方程式の右側では、さまざまな具象型でラップされた値を使用していることに注意してください。のパターン マッチは、TypeRep実際には型レベルの情報を導入しています。

于 2012-09-05T07:13:14.507 に答える
3

ランタイム データに基づいて、異なる型の値を返す関数が必要です。わかりました。しかし、型の全体的な目的は、値に対して実行できる操作を示すことです。関数から返される型がわからない場合、関数が返す値をどうしますか? それらに対してどのような操作を実行できますか? 次の 2 つのオプションがあります。

  • タイプを読み取り、それがどのタイプであるかに基づいて何らかの動作を実行する必要があります。この場合、基本的に「それはこのタイプですか? その後、この操作を行います...」をテストすることによって、事前に既知のタイプの有限リストに対応することしかできません。これは現在のフレームワークで簡単に可能です。オブジェクトをDynamic返すだけで、 を使用してそれらをフィルタリングし、結果を消費したい人に適用を任せます。さらに、消費者コードではなく生産者コードで型の有限リストを設定することを気にしないのであれば、それがなくても十分に可能です: 各型のコンストラクターで ADT を使用するだけです。この後者のオプションは、可能であれば断然ベストです。DynamicdynTypeRepfromDynamicDynamicdata Thing = Thing1 Int | Thing2 String | Thing3 (Thing,Thing)
  • たとえば、型クラス操作を使用して、まだ知らない型のファミリー全体で機能する操作を実行したい場合。これはよりトリッキーで、概念的にもトリッキーです。なぜなら、型クラス インスタンスが存在するかどうかに基づいてプログラムが動作を変更することは許可されていないためです。これは、型クラス システムの重要なプロパティであり、新しいインスタンスの導入によってプログラムの型チェックを停止するか、型チェックを停止しますが、プログラムの動作を変更することはできません。したがって、入力リストに不適切なタイプが含まれている場合にエラーをスローすることはできません。そのため、ある時点で最初のソリューションに本質的にフォールバックすることを伴わずにできることがあるかどうかはわかりません。
于 2012-09-05T12:51:10.000 に答える