Deprecated in favour of harpie
This package provides an interface into the numhask API, and both type and value level shape manipulation routines.
:set -XRebindableSyntax
import NumHask.Prelude
import NumHask.ArrayIn situations where shape is only known at run-time, a clear module configuration is:
import NumHask.Array.Shape
import qualified NumHask.Array.Fixed as F
import qualified NumHask.Array.Dynamic as D‘chol’ uses the Cholesky-Crout algorithm.
:r
:set -Wno-type-defaults
:set -Wno-unused-do-bind
:set -Wno-name-shadowing
:set -XOverloadedStrings
:set -XOverloadedLabels
:set -XRebindableSyntax
:set -XDataKinds
import Data.Functor.Rep
import NumHask.Prelude
import NumHask.Array.Fixed qualified as F
import NumHask.Array.Shape qualified as S
import NumHask.Array.Dynamic qualified as D
putStrLn "ok"
‘chol’ uses the Cholesky-Crout algorithm.
Example from https://rosettacode.org/wiki/Cholesky_decomposition#Haskell
a = [25, 15, -5 ,15, 18, 0 ,-5, 0, 11] :: Matrix 3 3 Double
b = [ 18, 22, 54, 42 , 22, 70, 86, 62 , 54, 86, 174, 134 , 42, 62, 134, 106] :: Matrix 4 4 Double
chol a
chol b
fmap (fixed (Just 3)) (a `mmult` recip a)
fmap (fixed (Just 3)) (b `mmult` recip b)
fmap (fixed (Just 3)) (dot sum (*) b (recip b))[[5.0, 0.0, 0.0], [3.0, 3.0, 0.0], [-1.0, 1.0, 3.0]] [[4.242640687119285, 0.0, 0.0, -5.102196573270443e-15], [5.185449728701349, 6.565905201197403, 0.0, 0.0], [12.727922061357857, 3.0460384954008553, 1.6497422479090704, 0.0], [9.899494936611667, 1.624553864213788, 1.8497110052313648, 1.3926212476456026]] [["1.000", "0.000", "-0.000"], ["0.000", "1.000", "0.000"], ["-0.000", "0.000", "1.000"]] [["1.000", "0.000", "-0.000", "0.000"], ["-0.000", "1.000", "-0.000", "0.000"], ["-0.000", "0.000", "1.000", "0.000"], ["-0.000", "0.000", "-0.000", "1.000"]] [["1.000", "0.000", "-0.000", "0.000"], ["-0.000", "1.000", "-0.000", "0.000"], ["-0.000", "0.000", "1.000", "0.000"], ["-0.000", "0.000", "-0.000", "1.000"]]
:r
:set -Wno-name-shadowing
:set -Wno-type-defaults
:set -XNoImplicitPrelude
import NumHask.Prelude as P
import NumHask.Array.Dynamic qualified as D
import NumHask.Array.Shape as S
import NumHask.Array.Fixed as F
import Prettyprinter
a = fmap (1+) $ range [2,3,4] :: D.Array Int
pretty a
-- :t \d o l a -> backpermute (S.setDim d l) (S.modifyDim d (+o)) a
a = D.array [3,3] [4,12,-16,12,37,-43,-16,-43,98] :: D.Array Double
pretty (D.chol a)
D.mult (D.chol a) (D.transpose (D.chol a)) == a
pretty (D.inverse a)
D.mult (D.inverse a) a == a
a = D.array [3,3] ([1,0,1,0,1,2,0,0,1] :: [Double]) :: D.Array Double
n = D.shape a !! 0
ti = D.undiag 2 (fmap recip (D.diag a))
tl = zipWith (-) a (D.undiag 2 (D.diag a))
l = fmap negate (D.dot sum (*) ti tl)
l
-- fmap (sum (fmap (l ^) (fmap fromIntegral $ D.range [n])) *) ti
seq = D.range [n] :: D.Array Int
x' = fmap (\x -> fmap (^x) l) seq
D.shape x'
D.shape (x' ! [0,0])
foldr (zipWith (+)) (x' ! [0]) (D.tails [0] x')
D.isScalar $ heads [0] x'
x' ! [0]
D.tails [0] x'
import NumHask.Array.Fixed as F
import Data.Functor.Rep
:set -XOverloadedLists
a' = [1,0,1,0,1,2,0,0,1] :: F.Array '[3,3] Double
n = F.shape a' !! 0
ti = F.undiag (fmap recip (F.diag a'))
tl = a' - (F.undiag (F.diag a'))
l = fmap negate (F.dot sum (*) ti tl)
invtri a'
:t l
(l ^ 1)
(l ^^ 2)
a = D.array [3,3] ([1,0,1,0,1,2,0,0,1] :: [Double]) :: D.Array Double
n = D.shape a !! 0
ti = D.undiag 2 (fmap recip (D.diag a))
tl = zipWith (-) a (D.undiag 2 (D.diag a))
l = fmap negate (D.dot sum (*) ti tl)
pow a n = foldr ($) (D.ident [3,3]) (replicate n (D.mult a))
:t pow
pow l 2
add = zipWith (+)
sum' = foldl' add (D.konst [3,3] 0)
:t sum'
D.mult (sum' (fmap (pow l) (fmap fromIntegral $ D.range [n]))) ti
import Control.Monad
xs n = replicateM n . uniformRM (0,1)
:t xs
gen <- newIOGenM (mkStdGen 42)
:t xs 10 gen :: IO [Double]
import qualified Data.List as List
x = range [2,3]
x
D.backpermute (List.drop 1 :: [Int] -> [Int]) x
D.range (D.toScalar 3)
D.join $ D.tabulateA (D.toScalar 3) id
D.join $ D.tabulate (D.toScalar 3) id
D.tabulate (D.toScalar 3) id
D.tabulateA (D.toScalar 3) id
m = D.array [3,4] [0..11]
m
D.zipWith (-) m m
D.zipWith (-) m m
(x:|xs) = array [4] [0..3]
x
xs
(x:|xs)
Apply a binary fnuction to sub-components of an array matching the size of the second array, and an array.
import qualified Data.List as List
a = D.array [2,3] [0..5]
b = D.array [3] [0..2]
D.extracts [1] a
D.extracts [0] b
f = D.concatenate 0
D.transmits [(1,0)] f a b
let a = D.array [2,3,4] [0..23] :: D.Array Int
pretty a
pretty $ (D.shape @[Int]) <$> D.extracts [0] a
s = D.tabulate [] (const 0) :: D.Array Int
s
pretty s
s1 = D.array [1] [0]
s1
pretty s1
s2 = D.toScalar 0
s2
pretty s2
s3 = tabulate [] (const 3) :: D.Array Int
s3
s3' = tabulate [1] (const 3) :: D.Array Int
s3'
s3'' = tabulate (Scalar 1) (const 3) :: D.Array Int
s3''
D.indices []
D.indices [3]
D.indices (Scalar 3)
D.indices (D.array [] [3])
D.indices [2,3]
joins' $ fmap D.asArray $ D.indices []
joins' $ fmap D.asArray $ D.indices [3]
joins' $ fmap D.asArray $ D.indices (Scalar 3)
joins' $ fmap D.asArray $ D.indices (D.array [] [3])
joins' $ fmap D.asArray $ D.indices [2,3]
import NumHask.Array.Shape as S
:set -Wno-x-partial
a = D.array [] [3]
D.diag a
D.diag (D.array [3] [1,2,3])
D.diag (D.ident [3,2])
-- D.tabulate [S.minimum (zero:D.shape a)] (\xs -> index a (replicate (D.rank a) (head xs)))
-- D.tabulate [] (\xs -> index a (replicate (D.rank a) (head xs)))
-- S.minimum ((D.shape a) :: [Int])
-- index a []
D.indexes [2] [1] (D.array [] [3::Int])
D.indexes [0] [2] (D.array [3] [0..2::Int])
m = D.reshape [2,3] (D.range [6])
pretty m
D.indexes [1] [0] (D.reshape [2,3] (D.range [6]))
D.indexes [1] [2] (D.reshape [2,3] (D.range [6]))
D.indexes [0,1] [1,2] (D.reshape [2,3] (D.range [6]))
:t D.index @[Int]
:t \a -> D.index @_ @[Int] a
:t D.index @_ @[Int]
pretty $ D.folds [0,1] (sum . fmap (const one)) a
D.extracts [0,1] a
D.joins [0,1] (D.extracts [0,1] a)
D.joins [0,1] $ D.extracts [1,0] $ D.joins [1,0] (D.extracts [0,1] a)
pretty $ D.maps (D.reverses [0]) [0] a
pretty $ D.insert 2 2 a (D.array [2,3] [100..105])
S.index (D.shape a) 2
S.reverseIndex [0] [] []
S.reverseIndex [0] [5] [0]
S.reverseIndex [0] [5] [4]
S.reverseIndex [2] [2,3,4] [0,1,2]
:t (\ds ns xs -> fmap (\(i,x,n) -> bool x (n-1-x) (i `elem` ds)) (zip3 [0..] xs ns))
pretty $ D.reverses [0] $ D.array [3,2] [1..6]
import Data.Proxy
import NumHask.Array.Fixed as F
:t with (D.array @[Int] [2,3,4] [1..24]) (NumHask.Array.Fixed.indexes (Proxy :: Proxy '[0,1]) [1,1] :: F.Array '[2,3,4] Int -> F.Array '[4] Int)
pretty $ with (D.array @[Int] [2,3,4] [1..24]) (NumHask.Array.Fixed.indexes (Proxy :: Proxy '[0,1]) [1,1] :: F.Array '[2,3,4] Int -> F.Array '[4] Int)
let a = D.array [2,3,4] [0..23] :: D.Array Int
a
m = D.array [3,2] [0..5]
(x:|xs) = D.array [3,2] [0..5]
pretty x
pretty xs
D.indexes' [(0,0)] m
D.drops [1,0] m
S.shapen [] 20
S.flatten [] []
S.deleteDim [] 2
S.setDim 0 1 []
S.modifyDim 0 (+1) []
S.setDim 1 3 []
S.reverseIndex [0] [] []
S.rotateIndex [(0,1)] [] [1]
D.stretch 0 (D.toScalar 1)
x = D.toScalar 1 :: D.Array Int
y = D.toScalar 2 :: D.Array Int
D.length x
fmap (+1) x
-- > toScalar x == D.tabulate [] (const x)
D.index x []
D.indices []
D.indexes [] x
D.indexes [(0,0)] x
D.indexes [(2,2)] x
D.takes [] x
D.takes [(0,1)] x
D.takes [(1,1)] x
-- D.drops [(0,0)] x
-- D.row 0 (D.toScalar 2)
-- D.concatenate 0 (D.toScalar 2) (D.toScalar 3)
A.divide (D.toScalar 1) (D.toScalar 2)
:set -XPolyKinds
:t Array @[2,3]
fromList [1..24] :: Array [2,3,4] Int
APLicative Programming with Naperian Functors
:r
:set -Wno-name-shadowing
:set -Wno-type-defaults
:set -XNoImplicitPrelude
import NumHask.Prelude as P
import NumHask.Array.Dynamic qualified as D
import NumHask.Array.Shape as S
import NumHask.Array.Fixed as F
import Prettyprinter
import GHC.TypeNats
import Data.Proxy
import Test.QuickCheck
import Data.Vector qualified as V
a = range @[2,3,4]
pretty a
:t a
a = aVector [2,3,4]
:t a
show a
a' = aVector' [2,3,4]
:t a'
show a'
show a'
(\(SomeVector' (SNat :: SNat n) a) -> toDynamic @'[n] a) a'
(\(SomeVector' sn _) -> fromSNat sn) a'
(\(SomeVector' _ v) -> asVector v) a'
example_append a
example_append' a'
example_insert a
example_insert' a'
Cannot satisfy 1 <= n
example_delete' :: (Show a) => SomeVector' a -> String
example_delete' (SomeVector' (SNat :: SNat n) a) = show (delete (SNat @0) 0 a)
:t (\(SomeVector' (SNat :: SNat n) v) -> delete (SNat @0) 0 v) a'
import GHC.TypeNats
:i SNat
x = SNat @1
:t x
x
y = natSing @2
:t y
y
fromSNat x
:{
import Data.Proxy
f :: forall n. SNat n -> Nat
f SNat = natVal (Proxy :: Proxy n)
:}
f (SNat @4)
withSomeSNat 5 f
For when you have both an SNat input and a KnownNat constraint (which is always in this API).
Uses both withKnownNat and withSomeNat. Very similar to reifyNat …
reifyNat :: forall r. Integer -> (forall (n :: Nat). KnownNat n => Proxy n -> r) -> r
reifyNat n k = TN.withSomeSNat (fromInteger n :: Numeric.Natural) $
\(sn :: (SNat n)) -> TN.withKnownNat sn $ k (Proxy :: Proxy n)
:t \n -> vector' n [2,3,4::Int]
vector' (SNat @3) [2,3,4::Int]
withSomeNat 3 (\n -> pretty $ vector' n [2,3,4])
withSomeNat 2 (\n -> pretty $ vector' n [2,3,4])
withSomeNat 3 (\n -> vector' n [2,3,4])
withSomeSNat works where there are no external upstream KnownNat constraints (which is almost never).
withSomeSNat 3 (\n -> show $ vector' n [2,3,4])
withSomeSNat 3 (\n -> pretty $ vector' n [2,3,4])
withKnownNat needs to be nailed down to work:
:t withSomeNat
:t vector [2,3,4]
:t \n -> withKnownNat n (vector [2,3,4])
f = (\n -> withKnownNat n (vector [2,3,4])) :: (forall n. KnownNat n => SNat n -> Array '[n] Int)
:t f
withSomeNat 3 (pretty . f)
:t vector [2,3,4]
:t \n -> withKnownNat n (pretty (vector [2,3,4]))
:t withKnownNat
Simple example:
https://snakamura.github.io/log/2021/9/length_indexed_vector.html
:t withSomeNat
s = someVector' (SNat @3) [2,3,4]
show s
-- :t withKnownNat (SNat @3) (show $ someVector [2,3,4])
v = aVector' [2,3,4]
show v
v = aVector [2,3,4]
show v
Existentials on a leash:
https://github.com/cdfa/existentials-on-a-leash
HMatrix uses an SNat:
A SomeVec that uses SNat rather than KnownNat:
Sigma usage:
rvs <- sample' arbitrary :: IO [SomeVector' Int]
show rvs
withKnownNat
:t \xs -> vector xs
:t \xs -> (\(SNat :: SNat n) -> vector @n xs)
:t \xs sn -> withKnownNat sn (vector xs)
g = \xs -> (\(SNat :: SNat n) -> vector @n xs)
:t g
More complicated functions look too hard.
a = F.range @[2,3,4]
F.take (SNat @1) (SNat @2) a
withSomeNat 2 (\sd -> show (F.take (SNat @2) sd a))
instance GArbitrary SNat where
garbitrary = do
n <- arbitrary
TN.withSomeSNat n (pure . Some)
instance Arbitrary SomeSNat where
arbitrary :: Gen SomeSNat
arbitrary = do
n <- fromInteger . getNonNegative <$> arbitrary
return $ withSomeSNat n SomeSNat
:t someNatVal 5
:t withKnownNat
:t iota
withKnownNat (SNat @4) iota
:{
withKnownNat' :: Nat -> (forall n. KnownNat n => r) -> r
withKnownNat' n f = withSomeSNat n $ \(SNat :: SNat n) -> f @n
:}
withKnownNat' 4 iota
AllowAmbiguousTypes injectivity
https://www.youtube.com/watch?v=1vd9mvH8Bos&list=PLD8gywOEY4HaG5VSrKVnHxCptlJv2GAn7&index=4
:{
withKnownNat2 :: (forall n1 n2 . (KnownNat n1, KnownNat n2) => r) -> Natural -> Natural -> r
withKnownNat2 f n1 n2 = withSomeSNat n1 $ \(SNat :: SNat n1) ->
withSomeSNat n2 $ \(SNat :: SNat n2) ->
f @n1 @n2
:}
:t \d x -> withKnownNat2 (F.take d x a) 1 2
https://hackage.haskell.org/package/fin-0.3.1/docs/Data-Type-Nat.html#t:SNatI
https://github.com/Mikolaj/horde-ad/blob/master/src/HordeAd/Core/Types.hs
:{
withSNat :: Int -> (forall n. KnownNat n => (SNat n -> r)) -> r
withSNat i f = withSomeSNat (fromIntegral i) $ \msnat -> case msnat of
snat@SNat -> f snat
:}
:t withSNat 5
a = F.range @[2,3,4]
pretty $ F.take (SNat @1) (SNat @2) a
:t withSomeSNat 5
a = F.range @[2,3,4]
pretty $ F.take (SNat @1) (SNat @2) a
:t withSomeSNat 5 iota
:t \d x -> withSomeSNat d $ \(SNat @d) -> (withSomeSNat x $ \(SNat @x) -> F.take (SNat @d) (SNat @x) a)
:t \n -> withSomeSNat n (\(SNat @n) -> iota @n)
https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/37
-- Convert regular Int to type
-- Can't simply do: exists n. Int -> Proxy n
-- Existential trick: Use CPS
reifyNat :: Int -> (forall n. KnownNat n => Proxy n -> r) -> r
reifyNat 0 k = k (Proxy :: Proxy Z)
reifyNat n k = reifyNat (n - 1) $ \(Proxy :: Proxy n_1) -> k (Proxy :: Proxy (S n_1))
-- As found in the `reflection` library
reifyNat :: Integer -> (forall (n :: Nat). KnownNat n => Proxy n -> r) -> r
reifyNat n k = withSomeSNat n $ \(mbSn :: Maybe (SNat n)) ->
case mbSn of
Just sn -> withKnownNat sn $ k @n Proxy
Nothing -> throw Underflow
import GHC.TypeLits.KnownNat.Solver
:{
-- | proof that plugin exists and is working
pluginf' :: forall n . KnownNat n => Proxy n -> Nat
pluginf' _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2))
:}
https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/5
https://github.com/goldfirere/singletons/blob/master/README.md
:{
example_inserta :: (Show a, FromInteger a) => SomeArray a -> String
example_inserta (SomeArray (SNats :: SNats ns) a) = show (insert (SNat @0) (SNat @0) a (toScalar 0))
:}
-- (If (s Data.Type.Equality.== '[]) '[1] s)’
-- arising from a use of ‘insert’
segfaults as SNats is somehow SNat @’[]
:{
import Fcf (Eval)
someTakeDim :: forall d t s. (KnownNats s, KnownNat d, KnownNat t) => SNats (Eval (TakeDim d t s))
someTakeDim = withSomeSNats (fromIntegral <$> takeDim (int (SNat :: SNat d)) (int (SNat :: SNat t)) (ints (SNats :: SNats s))) unsafeCoerce
example_take :: forall a s. (KnownNats s, Show a) => Nat -> Nat -> Array s a -> String
example_take d t a =
withSomeSNat d
(\(SNat :: SNat d) ->
withSomeSNat t
(\(SNat :: SNat t) ->
case someTakeDim @d @t @s of
SNats -> show $ F.take (SNat @d) (SNat @t) a))
:}
but this is ok
:{
someTakeDim2 :: forall d t s. (KnownNats s, KnownNat d, KnownNat t) => SNats (Eval (TakeDim d t s))
someTakeDim2 = UnsafeSNats (fromIntegral <$> takeDim (int @d) (int @t) (ints @s))
example_take' :: forall a s. (KnownNats s, Show a) => Nat -> Nat -> Array s a -> String
example_take' d t a =
withSomeSNat d
(\(SNat :: SNat d') ->
withSomeSNat t
(\(SNat :: SNat t) ->
case someTakeDim2 @d' @t @s of
x -> show x <> " " <> show (someTakeDim2 @d' @t @s) <> " : take " <> show (SNat @d') <> " " <> show (SNat @t) <> " " <> show a))
:}