Czy mogę uzyskać KnownNat n sugerować KnownNat (n * 3), etc?

Question

pracuję z typów danych tego kształtu, używając V z linear:

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

Mając to ustalone na n jest bardzo ważne, ponieważ chcę, aby być w stanie zapewnić, że ja przechodząc w prawo liczba elementów podczas kompilacji. To część mojego programu, który działa już dobrze, niezależnie od tego, co tu robię.

Dla każdego KnownNat n, mogę wygenerować Foo n spełniając zachowanie, które mój program potrzebuje. Dla celów tej kwestii może być coś głupie jak

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

lub dla bardziej znaczący przykład, może wygenerować losowy V o tej samej długości i używać dot na dwie części. Ograniczenie KnownNat jest tutaj zbędne, ale w rzeczywistości konieczne jest zrobienie Foo. Tworzę jeden Foo i używam go do całego mojego programu (lub z wieloma wejściami), więc to gwarantuje, że za każdym razem, gdy go używam, używam rzeczy o tej samej długości i na rzeczach, które dyktuje struktura Foo.

I wreszcie, mam funkcję, która sprawia, że ​​wejść do Foo:

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

poprzeczkę jest rzeczywiście powodem używam n * 3 jako funkcja typu, zamiast po prostu ręcznie ją rozszerza . Powodem jest to, że bar może wykonać swoją pracę, używając trzech wektorów o długości n i dołączając je wszystkie razem jako wektor o długości n * 3. Ponadto, n jest znacznie bardziej znaczącym parametrem dla funkcji, semantycznie niż n * 3. To także pozwala mi zabronić niewłaściwych wartości jak n „s, które nie są wielokrotnością 3, itd

Teraz, zanim wszystko działało w porządku tak długo, jak zdefiniowano synonim typu od początku:

type N = 5 

I mogę po prostu przekazać w Proxy :: Proxy N do bar i użyć mkFoo :: Foo N. I wszystko działało dobrze.

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

Ale teraz chcę, aby móc dostosować N podczas wykonywania przez załadowanie danych z pliku lub z argumentów wiersza poleceń.

Próbowałem robić to poprzez wywołanie reflectNat:

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

Ale ... bar i mkFoo wymagają KnownNat (n * 3), ale reflectNat po prostu daje mi KnownNat n.

Czy istnieje sposób, w jaki mogę uogólnić dowód, że reflectNat daje mi do spełnienia foo?

Answer 1

zamieścić kolejną odpowiedź, ponieważ jest bardziej bezpośredni, edytując poprzedni nie ma sensu.

W rzeczywistości, stosując podstęp (spopularyzowany jeśli nie wymyślił Edward Kmett), z reflectionsreifyNat:

{-# 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)) 

Więc kiedy go uruchomić:

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

Sztuką jest oparty na fakcie, że w GHC słowniki jednej klasy (takie jak KnownNat) są reprezentowane przez samego członka. W przypadku KnownNat okazuje się, że jest to Integer. Mamy tam tylko unsafeCoerce. Uniwersalne kwantyfikowanie sprawia, że ​​brzmi on z zewnątrz.

Answer 2

Twoje pytanie nie jest bardzo opisowe, więc postaram mojej mocy, aby czuć półfabrykatów:

Załóżmy, że Blah n jest Proxy n.

Zakładam również, że reflectNat jest sposobem wywoływania uniwersalnej kwantyfikacji (nad typelelą Nat) funkcji, z użyciem liczby naturalnej na poziomie sem.

Nie znam lepszego sposobu niż pisanie własnego reflectNat pod warunkiem, że

{-# 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) 

---

Alternatywnie, przy użyciu singletons można użyć SomeSing. Następnie typy będą różne

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

tj. zamiast magicznego dyktafonu KnownNat masz konkretną wartość singleton. Tak więc w foo musisz jawnie napisać SomeSing (1 + n), biorąc pod uwagę SomeSing n - co jest dość proste.

W czasie wykonywania zarówno KnownNat słownik i SomeSing wartość zostanie przekazany wokół załadowane wartości liczbowej i wyraźny jest IMHO lepiej w tym situation.p)

Answer 3

Tak więc, trzy miesiące później chodziłem tam iz powrotem po dobrych sposobach, aby to osiągnąć, ale w końcu zdecydowałem się na bardzo zwięzłą sztuczkę, która nie wymaga żadnych nowych wyrzuconych typów; obejmuje użycie biblioteki Dict z biblioteki ; można łatwo napisać:

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) 

A gdy pojawi się Dict (KnownNat (n * 3) można wzór mecz na to, aby uzyskać instancję (n * 3) w zakresie:

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

Rzeczywiście można je skonfigurować jako uniwersalne, zbyt :

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) 

Albo można uczynić je operatorom i można z nich korzystać, aby "połączyć" dicts:

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

i można zrobić rzeczy jak:

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

mam owinięte to w ładnym biblioteki, typelits-witnesses że używam. Dziękuję wszystkim za pomoc!