5

これは、Haskell の Data.Reflection に関するタイプの質問です。リフレクションを使用すると、Int を取得して型に変換できます。

以下の関数 f と g は、合理的な方法で最善を尽くしたものです。

たとえば、次のようにして 41 を法とする数値を追加できます。

import Data.Reflection
import Data.Proxy

newtype Zq q i = Zq i deriving (Eq)
instance (Reifies q i, Integral i) => Num (Zq q i) where
   (...)
zqToIntegral :: (Reifies q i, Integral i) => Zq q i -> i
   (...)

f :: forall i . (Integral i) => i -> (forall q . Reifies q i => Zq q i) -> i
f modulus k = 
    reify modulus (\ (_::Proxy t) -> zqToIntegral (k :: Zq t i)

それで

>>:t (f 41 (31+15))
(f 41 (31+15)) :: Integral i => i

ただし、次のような関数を書きたいと思います。

g :: forall i . (Integral i) => i -> (forall q . Reifies q i => Zq q i) -> Zq q i
g modulus k = 
    reifyIntegral modulus (\ (_::Proxy t) -> (k :: Zq t i)

そして取得したい：

>>:t (g 41 (31+15))
(g 41 (31+15)) :: <some type info> => Zq q i

違いは、具体化された int を使用する型を返せるようにしたいということです。上記の定義に関する少なくとも 1 つの問題は、ランク 2 の型 q が戻り値の型から見えないことです。

Data.Reflection の reify の署名は次のとおりです。

reify :: a -> (forall s. Reifies s a => Proxy s -> r) -> r

私たちが知る限り、これにはランク 2 の型が必要であり、この型を関数の戻り値の型に公開する方法が (実際に可能であれば) わかりません。

4

1 に答える 1

1

値を型に持ち上げることができます。しかし、その型はリフティングを行う関数から逃れることができません。それがランク 2 タイプの仕組みです。あなたが説明したように書くことができたら想像してみgてください。次に、ユーザー入力値が与えられると、Zq実行時にさまざまな q を取得できます。

しかし、それでは、彼らに何ができるでしょうか?

Zq同じが 2 つある場合はq、それらを追加できます。しかし、それらが同じ q であるかどうかは実行時までわかりません! コンパイル時に追加できるかどうかを判断する必要があるため、型を確認するには遅すぎます。ファントム位置にあるという事実を無視すると、これは、入力に基づいてコンパイル時にまたはqを返す関数を使用できないのと同じ理由です（もちろん、を使用できます）。IntBoolEither

したがって、コメントに記載されているように、いくつかの異なることができます。

できることの 1 つは、実行時にモジュラス (つまり、 の値レベル バージョンq) を結果と共に返すことです。その後、いつでも使用できます。

それは次のようになります。

g :: forall i . (Integral i) => i -> (forall q . Reifies q i => Zq q i) -> (i,i)
g modulus k = reify modulus (\ m@(_::Proxy t) -> (zqToIntegral (k :: Zq t i), reflect m))

他にできることは、次のように存在を使用することです。

data ZqE i = forall q. ZqE (Zq q i)

h :: forall i . (Integral i) => i -> (forall q . Reifies q i => Zq q i) -> ZqE i
h modulus k = reify modulus (\ (_::Proxy t) -> ZqE (k :: Zq t i))

ZqE でできることは、それをアンパックしてq、型で直接公開されない何かを返すことだけです。

qin の 2 つが等しいことを知る方法がZqEないため、それらを直接結合する操作を行うことはできず、同じreify呼び出しですべてを作成する必要があることに注意してください。これはバグではなく、機能です。

于 2013-02-06T03:53:39.270 に答える