haskell - 多態的なデータ構造を GADT にリフトするための型の実行時の比較

Question

型の比較のために GADT を定義するとします。

data EQT a b where
  Witness :: EQT a a

次に、次の型シグネチャで関数eqtを宣言することは可能ですか:

eqt :: (Typeable a, Typeable b) => a -> b -> Maybe (EQT a b)

... typeOf x == typeOf y --- の場合、 eqt xyがJust Witnessと評価され、それ以外の場合はNothingと評価されるようなものですか?

関数eqtを使用すると、通常のポリモーフィックデータ構造を GADT に持ち上げることができます。

score 11 · Accepted Answer

はい、そうです。1 つの方法を次に示します。

まず、型等価型。

data EQ :: * -> * -> * where
  Refl :: EQ a a  -- is an old traditional name for this constructor
  deriving Typeable

それ自体を Typeable のインスタンスにすることができることに注意してください。それが鍵です。あとは、このように、必要な Refl を手に入れるだけです。

refl :: a -> EQ a a
refl _ = Refl

これで、Data.Typeable のキャスト演算子を使用して、(Refl :: Eq aa) を (Eq ab) 型に変換することができます。これは、a と b が等しい場合に機能します。

eq :: (Typeable a, Typeable b) => a -> b -> Maybe (EQ a b)
eq a _ = cast (refl a)

大変な作業はすでに行われています。

このテーマのその他のバリエーションは Data.Witness ライブラリにありますが、この仕事に必要なのは Data.Typeable キャスト演算子だけです。もちろん、それは不正行為ですが、安全にパッケージ化された不正行為です。

1 に答える 1