bodil / bodil/purescript-sized-vectors

Type-safe indexed maps

Open
#33 1 comment 0 reactions 0 assignees View on GitHub
Dominant language
PureScript
Stars
18
Forks
12
PR merge metrics
No merged PRs in 30d

Description

Hi!

In one of my projects, I found myself writing this:

```purescript
import Data.Typelevel.Num (class Lt, class Nat, class Pos, class Pred, class Sub, class Succ, D0, D1, D2, D3, D4, D5, D6, D7, D8, D9, NumCons(..), d0, d1, d2, d3, d4, d5, d6, d7, d8, d9)
import Data.Vec as V
import Type.Proxy (Proxy(..))

class ProxyToNat n where
proxyToNat :: Proxy n -> n

instance proxyToNatD0 :: ProxyToNat D0 where
proxyToNat _ = d0
instance proxyToNatD1 :: ProxyToNat D1 where
proxyToNat _ = d1
instance proxyToNatD2 :: ProxyToNat D2 where
proxyToNat _ = d2
instance proxyToNatD3 :: ProxyToNat D3 where
proxyToNat _ = d3
instance proxyToNatD4 :: ProxyToNat D4 where
proxyToNat _ = d4
instance proxyToNatD5 :: ProxyToNat D5 where
proxyToNat _ = d5
instance proxyToNatD6 :: ProxyToNat D6 where
proxyToNat _ = d6
instance proxyToNatD7 :: ProxyToNat D7 where
proxyToNat _ = d7
instance proxyToNatD8 :: ProxyToNat D8 where
proxyToNat _ = d8
instance proxyToNatD9 :: ProxyToNat D9 where
proxyToNat _ = d9
instance proxyToNatCons :: (ProxyToNat a, ProxyToNat b) => ProxyToNat (NumCons a b) where
proxyToNat _ = NumCons (proxyToNat (Proxy :: _ a)) (proxyToNat (Proxy :: _ b))

class
(Nat total, Nat n, ProxyToNat total, ProxyToNat n) <= VectorMap' total n where
mapWithTypedIndex' :: forall a b. Proxy total -> (forall i. Nat i => ProxyToNat i => Lt i total => Proxy i -> a -> b) -> V.Vec n a -> V.Vec n b

class
(Nat n, ProxyToNat n) <= VectorMap n where
mapWithTypedIndex :: forall a b. (forall i. Nat i => ProxyToNat i => Lt i n => Proxy i -> a -> b) -> V.Vec n a -> V.Vec n b

instance vectorMap :: VectorMap' n n => VectorMap n where
mapWithTypedIndex = mapWithTypedIndex' (Proxy :: _ n)

instance vectorMapD0 :: (Nat n, ProxyToNat n) => VectorMap' n D0 where
mapWithTypedIndex' _ _ _ = V.empty
else instance vectorMapN ::
( Nat x
, ProxyToNat x
, ProxyToNat n
, Lt x total
, Pos total
, Pred n n'
, Succ n' n
, VectorMap' total n'
, Sub total n x
) =>
VectorMap' total n where
mapWithTypedIndex' t f a =
V.cons (f (Proxy :: _ x) (V.head a))
(mapWithTypedIndex' t f (V.tail a))
```

If you do ie:

```purescript
test0 = V.fill identity :: V.Vec D10 Int
test1 = mapWithTypedIndex (\px _ -> V.modifyAt (proxyToNat px) (const 42) test0) test0 :: V.Vec D10 (V.Vec D10 Int)
```

You get for `test1`:

```purescript
((42 +> 1 +> 2 +> 3 +> 4 +> 5 +> 6 +> 7 +> 8 +> 9 +> empty) +> (0 +> 42 +> 2 +> 3 +> 4 +> 5 +> 6 +> 7 +> 8 +> 9 +> empty) +> (0 +> 1 +> 42 +> 3 +> 4 +> 5 +> 6 +> 7 +> 8 +> 9 +> empty) +> (0 +> 1 +> 2 +> 42 +> 4 +> 5 +> 6 +> 7 +> 8 +> 9 +> empty) +> (0 +> 1 +> 2 +> 3 +> 42 +> 5 +> 6 +> 7 +> 8 +> 9 +> empty) +> (0 +> 1 +> 2 +> 3 +> 4 +> 42 +> 6 +> 7 +> 8 +> 9 +> empty) +> (0 +> 1 +> 2 +> 3 +> 4 +> 5 +> 42 +> 7 +> 8 +> 9 +> empty) +> (0 +> 1 +> 2 +> 3 +> 4 +> 5 +> 6 +> 42 +> 8 +> 9 +> empty) +> (0 +> 1 +> 2 +> 3 +> 4 +> 5 +> 6 +> 7 +> 42 +> 9 +> empty) +> (0 +> 1 +> 2 +> 3 +> 4 +> 5 +> 6 +> 7 +> 8 +> 42 +> empty) +> empty)
```

Does that sort of thing seem interesting for this library? If so, I'll make a PR!

Contributor guide

No contributing guide indexed for this repository

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.