Vta2

CHANGELOG.md

@@ -1,5 +1,10 @@
 # Changelog
 
+## Unreleased
+
+**Breaking changes**
+- Update to use VTAs
+
 ## [v0.7.0]
 - Add read & write optimised sparse vectors (#10 by @mikesol)
 

README.md

@@ -2,6 +2,10 @@
 
 Fast, type-safe vector libary for Purescript inspired by [Idris](https://www.idris-lang.org/). A vector is list with its size encoded in the type.
 
+https://user-images.githubusercontent.com/77549848/179352478-36ddb5ee-dc51-4d53-ad5c-19b244cd2f7b.mp4
+
+
+
 ## Installation
 
 ```bash
@@ -41,7 +45,7 @@ You will get an `elem` back, no need to handle a `Maybe`. And this operation is
 
 Similarly, the `index` function has the following type signature (conceptually - the real one is slightly more complex):
 ```purescript
-index :: forall i m elem. Term i -> Vect m elem -> elem
+index :: forall @i m elem. Vect m elem -> elem
 ```
 If the index `i` (represented as a typelevel symbol) is in bounds, i.e. `i < m`, you will get an `elem` back, otherwise you will get a compile-time error. 
 
@@ -59,35 +63,35 @@ import Prelude
 
 import Data.FastVect.FastVect (Vect)
 import Data.FastVect.FastVect as FV
-import Typelevel.Arithmetic.Add (Term, term)
 
 as :: Vect 300 String
-as = FV.replicate (term :: Term 300) "a"
--- Note you could also leave out the Term type annotation, as PS can infer it:
--- as = FV.replicate (term :: _ 300) "a"
+as = FV.replicate @300 "a"
+-- Note: you can leave out the type annotation, as PS can infer it:
+-- as = FV.replicate @300 "a"
 
 bs :: Vect 200 String
-bs = FV.replicate (term :: Term 200) "b"
+bs = FV.replicate @200 "b"
 
 cs :: Vect 500 String
 cs = FV.append as bs
 
 ds :: Vect 2 String
-ds = cs # FV.drop (term :: Term 299) # FV.take (term :: Term 2)
+ds = cs # FV.drop @299 # FV.take @2
 
 x :: String
-x = FV.index (term :: Term 499) cs
+x = FV.index @499 cs
 
 y :: String
 y = FV.head (FV.singleton "a")
 
 big1 :: Vect 23923498230498230420 String
-big1 = FV.replicate (term :: Term 23923498230498230420) "a"
+big1 = FV.replicate @23923498230498230420 "a"
 
 big2 :: Vect 203948023984590684596840586 String
-big2 = FV.replicate (term :: Term 203948023984590684596840586) "b"
+big2 = FV.replicate @203948023984590684596840586 "b"
 
 big :: Vect 203948047908088915095071006 String
 big = FV.append big1 big2
--- Note the big example will blow up during runtime.
+-- Note: the big example will blow up during runtime. Need to increase Node.js memory for this ;)
 ```
+

src/Data/FastVect/Common.purs

@@ -41,8 +41,8 @@ class TraversableWithIndex Int f <= IsVect f
 term ∷ forall (i ∷ Int). Proxy i
 term = Proxy
 
-toInt ∷ forall (len ∷ Int). Reflectable len Int ⇒ Proxy len → Int
-toInt = reflectType
+toInt ∷ forall (@len ∷ Int). Reflectable len Int ⇒ Int
+toInt = reflectType (Proxy :: _ len)
 
 -- -- | Create a `Vect` by replicating `len` times the given element
 -- -- |
@@ -53,8 +53,7 @@ toInt = reflectType
 type Replicate vect len elem =
   Compare len NegOne GT
   ⇒ Reflectable len Int
-  ⇒ Proxy len
-  → elem
+  ⇒ elem
   → vect len elem
 
 -- -- | Creates the empty `Vect`.
@@ -121,8 +120,7 @@ type Drop vect m n m_plus_n elem =
   ⇒ Reflectable m Int
   ⇒ Compare m NegOne GT
   ⇒ Compare n NegOne GT
-  ⇒ Proxy m
-  → vect m_plus_n elem
+  ⇒ vect m_plus_n elem
   → vect n elem
 
 -- -- | Safely take `m` elements from a `Vect`.
@@ -141,8 +139,7 @@ type Take vect m n m_plus_n elem =
   ⇒ Reflectable m Int
   ⇒ Compare m NegOne GT
   ⇒ Compare n NegOne GT
-  ⇒ Proxy m
-  → vect m_plus_n elem
+  ⇒ vect m_plus_n elem
   → vect m elem
 
 -- -- | Safely modify element `m` from a `Vect`.
@@ -159,8 +156,7 @@ type Modify vect m n elem =
   ⇒ Compare m NegOne GT
   ⇒ Compare n NegOne GT
   ⇒ Compare m n LT
-  ⇒ Proxy m
-  → (elem → elem)
+  ⇒ (elem → elem)
   → vect n elem
   → vect n elem
 
@@ -178,8 +174,7 @@ type Set vect m n elem =
   ⇒ Compare m NegOne GT
   ⇒ Compare n NegOne GT
   ⇒ Compare m n LT
-  ⇒ Proxy m
-  → elem
+  ⇒ elem
   → vect n elem
   → vect n elem
 
@@ -201,8 +196,7 @@ type SplitAt vect m n m_plus_n elem =
   ⇒ Reflectable m Int
   ⇒ Compare m NegOne GT
   ⇒ Compare n NegOne GT
-  ⇒ Proxy m
-  → vect m_plus_n elem
+  ⇒ vect m_plus_n elem
   → { before ∷ vect m elem, after ∷ vect n elem }
 
 -- -- | Safely access the `n`-th modulo m element of a `Vect`.
@@ -243,8 +237,7 @@ type Index vect m m_minus_one i n elem =
   ⇒ Add i n m_minus_one
   ⇒ Compare i NegOne GT
   ⇒ Reflectable i Int
-  ⇒ Proxy i
-  → vect m elem
+  ⇒ vect m elem
   → elem
 
 type IndexM vect m m_minus_one i n elem =
@@ -254,8 +247,7 @@ type IndexM vect m m_minus_one i n elem =
   ⇒ Add i n m_minus_one
   ⇒ Compare i NegOne GT
   ⇒ Reflectable i Int
-  ⇒ Proxy i
-  → vect m elem
+  ⇒ vect m elem
   → Maybe elem
 -- -- | Safely access the head of a `Vect`.
 -- -- |

src/Data/FastVect/FastVect.purs

@@ -49,7 +49,7 @@ newtype Vect ∷ Int → Type → Type
 newtype Vect len elem = Vect (Array elem)
 
 instance (Show elem, Reflectable len Int) ⇒ Show (Vect len elem) where
-  show (Vect elems) = "Vect " <> show (Common.toInt (Common.term ∷ _ len)) <> " " <> show elems
+  show (Vect elems) = "Vect " <> show (Common.toInt @len) <> " " <> show elems
 
 derive newtype instance Eq elem ⇒ Eq (Vect len elem)
 derive newtype instance Ord elem ⇒ Ord (Vect len elem)
@@ -58,7 +58,7 @@ instance Apply (Vect len) where
   apply (Vect fab) (Vect a) = Vect (Array.zipWith ($) fab a)
 
 instance (Compare len Common.NegOne GT, Reflectable len Int) ⇒ Applicative (Vect len) where
-  pure = replicate (Proxy :: _ len)
+  pure = replicate @len
 
 derive newtype instance FunctorWithIndex Int (Vect len)
 derive newtype instance Foldable (Vect len)
@@ -72,8 +72,8 @@ derive newtype instance TraversableWithIndex Int (Vect len)
 -- -- | vect ∷ Vect 300 String
 -- -- | vect = replicate (Common.term ∷ _ 300) "a"
 -- -- | ```
-replicate ∷ ∀ len elem. Common.Replicate Vect len elem
-replicate proxy elem = Vect $ A.replicate (Common.toInt proxy) elem
+replicate ∷ ∀ @len elem. Common.Replicate Vect len elem
+replicate elem = Vect $ A.replicate (Common.toInt @len) elem
 
 -- -- | Creates the empty `Vect`.
 -- -- |
@@ -118,8 +118,8 @@ append (Vect xs) (Vect ys) = Vect (xs <> ys)
 -- -- | newVect ∷ Vect 200 String
 -- -- | newVect = drop (Common.term ∷ _ 100) vect
 -- -- | ```
-drop ∷ ∀ m n m_plus_n elem. Common.Drop Vect m n m_plus_n elem
-drop proxy (Vect xs) = Vect (A.drop (Common.toInt proxy) xs)
+drop ∷ ∀ @m n m_plus_n elem. Common.Drop Vect m n m_plus_n elem
+drop (Vect xs) = Vect (A.drop (Common.toInt @m) xs)
 
 -- -- | Safely take `m` elements from a `Vect`.
 -- -- | Will result in a compile-time error if you are trying to take more elements than exist in the vector.
@@ -131,8 +131,8 @@ drop proxy (Vect xs) = Vect (A.drop (Common.toInt proxy) xs)
 -- -- | newVect ∷ Vect 100 String
 -- -- | newVect = take (Common.term ∷ _ 100) vect
 -- -- | ```
-take ∷ ∀ m n m_plus_n elem. Common.Take Vect m n m_plus_n elem
-take proxy (Vect xs) = Vect (A.take (Common.toInt proxy) xs)
+take ∷ ∀ @m n m_plus_n elem. Common.Take Vect m n m_plus_n elem
+take (Vect xs) = Vect (A.take (Common.toInt @m) xs)
 
 foreign import modifyImpl :: forall n elem. Int → (elem → elem) → Vect n elem → Vect n elem
 
@@ -145,8 +145,8 @@ foreign import modifyImpl :: forall n elem. Int → (elem → elem) → Vect n e
 -- -- | newVect ∷ Vect 100 String
 -- -- | newVect = modify (Common.term ∷ _ 100) (append "b") vect
 -- -- | ```
-modify ∷ ∀ m n elem. Common.Modify Vect m n elem
-modify proxy = modifyImpl (Common.toInt proxy)
+modify ∷ ∀ @m n elem. Common.Modify Vect m n elem
+modify = modifyImpl (Common.toInt @m)
 
 -- -- | Safely set element `m` from a `Vect`.
 -- -- |
@@ -158,7 +158,7 @@ modify proxy = modifyImpl (Common.toInt proxy)
 -- -- | newVect = modify (Common.term ∷ _ 100) "b" vect
 -- -- | `
 set ∷ ∀ m n elem. Common.Set Vect m n elem
-set proxy = modify proxy <<< const
+set = modify @m <<< const
 
 -- -- | Split the `Vect` into two sub vectors `before` and `after`, where before contains up to `m` elements.
 -- -- |
@@ -172,10 +172,10 @@ set proxy = modify proxy <<< const
 -- -- |   }
 -- -- | split = splitAt (Common.term ∷ _ 3) vect
 -- -- | ```
-splitAt ∷ ∀ m n m_plus_n elem. Common.SplitAt Vect m n m_plus_n elem
-splitAt proxy (Vect xs) = { before: Vect before, after: Vect after }
+splitAt ∷ ∀ @m n m_plus_n elem. Common.SplitAt Vect m n m_plus_n elem
+splitAt (Vect xs) = { before: Vect before, after: Vect after }
   where
-  { before, after } = A.splitAt (Common.toInt proxy) xs
+  { before, after } = A.splitAt (Common.toInt @m) xs
 
 -- -- | Safely access the `n`-th modulo m element of a `Vect`.
 -- -- |
@@ -187,7 +187,7 @@ splitAt proxy (Vect xs) = { before: Vect before, after: Vect after }
 -- -- | elem = indexModulo 5352523 vect
 -- -- | ```
 indexModulo ∷ ∀ m elem. Common.IndexModulo Vect m elem
-indexModulo i = indexImpl (i `mod` Common.toInt (Proxy ∷ _ m))
+indexModulo i = indexImpl (i `mod` Common.toInt @m)
 
 foreign import indexImpl :: forall m elem. Int → Vect m elem → elem
 
@@ -200,8 +200,8 @@ foreign import indexImpl :: forall m elem. Int → Vect m elem → elem
 -- -- | elem ∷ String
 -- -- | elem = index (Common.term ∷ _ 299) vect
 -- -- | ```
-index ∷ ∀ m m_minus_one i n elem. Common.Index Vect m m_minus_one i n elem
-index = indexImpl <<< Common.toInt
+index ∷ ∀ m m_minus_one @i n elem. Common.Index Vect m m_minus_one i n elem
+index = indexImpl (Common.toInt @i)
 
 -- -- | Safely access the head of a `Vect`.
 -- -- |
@@ -223,14 +223,13 @@ head = indexImpl 0
 -- -- | fromArray (Common.term ∷ _ 4) ["a", "b", "c"] = Nothing
 -- -- | ```
 fromArray
-  ∷ ∀ len elem
+  ∷ ∀ @len elem
   . Reflectable len Int
   ⇒ Compare len Common.NegOne GT
-  ⇒ Proxy len
-  → Array elem
+  ⇒ Array elem
   → Maybe (Vect len elem)
-fromArray proxy array | Array.length array == Common.toInt proxy = Just (Vect array)
-fromArray _ _ = Nothing
+fromArray array | Array.length array == Common.toInt @len = Just (Vect array)
+fromArray _ = Nothing
 
 -- -- | Converts the `Vect` to an `Array`, effectively dropping the size information.
 toArray
@@ -248,28 +247,26 @@ toArray (Vect arr) = arr
 -- -- | toArray $ adjust (Common.term ∷ _ 3) 0 [ 0, 0, 0, 0, 1, 2, 3 ] == [ 1, 2, 3 ]
 -- -- | ```
 adjust
-  ∷ ∀ len elem
+  ∷ ∀ @len elem
   . Reflectable len Int
   ⇒ Compare len Common.NegOne GT
-  ⇒ Proxy len
-  → elem
+  ⇒ elem
   → Array elem
   → Vect len elem
-adjust proxy elem array = case Array.length array - Common.toInt proxy of
+adjust elem array = case Array.length array - Common.toInt @len of
   0 → Vect array
   len | len < 0 → Vect $ A.replicate (abs len) elem <> array
   len → Vect $ A.drop len array
 
 -- -- | Like `adjust` but uses the Moinoid instance of elem to create the elements.
 adjustM
-  ∷ ∀ len elem
+  ∷ ∀ @len elem
   . Monoid elem
   ⇒ Reflectable len Int
   ⇒ Compare len Common.NegOne GT
-  ⇒ Proxy len
-  → Array elem
+  ⇒ Array elem
   → Vect len elem
-adjustM proxy = adjust proxy mempty
+adjustM = adjust @len mempty
 
 -- -- | Attaches an element to the front of the `Vect`, creating a new `Vect` with size incremented.
 -- -- |