SelectiveSigma.hs

{-# LANGUAGE GADTs, RankNTypes, TypeFamilies, DataKinds, PolyKinds, TypeOperators, ScopedTypeVariables #-}

-- Lots of ways you can phrase this, but this works for me
-- For folks who haven't seen it before, this is "the essence of the sum type" and sigma stands for sum.
-- You see it far more often in dependent types than elsewhere because it becomes a lot more pleasant to
-- work with there, but it's doable in other contexts too. Think of the first parameter to the data
-- constructor as a generalized "tag" as we talk about in "tagged union", and the second parameter is the
-- "payload". It turns out that you can represent any simple sum type you could write in Haskell this way
-- by using a finite and enumerable `f`, but things can get more unusual when `f` isn't either. In such
-- cases, it's often easier to think of this as the essence of existential types.
data Sigma f where
  Sigma :: f a -> a -> Sigma f

-- How to get Either out of here
data Eitherish a b c where
  A :: Eitherish a b a
  B :: Eitherish a b b

left :: a -> Sigma (Eitherish a b)
left = Sigma A

right :: b -> Sigma (Eitherish a b)
right = Sigma B

fromEither :: Either a b -> Sigma (Eitherish a b)
fromEither = either left right

{-
class Applicative f => Selective f where
  handle :: f (Either a b) -> f (a -> b) -> f b
-}

-- Squint really hard and it's similar to the above, except with
-- n-ary (possibly infinite, depending on h) branching
-- Might be more obvious if you compare to the selection function
-- from https://blogs.ncl.ac.uk/andreymokhov/selective/:
--   select :: Selective f => f (Either a b) -> f (a -> c) -> f (b -> c) -> f c
class Applicative f => SigmaSelective f where
  sigmaSelect :: f (Sigma h) -> (forall a. h a -> f (a -> c)) -> f c

-- We can get Andrey's `select` from `sigmaSelect`
select :: forall f a b c. SigmaSelective f => f (Either a b) -> f (a -> c) -> f (b -> c) -> f c
select choice l r = sigmaSelect (fmap fromEither choice) choose
  where
  -- GADT matching so I need to provide the type sig or GHC gets confused
  choose :: forall x. Eitherish a b x -> f (x -> c)
  choose A = l
  choose B = r

data WeirdSelector a b where
  WeirdSelector :: a -> WeirdSelector a ()
  
-- 😱
bind :: forall f a b. SigmaSelective f => f a -> (a -> f b) -> f b
bind x f = sigmaSelect (fmap (\x -> Sigma (WeirdSelector x) ()) x) getItOut
  where
  getItOut :: forall u. WeirdSelector a u -> f (u -> b)
  getItOut (WeirdSelector x) = fmap const (f x)


-- Back to Andrey's woes with lots of nested Eithers...
data NAry :: [a] -> a -> * where
  Here  :: NAry (x ': xs) x
  There :: NAry xs x -> NAry (y ': xs) x

twoAry :: Either a b -> Sigma (NAry '[a, b])
twoAry (Left a) = Sigma Here a
twoAry (Right b) = Sigma (There Here) b

threeAry :: Either a (Either b c) -> Sigma (NAry '[a, b, c])
threeAry (Left a) = Sigma Here a
threeAry (Right (Left b)) = Sigma (There Here) b
threeAry (Right (Right c)) = Sigma (There (There Here)) c

-- I haven't actually played with this to see if it falls apart later, but have had some version
-- of this floating around in my head for ages. I also haven't written fancy Haskell in ages so
-- I might be behind the times a bit on conventions :)