5

簡単な言語を考えると、

data E where
  ValE :: Typeable a => a -> E
  AppE :: E -> E -> E

それを型付き表現に変換することは可能ですか:

data T a where
  ValT :: Typeable a => a -> T a
  AppT :: T (a -> b) -> T a -> T b
  deriving Typeable

次のようなさまざまなアプローチを試しました。

e2t :: Typeable a => E -> Maybe (T a)
e2t (ValE x) = cast (ValT x)
e2t (AppE e1 e2) = liftM2 AppT (e2t e1) (e2t e2)

これは機能せず、次のエラー メッセージが表示されます。

制約内のあいまいな型変数 'a':
'Typeable a'
は、'e2t' の使用に起因します ...
推定修正: これらの型変数を修正する型シグネチャを追加します

しかし、もし私がこれを好きなら

e2t :: Typeable a => E -> Maybe (T a)
e2t (ValE x) = cast (ValT x)
e2t (AppE e1 e2) = liftM2 AppT (e2t e1) (e2t e2 :: Maybe (T Int))

コンパイルします。

4

1 に答える 1

2

それは正しい。あなたはそれを理解していないかもしれませんが、あなたはあなたの言語で型推論をしようとしています。式を型付きGADTに変換する場合f xは、結果の型を知るだけでは不十分です。f :: Bool -> Intwith x :: Bool、f :: (Int -> Int) -> Intwithなどがありx :: Int -> Intます。そして、型付き表現は、特に定数が必要なため、それを知っていると主張します（制約Typeableがない場合は、型が何であるかを知ることについて嘘をつくことで逃げることができるかもしれません） Typeable。

e2t式がどのタイプであると予想されるかについての知識が必要です。アプリケーションの引数がどのタイプであると予想されるかを判断する方法が必要です。たぶん、あなたはこれを必要とすることを回避することができます、すなわち：

e2t :: E -> Maybe (exists a. T a)

つまりE、タイプを指定できるかどうかを確認しようとしているだけですが、タイプを指定するのではなく、タイプを指定します。これはボトムアップ推論であり、一般的に簡単です。これをエンコードするには：

data AnyT where
    AnyT :: Typeable a => T a -> AnyT

うーん、これでしばらく遊んだ後、戻ってくる途中でまったく同じ問題に遭遇したことに気づきました。だけでこれができるとは思いませんData.Typeable。dynAppfromのようなものを再作成する必要がありますが、通常のHaskellタイプの代わりにsを使用しますData.Dynamic。Tつまり、sに対していくつかの操作を実行し、安全であることがわかったらTypeRep、ある時点で「ただ私を信頼して」を挿入する必要があります。unsafeCoerceしかし、私が知る限り、コンパイラに安全であると納得させることはできません。

これはAgdaで行うことができます。これは、TypeRepsに対する同等の前述の操作がコンパイラーで観察できるためです。その言語を学ぶとき、それはおそらく良い練習になるでしょう。

于 2010-10-31T18:23:10.287 に答える