- Riff on https://www.reddit.com/r/haskell/comments/8qn0wr/safe_api_design_with_ghosts_of_departed_proofs/
- reddit thread: https://www.reddit.com/r/haskell/comments/dlzc46/ghosts_via_departed_proofs_experimenting/
Ghosts of Departed Proofs introduces sortBy
. It sorts using a comparison function a -> a -> Ordering
named "comp
". The name is then recorded in the return type: "this list is sorted by comp
"!
type Cmp :: Type -> Type
type Cmp a = (a -> a -> Ordering)
sortBy :: Cmp a~~comp -> [a] -> SortedBy comp [a]
This becomes important with mergeBy
where we have two sorted lists that we want to combine (to a sorted list). We can merge sorted lists sortBy up as
, sortBy down bs
quickly if up
and down
are the same.
mergeBy :: Cmp a~~comp -> SortedBy comp [a] -> SortedBy comp [a] -> SortedBy comp [a]
In Ghosts of Departed Proofs, we give names to the compare
("up
") & flip compare
("down
"). sortBy up
and sortBy down
now have different types and cannot be merged:
-- This FAILS
name (compare) \up ->
name (flip compare) \down ->
.. mergeBy up (sortBy up [1,2]) (sortBy down [3,4]) ..
-- wouldn't it be horrible if (`compare`) meant (flip compare)
Read the paper, it's good.
Now keep in mind we already have a way to refer to a comparison function Cmp a
. If you have a type a
with an Ord a
instance then you have such a function compare @a :: Cmp a
. For example there is a newtype, Data.Ord.Down
newtype Down a = Down a
-- -XInstancesVia (wip)
instance Ord a => Ord (Down a via a) where
compare :: Cmp a
compare = flip compare
flipCompare :: Cmp a
flipCompare = compare @(via Down) -- -XApplyingVia
The idea is, can we define
sortVia :: .. => [a] -> SortedVia vía a
which records its vía
type (i.e. the type a
gets coerced to via a
for an Ord
instance) in the type just as we did before, only this time we don't need to bring the named comparator into scope and pass it explicitly. We don't export the SortedVia
data constructor.
type role
SortedVia nominal nominal
newtype SortedVia :: (Type -> Type) -> (Type -> Type)
where SortedVia :: [a] -> SortedVia vía a
deriving
stock Show
Since we are sorting via vía a
we need that to have an ordering Ord (vía a)
.
sort @(vía a) :: Ord (vía a) => [vía a] -> [vía a]
We coerce
between vía a
and a
and requrire them to be Coercible
type (~𝈖) = Coercible
coerce :: (vía a ~𝈖 a) => ([vía a] -> [vía a]) -> ([a] -> [a])
type a `SortingVia` vía = (Ord (vía a), vía a ~𝈖 a)
sortVia :: forall vía a. a `SortingVia` vía => [a] -> SortedVia vía a
sortVia as = SortedVia (sort @(vía a) `coerce` as)
-- -XApplyingVia (wip)
-- sortVia = SortedVia . sort @(a via vía a)
Now we have
-- >> type Up = Identity
-- >> ehllo
-- SortedVia "ehllo"
ehllo :: SortedVia Up Char
ehllo = sortVia "hello"
-- >> ollhe
-- SortedVia "ollhe"
ollhe :: SortedVia Down Char
ollhe = sortVia "hello"
we don't need explicitly name up :: Cmp a~~up
and down :: Cmp a~~down
or pass them in. It is determined by the type.
We can also define a
instance a `SortingVia` vía => Semigroup (SortedVia vía a) where
-- (<>) = (¦) @(SortedVia vía a via vía a)
(<>) :: SortedVia vía a -> SortedVia vía a -> SortedVia vía a
(<>) = coerce ((¦) @(vía a)) where
(¦) :: Ord b => [b] -> [b] -> [b]
[] ¦ bs = bs
as ¦ [] = as
(a:as) ¦ (b:bs) = if a <= b then a:(as¦(b:bs)) else b:((a:as)¦bs)
instance a `SortingVia` vía => Monoid (SortedVia vía a) where
mempty :: SortedVia vía a
mempty = sortVia []
>> sortVia @Up "ABC" <> sortVia @Up "XYZ"
SortedVia "ABCXYZ"
>>
>> sortVia @Down "ABC" <> sortVia @Down "XYZ"
SortedVia "ZYXCBA"
Just a thought!