I've run into this in a handful of cases where I've got a contravariant applicative and I want to "map it over" a list (more accurately an indexable container like a vector). This mapping ends up depending on the length of the list, as the logic goes like so:
- I've got an
f a
- I've got an indexable container
v a with size :: v a -> Int and a partial ref :: v a -> Int -> a function
- I can use
contramap to take an index and convert f a to f (v a), where it only operates on the element at the index and ignores the others
- I can combine multiple instances of
f a in a way that's just repeatedly applying divide with conquer as the empty case
- Given this, I can go from a list of indexes to a combined
f (v a) that operates on the elements at those indexes
- Now I need to construct an
f (v a) that gets the size of the input container, uses that size to construct a list of all indexes in v a, constructs a combined f (v a) operating on the elements at those indexes, then applies that combined f (v a) to the input container
- In order to do that, I need some sort of "dependent" constructor for an
f that lets me turn any a -> f a function into an f a
I'm not sure if this something that Decidable can do or if the only reason using Decidable seems unintuitive to me is because of the partial nature of the ref function. For context, I mostly work with impure functional languages so a constant-time partial ref function is more idiomatic than it would be in Haskell.
I've run into this in a handful of cases where I've got a contravariant applicative and I want to "map it over" a list (more accurately an indexable container like a vector). This mapping ends up depending on the length of the list, as the logic goes like so:
f av awithsize :: v a -> Intand a partialref :: v a -> Int -> afunctioncontramapto take an index and convertf atof (v a), where it only operates on the element at the index and ignores the othersf ain a way that's just repeatedly applyingdividewithconqueras the empty casef (v a)that operates on the elements at those indexesf (v a)that gets the size of the input container, uses that size to construct a list of all indexes inv a, constructs a combinedf (v a)operating on the elements at those indexes, then applies that combinedf (v a)to the input containerfthat lets me turn anya -> f afunction into anf aI'm not sure if this something that
Decidablecan do or if the only reason usingDecidableseems unintuitive to me is because of the partial nature of thereffunction. For context, I mostly work with impure functional languages so a constant-time partialreffunction is more idiomatic than it would be in Haskell.