注入型関数に入力を与える方法

Question

私のアプリケーションでは、型が（パラメータ）dの（注入）関数である式を構築しています。たとえば：

op :: Proxy d -> Proxy ('S d) 
op _ = Proxy 

foo :: forall d . Proxy ('S ('S d)) 
foo = op $ op Proxy 

私はfooのような式を構築した後、私はそれを解釈したいと思います：

getValue :: Proxy (d :: Nat) -> Int 
getValue _ = ... 

fooを解釈するために、私はタイプのアプリケーションの構文を使用して、getValue $ foo @'Zを呼び出すことができます。私の意図が常にこのパターンでgetValueと呼ぶことを除いて、それはまあまあです。したがって、ユーザーにの式を'Zに相対的に指定する必要はなく、getValueに固有のプロパティである場合は、getValue fooと書くことができ、おそらくは2になると思います。

NB：foo :: Proxy d -> Proxy ('S ('S d))とgetValue :: (Proxy d1 -> Proxy d2) -> Int、その後、getValueが'Zに関数を適用している：一つの解決策はProxyと明示的な機能入力への入力を行うことです。これは私が望むものを実現しますが、余分なものはProxyです。この余分なものを必要としない方法はありますかProxy？

Answer 1

getValueをgetValue'に変更し、getValue foo = getValue' $ foo @'Zと書きます。

class ReifyNat (n :: Nat) where 
    reifyNat :: Integer 

instance ReifyNat 'Z where 
    reifyNat = 0 

instance ReifyNat n => ReifyNat ('S n) where 
    reifyNat = succ (reifyNat @n) 

getValue :: forall n. ReifyNat n => Proxy n -> Integer 
getValue _ = reifyNat @n 

それとも使用します：

getValue :: (forall (d :: Nat). Proxy d) -> Int 
getValue foo = getValue' $ foo @'Z 

getValue' :: Proxy (d :: Nat) -> Int 
getValue' Proxy = ... 

はここにそれがあなたの最終目標であるならば自然数を具体化するためのより良い方法だ

getValue :: forall n. ReifyNat n => Integer 
getValue = reifyNat 

あなたはおそらく、すべてのを取り除くことができますあなたが望むなら、この方法でProxyの使用。