Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
{-# 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 :)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.