AsSingleton pre-removal

readme.org

@@ -578,7 +578,7 @@ Failed, three modules loaded.
 #+begin_src haskell-ng :results output
 a = fmap (1+) $ range [2,3,4] :: D.Array Int
 pretty a
--- :t \d o l a -> backpermute (S.replaceDim d l) (S.modifyDim d (+o)) a
+-- :t \d o l a -> backpermute (S.setDim d l) (S.modifyDim d (+o)) a
 #+end_src
 
 #+RESULTS:
@@ -1108,9 +1108,9 @@ D.drops [1,0] m
 S.shapen [] 20
 S.flatten [] []
 S.deleteDim [] 2
-S.replaceDim 0 1 []
+S.setDim 0 1 []
 S.modifyDim 0 (+1) []
-S.replaceDim 1 3 []
+S.setDim 1 3 []
 S.reverseIndex [0] [] []
 S.rotateIndex [(0,1)] [] [1]
 #+end_src
@@ -1965,7 +1965,101 @@ ghci| ghci| ghci| ghci| ghci| ghci| ghci| ghci| ghci| ghci| ghci| ghci|
 
 https://discourse.haskell.org/t/how-to-create-arbitrary-instance-for-dependent-types/6990/5
 
-
 ** singletons
 
 https://github.com/goldfirere/singletons/blob/master/README.md
+
+
+** dependent type examples
+
+#+begin_src haskell-ng :results output
+example_inserta :: (Show a, FromInteger a) => SomeArray a -> String
+example_inserta (SomeArray (SNats :: SNats ns) a) = show (insert (SNat @0) 0 a (toScalar 0))
+-- Could not deduce ‘HasShape
+-- (If (s Data.Type.Equality.== '[]) '[1] s)’
+--    arising from a use of ‘insert’
+#+end_src
+
+segfaults as SNats is somehow SNat @'[]
+
+#+begin_src haskell-ng :results output
+example_take :: forall a s. (HasShape 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 $ take (SNat @d) (SNat @t) a))
+#+end_src
+
+#+begin_src haskell-ng :results output
+example_take' :: forall a s. (HasShape 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))
+#+end_src
+
+example_take' 0 1 (range @[2,3,4])
+"SNats @[1, 3, 4] SNats @[1, 3, 4] : take SNat @0 SNat @1 [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23]"
+
+vector examples
+
+#+begin_src haskell-ng :results output
+data SomeVector a where
+  SomeVector :: KnownNat n => Vector n a -> SomeVector a
+
+deriving instance (Show a) => Show (SomeVector a)
+
+withLength :: forall n a r. Vector n a -> (KnownNat n => r) -> r
+withLength v r = case someNatVal (fromIntegral $ V.length (asVector v)) of
+  SomeNat (Proxy :: Proxy n') -> case unsafeCoerce Refl of
+    (Refl :: n :~: n') -> r
+
+aVector :: FromVector t a => t -> SomeVector a
+aVector (Array . asVector -> v) = withLength v (SomeVector v)
+
+example_append :: (Show a, Num a, FromInteger a) => SomeVector a -> String
+example_append (SomeVector a) = show (append (SNat @0) a (toScalar 0))
+
+example_insert :: (Show a, FromInteger a) => SomeVector a -> String
+example_insert (SomeVector a) = show (insert (SNat @0) 0 a (toScalar 0))
+
+data SomeVector' a = forall n. SomeVector' (SNat n) (Vector n a)
+
+deriving instance (Show a) => Show (SomeVector' a)
+
+someVector' :: FromVector t a => KnownNat n => SNat n -> t -> SomeVector' a
+someVector' n t = SomeVector' n (vector' n t)
+
+aVector' :: forall a t. FromVector t a => t -> SomeVector' a
+aVector' t = withSomeSNat (fromIntegral $ V.length (asVector t)) $ \(SNat :: SNat n) -> SomeVector' SNat (vector' (SNat @n) (asVector t))
+
+example_insert' :: (Show a, FromInteger a) => SomeVector' a -> String
+example_insert' (SomeVector' (SNat :: SNat n) a) = show (insert (SNat @0) 0 a (toScalar 0))
+
+example_append' :: (Show a, Num a, FromInteger a) => SomeVector' a -> String
+example_append' (SomeVector' (SNat :: SNat n) a) = show (append (SNat @0) a (toScalar 0))
+
+instance (Arbitrary a) => Arbitrary (SomeVector' a) where
+  arbitrary = do
+    n <- arbitrary
+    v <- V.replicateM (Prelude.fromIntegral n) arbitrary
+    withSomeNat n $ \sn -> pure (someVector' sn v)
+#+end_src
+
+
+#+begin_src haskell-ng :results output
+someTakeDim :: forall d t s. (HasShape 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
+
+someTakeDim2 :: forall d t s. (HasShape s, KnownNat d, KnownNat t) => SNats (Eval (TakeDim d t s))
+someTakeDim2 = UnsafeSNats (fromIntegral <$> takeDim (int (SNat :: SNat d)) (int (SNat :: SNat t)) (ints (SNats :: SNats s)))
+
+someUnsafeGetIndex :: forall d s. (HasShape s, KnownNat d) => SNat (Eval (UnsafeGetIndex d s))
+someUnsafeGetIndex = withSomeSNat (fromIntegral $ getDim (int (SNat :: SNat d)) (ints (SNats :: SNats s))) unsafeCoerce
+#+end_src

src/NumHask/Array/Dynamic.hs

@@ -723,7 +723,7 @@ drop ::
   Array a
 drop d t a = backpermute dsNew (S.modifyDim d (\x -> x + bool t 0 (t < 0))) a
   where
-    dsNew = S.replaceDim d ((S.unsafeGetIndex d (shape a)) - abs t)
+    dsNew = S.setDim d ((S.getDim d (shape a)) - abs t)
 
 -- | Select an index along a dimension.
 --
@@ -823,7 +823,7 @@ append ::
   Array a ->
   Array a ->
   Array a
-append d a b = insert d (S.unsafeGetIndex d (shape a)) a b
+append d a b = insert d (S.getDim d (shape a)) a b
 
 -- | Insert along a dimension at the beginning.
 --
@@ -864,7 +864,7 @@ slice ::
   (Int, Int) ->
   Array a ->
   Array a
-slice d (o, l) a = backpermute (S.replaceDim d l) (S.modifyDim d (+ o)) a
+slice d (o, l) a = backpermute (S.setDim d l) (S.modifyDim d (+ o)) a
 
 
 -- * multi-dimension operators
@@ -883,8 +883,8 @@ takes ::
   Array a
 takes ts a = backpermute dsNew (List.zipWith (+) start) a
   where
-    dsNew = S.replaceDims ds xsAbs
-    start = List.zipWith (\x s -> bool 0 (s + x) (x<0)) (S.replaceDimsT ts (replicate (rank a) 0)) (shape a)
+    dsNew = S.setDims ds xsAbs
+    start = List.zipWith (\x s -> bool 0 (s + x) (x<0)) (S.setDimsT ts (replicate (rank a) 0)) (shape a)
     ds = fmap fst ts
     xs = fmap snd ts
     xsAbs = fmap abs xs
@@ -900,7 +900,7 @@ drops ::
 drops ts a = backpermute dsNew (List.zipWith (\d' s' -> bool (d' + s') s' (d' < 0)) xsNew) a
   where
     dsNew = S.modifyDims ds (fmap (flip (-)) xsAbs)
-    xsNew = S.replaceDims ds xs (replicate (rank a) 0)
+    xsNew = S.setDims ds xs (replicate (rank a) 0)
     ds = fmap fst ts
     xs = fmap snd ts
     xsAbs = fmap abs xs
@@ -1620,7 +1620,7 @@ concats ::
 concats ds n a = backpermute concatDims unconcatDims a
   where
     concatDims s = S.insertDim n (S.size $ S.takeDims ds s) (S.deleteDims ds s)
-    unconcatDims s = S.insertDims (List.zip ds (S.shapen (S.takeDims ds (shape a)) (S.unsafeGetIndex n s))) (S.deleteDim n s)
+    unconcatDims s = S.insertDims (List.zip ds (S.shapen (S.takeDims ds (shape a)) (S.getDim n s))) (S.deleteDim n s)
 
 -- | Rotate an array along a dimension.
 --