Ghosts Via Departed Proofs

GhostsViaDepartedProofs.md

• 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!