[ fix #870 ] Finish deprecating Data.Table #1078
Conversation
There was a problem hiding this comment.
Sorry, I thought I'd submitted this review ages ago. Obviously I hadn't!
Basically a few comments about design decisions that I made when adding this that I'd kind of like to take this opportunity to reverse. I'm happy to implement my suggestions if you'd like @gallais ?
| sumₜ : ∀ {n} → Table Carrier n → Carrier | ||
| sumₜ = Table.foldr _+_ 0# | ||
| sumₜ : ∀ {n} → Vector Carrier n → Carrier | ||
| sumₜ = Vector.foldr _+_ 0# |
There was a problem hiding this comment.
The name sumₜ probably needs to be changed as the ₜ refers to Table?
| -- Changes the order of elements in the table according to a permutation (i.e. | ||
| -- an 'Inverse' object on the indices). | ||
|
|
||
| permute : ∀ {m n a} {A : Set a} → Fin m ↔ Fin n → Vector A n → Vector A m |
There was a problem hiding this comment.
I'd quite like to take this opportunity to correct some sub-optimal design decisions that I think we (well mostly I!) made here.
For starters, the permute function should just take a Fin m → Fin n function rather than the full inverse proof right? This makes it more generally applicable, and we can then prove properties about it depending on what properties the function satisfies? (also we should try and avoid using the old function hierarchy)
| -- The result of 'select z i t' takes the value of 'lookup t i' at index 'i', | ||
| -- and 'z' everywhere else. | ||
|
|
||
| select : ∀ {n} {a} {A : Set a} → A → Fin n → Vector A n → Vector A n |
There was a problem hiding this comment.
We should try to be consistent with the terminology in List and Vec by using the standard _[_]≔_ syntax
|
|
||
| module _ (S@record { Carrier = A } : Setoid c ℓ) where | ||
|
|
||
| ↔Vec : ∀ {n} → Inverse (Pw.setoid S n) (VecPw.setoid S n) |
There was a problem hiding this comment.
Again we should use the new function hierarchy here?
| -- There exists an isomorphism between vectors as functions on the one | ||
| -- and and vectors as datatypes on the other. | ||
|
|
||
| module _ (S@record { Carrier = A } : Setoid c ℓ) where |
There was a problem hiding this comment.
Ooooh that's fancy syntax. Is that new in 2.6.1?
|
Going to try and have a look at this this morning. |
|
Superseded by #1100 |
MatthewDaggitt
added
status: duplicate
No description provided.