Improve make/Make implementation for Data.V.Linear
#364
Conversation
|
I set the base of this PR to tbagrel1/dupable-new-impl, so as to reduce clutter in the diff pane, but the idea is to merge this one only after that tbagrel1/dupable-new-impl has been merged into |
|
I know what this PR is about. Today. But please don't make a PR without a description. I'm not the only one who is to read these. And even if this was just for you and me, we may want to revisit the PR in the future to remember why we did X and Y, without an apt description, it becomes impossible. |
src/Data/V/Linear/Internal.hs
Outdated
| -- The idea behind 'Make' \/ @make\'@ \/ 'make' is the following: | ||
| -- | ||
| -- @f@ takes @m@ values of type @a@, but returns a @'V' n a@ (with @n@ ≥ @m@), | ||
| -- so the @n - m@ missing values must be supplied via the accumulator. | ||
| -- | ||
| -- @make\'@ is initially called with @m = n@ via 'make', and as @m@ decreases, | ||
| -- the number of lambda on the left increases and the captured values are put | ||
| -- in the accumulator | ||
| -- (@V[ ... ] \<\>@ represents the "extend" operation for 'V'): | ||
| -- | ||
| -- > make @n | ||
| -- > --> make' @n @n (V[] <>) | ||
| -- > --> λx. make' @(n - 1) @n (V[x] <>) | ||
| -- > --> λx. λy. make' @(n - 2) @n (V[x, y] <>) | ||
| -- > --> ... | ||
| -- > --> λx. λy. ... λz. make' @0 @n (V[x, y, ... z] <>) -- make' @0 @n f = f V[] | ||
| -- > --> λx. λy. ... λz. V[x, y, ... z] |
There was a problem hiding this comment.
I think that this documentation should be on the make function, not the Make class.
Plus it speaks of make', which isn't exported. Let's avoid this. If you need to document the implementation, do so outside of the docstring, in regular comments.
Remember to give instantiations of the type of make with concrete values. Examples are very helpful to disentangle very general types.
tbagrel1
force-pushed
the
tbagrel1/v-make-improvement
branch
from
0b07dc7 to
6e26c50
Compare
V n arepresents vector havingnelements of typea. Such a vector can be built using themakefunction, takingnlinear arguments of typea, and returning aV n a.At the moment,
makeuses a lot of type-level machinery aroundNats, and is implemented in a way such that it cannot be inlined; even ifnis compile-time known.With #360 (now merged), the
Data.V.Linearmodule has been overhauled, and theelimfunction has been rewritten to be inlinable.The aim of this PR is to provide an efficient
makeimplementation using typeclasses so as to make it inlinable whennis known at compile-time. It also adds more symmetry betweenmakeandelim, and allows us to get rid of a lot of internal helper functions.