|
|
|
|
|
|
by Iceland_jack
148 days ago
|
|
|
This is to say that (length-indexed) "Arrays" are Representable functors[1]. A `Vec n a` is isomorphic to (Fin n -> a), where Fin n = { x :: Nat | x < n }. instance pi n. Representable (Vec n) where
type Rep (Vec n) = Fin n
index :: Vec n a -> (Fin n -> a)
index = ..
tabulate :: (Fin n -> a) -> Vec n a
tabulate = ..
[1] https://hackage-content.haskell.org/package/adjunctions-4.4.... |
|
|