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 :)