Data.Type.Equalityパターンマッチングを別の関数に抽出することは可能ですか？

Question

いくつかのテストコードでは、単体実装を使用して多態関数を実装できる関数を書いています。それはこのようになります使用

assertEq :: forall a b. (Show a, Typeable a, Typeable b) => a -> (a :~: b) 
assertEq x = fromMaybe (error errorMessage) eqT 
    where errorMessage = 
      "expected value of type ‘" <> show (typeRep (Proxy :: Proxy b)) 
     <> "’, but got ‘" <> show x 
     <> "’, which is of type ‘" <> show (typeRep (Proxy :: Proxy a)) <> "’" 

：

insertUser :: forall record m. (RelationalEntity record, Monad m) => record -> m (Either (Entity record) (Key record)) 
insertUser user = case (assertEq user :: record :~: User) of 
    Refl -> return . Right $ UserId 1234 

重要なのは、型シグネチャは、任意のRelationalEntityのために動作しますが、それは実際にUserを期待し、私はそれがこのようData.Type.Equalityを使用して実装しました。通常、この種の関数はうまくいくでしょうが、例外が発生すると単にテストが失敗するため、テストコードでうまく動作します。これはまさに私が望むものです。

もちろん、assertEqを使用しているのはやや言い方です。幸運なことに、Haskellは参照透過性を持っているので、caseの一致をヘルパー関数にパックするのは本当に簡単でしょうか？

withAssertEq :: forall a b c. (Show a, Typeable a, Typeable b) => a -> (b -> c) -> c 
withAssertEq x f = case (assertEq x :: a :~: b) of Refl -> f x 

は、今私は insertUser内から withAssertEqを使用することができるはずです：：まあ、私はそれを実行しようとしました

insertUser :: forall record m. (RelationalEntity record, Monad m) => record -> m (Either (Entity record) (Key record)) 
insertUser x = withAssertEq x $ \(_ :: User) -> 
    return . Right $ UserId 1234 

は残念ながら、これはです。TypeCheckしません。タイプチェッカーがReflのパターンマッチから得た情報がwithAssertEqの範囲内で使用に伝播しないので、タイプチェッカーは期待される結果であるKey recordを実際の結果であるKey Userと統一することができません。

はのような種類の情報を伝播する関数を書く方法はありますか？あるいは、タイプ平等に関する情報を型チェッカーに伝えるために、case式を直接使用するには、にが必要ですか？

Answer 1

gcastWithをご覧ください。

gcastWith :: a :~: b -> (a ~ b => r) -> r 
gcastWith Refl x = x 

このタイプは少し読んでいます。 gcastWithは、等価プルーフ（a :~: b）と、a ~ b（a ~ b => r）と仮定して型チェックする値をとり、その仮定を排除してその値を返します（r）。

gcastWithのボディで行われている作業は、Reflのパターンマッチングです。これはgcastWithの体でa ~ bの等価性を持つコンテキストをシードし、GHCは忠実にxのタイプになります。かなりクール！

つまり、あなたのwithAssertEqのためのテンプレートとしてgcastWithの型を使用することができます。

withAssertEq :: forall a b r. (Typeable a, Typeable b) => Proxy a -> Proxy b -> (a ~ b => r) -> r 
withAssertEq _ _ = gcastWith (fromJust eqT :: a :~: b) 

Proxy sがTypeable辞書はaとbに使用するGHCに伝えるために呼び出しサイトが有効になっています。型がないとあいまいチェックに失敗します。

通常の注意点が適用されますが、部分的な機能は使用しないでください。