discussed.
import Data.List
newtype Count = Count Int deriving(Eq, Show, Ord, Num)
newtype Ix = Ix Int deriving(Eq, Show, Ord, Num)
eqscan :: Eq a => a -> [a] -> [Count]
eqscan a0 as = map Count $ scanl (+) 0 [if a0 == a then 1 else 0 | a <- as]
select :: Eq a => a -> [a] -> Count -> Maybe Ix
select a0 as c = Ix <$> findIndex (== c) (eqscan a0 as)
rank :: Eq a => a -> [a] -> Ix -> Count
rank a as (Ix ix) = (eqscan a as) !! ix
Given this, we can prove that select
and rank
are adjunctions. There
are different ways to think about this. My favourite way to is to notice
that an Ix
(index) is much "finer" information than Count
. Hence,
the concrete domain must be Ix
, the abstract domain must be Count
,
and rank-select is an abstract interpretation!
§ Co-select
We can build another version of select
called co-select
that scans
from the right. Alternatively, it finds on the reverse list:
coselect :: Eq a => a -> [a] -> Count -> Maybe Ix
coselect a0 as c = Ix <$> findIndex (== c) (reverse (eqscan a0 as))
Thanks to Edward Kmett for teaching me this.