KnownNat nにKnownNat（n * 3）などを含めることができますか？

Question

は、私が使用して、この形状のデータ・タイプで働いているVlinearから：

type Foo n = V (n * 3) Double -> Double 

私は右に渡していることを保証することができるようにしたいので、それは、かなり重要ですnに固定持ちますコンパイル時の要素数。これは私がここでやっていることとは関係なく、すでにうまくいく私のプログラムの一部です。

KnownNat nについては、私のプログラムに必要な動作を満たすFoo nを生成することができます。この質問の目的のために、

mkFoo :: KnownNat (n * 3) => Foo n 
mkFoo = sum 

以上有意義例えば、それは同じ長さのランダムVを生成することができますし、2にdotを使用するような愚かなものにすることができます。ここではKnownNatの制約は冗長ですが、実際にはFooを作成する必要があります。私はFooを1つ作成し、それを私のプログラム全体（または複数の入力）に使用するので、私はいつでも同じ長さのものとFooの構造が指示するものを使用しています。

そして最後に、私はFooのための入力を作る機能があります。

bar :: KnownNat (n * 3) => Proxy n -> [V (n * 3) Double] 

バーは、実際に私はタイプの関数としてn * 3を使用して、代わりにだけ手動でそれを拡張していた理由であります。その理由は、barは、長さがnの3つのベクトルを使用し、それらをすべて長さがn * 3のベクトルとして追加することによってその仕事を行う可能性があるためです。また、nは、意味的には、n * 3よりもはるかに意味のあるパラメータです。また、これは私が今など、

を3の倍数ではありませんn年代のような不適切な値を禁止することができます、前に、すべてがいる限り、私は最初に型シノニムを定義したとして罰金働いた：

type N = 5 

そして、私はちょうどProxy :: Proxy Nをbarに渡し、mkFoo :: Foo Nを使うことができます。そしてすべてがうまくいった。

-- works fine 
doStuff :: [Double] 
doStuff = let inps = bar (Proxy :: Proxy N) 
      in map (mkFoo :: Foo N) inps 

しかし、今、私は、ファイルから、またはコマンドライン引数から情報をロードすることにより、実行時にNを調整できるようにしたいです。

私はreflectNatを呼び出すことによって、それをやってみました：

doStuff :: Integer -> Double 
doStuff n = reflectNat 5 $ \pn@(Proxy :: Proxy n) -> 
       let inps = bar (Proxy :: Proxy n) 
       in map (mkFoo :: Foo n) inps 

しかし... barとmkFooはKnownNat (n * 3)が必要ですが、reflectNatはちょうど私KnownNat nを与えます。

私はreflectNatが私にfooを満足させるという証拠を一般化する方法はありますか？

Answer 1

それはより直接的であると私は編集、別の答えを投稿以前は意味をなさないでしょう。 reflectionsreifyNatから、（エドワード・Kmettによって発明されていない場合普及）のトリックを使って実際に

：

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE ScopedTypeVariables #-} 
{-# LANGUAGE FlexibleContexts #-} 
import GHC.TypeLits 
import Data.Proxy 
import Unsafe.Coerce 

newtype MagicNat3 r = MagicNat3 (forall (n :: Nat). KnownNat (n * 3) => Proxy n -> r) 

trickValue :: Integer -> Integer 
trickValue = (*3) 

-- No type-level garantee that the function will be called with (n * 3) 
-- you have to believe us 
trick :: forall a n. KnownNat n => Proxy n -> (forall m. KnownNat (m * 3) => Proxy m -> a) -> a 
trick p f = unsafeCoerce (MagicNat3 f :: MagicNat3 a) (trickValue (natVal p)) Proxy 

test :: forall m. KnownNat (m * 3) => Proxy m -> Integer 
test _ = natVal (Proxy :: Proxy (m * 3)) 

だから、あなたはそれを実行します。

λ *Main > :t trick (Proxy :: Proxy 4) test :: Integer 
trick (Proxy :: Proxy 4) test :: Integer :: Integer 
λ *Main > trick (Proxy :: Proxy 4) test :: Integer 
12 

トリックは事実に基づいていますGHCでは、1つのメンバークラス辞書（KnownNatなど）がメンバー自体によって表されているということです。 KnownNat状況ではIntegerとなります。だから我々はただunsafeCoerceそれがある。ユニバーサル定量化は、外部からの音を発する。

Answer 2

あなたの質問は非常に説明的ではないので、私は空白を感じるように全力を尽くすよ：

のはBlah nがProxy nであると仮定しよう。

また、reflectNatは、用語レベルの自然数を使用して、普遍的に定量化された（タイプレベルNat）関数を呼び出す方法です。

私はreflectNatあなたがSomeSingを使用することができますsingletonsを使用して、代わりにその

{-# LANGUAGE RankNTypes #-} 
{-# LANGUAGE GADTs #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE ScopedTypeVariables #-} 
{-# LANGUAGE FlexibleContexts #-} 
import GHC.TypeLits 
import Data.Proxy 

data Vec a (n :: Nat) where 
    Nil :: Vec a 0 
    Cons :: a -> Vec a n -> Vec a (1 + n) 

vecToList :: Vec a n -> [a] 
vecToList Nil = [] 
vecToList (Cons h t) = h : vecToList t 

repl :: forall n a. KnownNat n => Proxy n -> a -> Vec a n 
repl p x = undefined -- this is a bit tricky with Nat from GHC.TypeLits, but possible 

foo :: forall (n :: Nat). KnownNat (1 + n) => Proxy n -> Vec Bool (1 + n) 
foo _ = repl (Proxy :: Proxy (1 + n)) True 

-- Here we have to write our own version of 'reflectNat' providing right 'KnownNat' instances 
-- so we can call `foo` 
reflectNat :: Integer -> (forall n. KnownNat (1 + n) => Proxy (n :: Nat) -> a) -> a 
reflectNat = undefined 

test :: [Bool] 
test = reflectNat 5 $ \p -> vecToList (foo p) 

---

を提供する独自のものを書くより良い方法を知りません。次にタイプが異なる。

reflectNat :: Integer -> (forall (n :: Nat). SomeSing (n :: Nat) -> a) -> a 

Ie.魔法の代わりにKnownNatあなたは具体的なシングルトンの値を持っています。したがって、fooでは、SomeSing nと指定されていると、SomeSing (1 + n)を明示的に構築する必要があります。これは非常に簡単です。

実行時にKnownNat辞書とSomeSing値の両方が数値を持ち歩くの周りに渡され、明示的には、このsituation.pで私見良いです）

Answer 3

3か月後、私はこれを達成するために良い方法で前後していましたが、最終的には全く新しいタイプを必要としない実際の非常に簡潔なトリックに着きました。 constraintsライブラリのDictを使用します。あまりにも、あなたが実際に一般的なように、これらの設定ができ

case triple (Proxy :: Proxy n) of 
    Dict -> -- KnownNat (n * 3) is in scope 

：

natDict :: KnownNat n => Proxy n -> Dict (KnownNat n) 
natDict _ = Dict 

triple :: KnownNat n => Proxy n -> Dict (KnownNat (n * 3)) 
triple p = reifyNat (natVal p * 3) $ 
      \p3 -> unsafeCoerce (natDict p3) 

をそして、あなたはDict (KnownNat (n * 3)を得れば、あなたはパターンマッチ、それはスコープ内(n * 3)インスタンスを取得することができます上：あなたは簡単に書くことができます：

addNats :: (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Dict (KnownNat (n * m)) 
addNats px py = reifyNat (natVal px + natVal py) $ 
        \pz -> unsafeCoerce (natDict pz) 

それとも、あなたは彼らに演算子を作ることができますし、Dicts "結合" するためにそれらを使用することができます。

を私は素敵なライブラリでこれを包んまし

case d1 %* d2 %+ d3 of 
    Dict -> -- in here, KnownNat (n1 * n2 + n3) is in scope 

、私が使ってきたtypelits-witnesses：ようの

infixl 6 %+ 
infixl 7 %* 
(%+) :: Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n + m)) 
(%*) :: Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n * m)) 

そして、あなたが行うことができますもの。あなたの助けをありがとう！