{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE UndecidableInstances #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Extensible.Sum
-- Copyright   :  (c) Fumiaki Kinoshita 2018
-- License     :  BSD3
--
-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
--
------------------------------------------------------------------------
module Data.Extensible.Sum (
  (:/)(..)
  , hoist
  , embed
  , strike
  , strikeAt
  , (<:|)
  , exhaust
  , embedAssoc
  ) where

import Data.Extensible.Class
import Data.Kind (Type)
import Data.Profunctor
import Data.Proxy
import Data.Type.Equality
import Type.Membership

-- | The extensible sum type
--
-- @(:/) :: [k] -> (k -> Type) -> Type@
--
data (xs :: [k]) :/ (h :: k -> Type) where
  EmbedAt :: !(Membership xs x) -> h x -> xs :/ h

instance Enum (xs :/ Proxy) where
  fromEnum :: (xs :/ Proxy) -> Int
fromEnum (EmbedAt Membership xs x
m Proxy x
_) = Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ Membership xs x -> Int
forall k (xs :: [k]) (x :: k). Membership xs x -> Int
getMemberId Membership xs x
m
  toEnum :: Int -> xs :/ Proxy
toEnum Int
i = Int
-> (forall {x :: k}. Membership xs x -> xs :/ Proxy) -> xs :/ Proxy
forall {k} (xs :: [k]) r.
Int -> (forall (x :: k). Membership xs x -> r) -> r
reifyMembership (Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i) ((forall {x :: k}. Membership xs x -> xs :/ Proxy) -> xs :/ Proxy)
-> (forall {x :: k}. Membership xs x -> xs :/ Proxy) -> xs :/ Proxy
forall a b. (a -> b) -> a -> b
$ \Membership xs x
m -> Membership xs x -> Proxy x -> xs :/ Proxy
forall {k} (xs :: [k]) (x :: k) (h :: k -> Type).
Membership xs x -> h x -> xs :/ h
EmbedAt Membership xs x
m Proxy x
forall {k} (t :: k). Proxy t
Proxy

instance (Last xs ∈ xs) => Bounded (xs :/ Proxy) where
  minBound :: xs :/ Proxy
minBound = Int
-> (forall {x :: k}. Membership xs x -> xs :/ Proxy) -> xs :/ Proxy
forall {k} (xs :: [k]) r.
Int -> (forall (x :: k). Membership xs x -> r) -> r
reifyMembership Int
0 ((forall {x :: k}. Membership xs x -> xs :/ Proxy) -> xs :/ Proxy)
-> (forall {x :: k}. Membership xs x -> xs :/ Proxy) -> xs :/ Proxy
forall a b. (a -> b) -> a -> b
$ \Membership xs x
m -> Membership xs x -> Proxy x -> xs :/ Proxy
forall {k} (xs :: [k]) (x :: k) (h :: k -> Type).
Membership xs x -> h x -> xs :/ h
EmbedAt Membership xs x
m Proxy x
forall {k} (t :: k). Proxy t
Proxy
  maxBound :: xs :/ Proxy
maxBound = Membership xs (Last xs) -> Proxy (Last xs) -> xs :/ Proxy
forall {k} (xs :: [k]) (x :: k) (h :: k -> Type).
Membership xs x -> h x -> xs :/ h
EmbedAt (Membership xs (Last xs)
forall {k} (xs :: [k]) (x :: k). Member xs x => Membership xs x
membership :: Membership xs (Last xs)) Proxy (Last xs)
forall {k} (t :: k). Proxy t
Proxy

-- | Change the wrapper.
hoist :: (forall x. g x -> h x) -> xs :/ g -> xs :/ h
hoist :: forall {k} (g :: k -> Type) (h :: k -> Type) (xs :: [k]).
(forall (x :: k). g x -> h x) -> (xs :/ g) -> xs :/ h
hoist forall (x :: k). g x -> h x
f (EmbedAt Membership xs x
p g x
h) = Membership xs x -> h x -> xs :/ h
forall {k} (xs :: [k]) (x :: k) (h :: k -> Type).
Membership xs x -> h x -> xs :/ h
EmbedAt Membership xs x
p (g x -> h x
forall (x :: k). g x -> h x
f g x
h)
{-# INLINE hoist #-}

-- | /O(1)/ lift a value.
embed :: (x ∈ xs) => h x -> xs :/ h
embed :: forall {k} (x :: k) (xs :: [k]) (h :: k -> Type).
(x ∈ xs) =>
h x -> xs :/ h
embed = Membership xs x -> h x -> xs :/ h
forall {k} (xs :: [k]) (x :: k) (h :: k -> Type).
Membership xs x -> h x -> xs :/ h
EmbedAt Membership xs x
forall {k} (xs :: [k]) (x :: k). Member xs x => Membership xs x
membership
{-# INLINE embed #-}

-- | Try to extract something you want.
strike :: forall h x xs. (x ∈ xs) => xs :/ h -> Maybe (h x)
strike :: forall {k} (h :: k -> Type) (x :: k) (xs :: [k]).
(x ∈ xs) =>
(xs :/ h) -> Maybe (h x)
strike = Membership xs x -> (xs :/ h) -> Maybe (h x)
forall {k} (h :: k -> Type) (x :: k) (xs :: [k]).
Membership xs x -> (xs :/ h) -> Maybe (h x)
strikeAt Membership xs x
forall {k} (xs :: [k]) (x :: k). Member xs x => Membership xs x
membership
{-# INLINE strike #-}

-- | Try to extract something you want.
strikeAt :: forall h x xs. Membership xs x -> xs :/ h -> Maybe (h x)
strikeAt :: forall {k} (h :: k -> Type) (x :: k) (xs :: [k]).
Membership xs x -> (xs :/ h) -> Maybe (h x)
strikeAt Membership xs x
q (EmbedAt Membership xs x
p h x
h) = case Membership xs x -> Membership xs x -> Either Ordering (x :~: x)
forall {k} (xs :: [k]) (x :: k) (y :: k).
Membership xs x -> Membership xs y -> Either Ordering (x :~: y)
compareMembership Membership xs x
p Membership xs x
q of
  Right x :~: x
Refl -> h x -> Maybe (h x)
forall a. a -> Maybe a
Just h x
h x
h
  Either Ordering (x :~: x)
_ -> Maybe (h x)
forall a. Maybe a
Nothing
{-# INLINE strikeAt #-}

-- | /O(1)/ Naive pattern match
(<:|) :: (h x -> r)
    -> (xs :/ h -> r)
    -> (x ': xs) :/ h
    -> r
<:| :: forall {k} (h :: k -> Type) (x :: k) r (xs :: [k]).
(h x -> r) -> ((xs :/ h) -> r) -> ((x : xs) :/ h) -> r
(<:|) h x -> r
r (xs :/ h) -> r
c = \(EmbedAt Membership (x : xs) x
i h x
h) -> Membership (x : xs) x
-> ((x :~: x) -> r) -> (Membership xs x -> r) -> r
forall {k} (y :: k) (xs :: [k]) (x :: k) r.
Membership (y : xs) x
-> ((x :~: y) -> r) -> (Membership xs x -> r) -> r
testMembership Membership (x : xs) x
i
  (\x :~: x
Refl -> h x -> r
r h x
h x
h)
  (\Membership xs x
j -> (xs :/ h) -> r
c (Membership xs x -> h x -> xs :/ h
forall {k} (xs :: [k]) (x :: k) (h :: k -> Type).
Membership xs x -> h x -> xs :/ h
EmbedAt Membership xs x
j h x
h))
infixr 1 <:|
{-# INLINE (<:|) #-}

-- | There is no empty union.
exhaust :: '[] :/ h -> r
exhaust :: forall {k} (h :: k -> Type) r. ('[] :/ h) -> r
exhaust '[] :/ h
_ = [Char] -> r
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible"

-- | Embed a value, but focuses on its key.
embedAssoc :: Lookup xs k a => h (k ':> a) -> xs :/ h
embedAssoc :: forall {k} {v} (xs :: [Assoc k v]) (k :: k) (a :: v)
       (h :: Assoc k v -> Type).
Lookup xs k a =>
h (k ':> a) -> xs :/ h
embedAssoc = Membership xs (k ':> a) -> h (k ':> a) -> xs :/ h
forall {k} (xs :: [k]) (x :: k) (h :: k -> Type).
Membership xs x -> h x -> xs :/ h
EmbedAt Membership xs (k ':> a)
forall {k} {v} (xs :: [Assoc k v]) (k1 :: k) (v1 :: v).
Lookup xs k1 v1 =>
Membership xs (k1 ':> v1)
association
{-# INLINE embedAssoc #-}

instance (Applicative f, Choice p) => Extensible f p (:/) where
  pieceAt :: forall (xs :: [k]) (h :: k -> Type) (x :: k).
ExtensibleConstr (:/) xs h x =>
Membership xs x -> Optic' p f (xs :/ h) (h x)
pieceAt Membership xs x
m = ((xs :/ h) -> Either (xs :/ h) (h x))
-> (Either (xs :/ h) (f (h x)) -> f (xs :/ h))
-> p (Either (xs :/ h) (h x)) (Either (xs :/ h) (f (h x)))
-> p (xs :/ h) (f (xs :/ h))
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: Type -> Type -> Type) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (\t :: xs :/ h
t@(EmbedAt Membership xs x
i h x
h) -> case Membership xs x -> Membership xs x -> Either Ordering (x :~: x)
forall {k} (xs :: [k]) (x :: k) (y :: k).
Membership xs x -> Membership xs y -> Either Ordering (x :~: y)
compareMembership Membership xs x
i Membership xs x
m of
    Right x :~: x
Refl -> h x -> Either (xs :/ h) (h x)
forall a b. b -> Either a b
Right h x
h
    Left Ordering
_ -> (xs :/ h) -> Either (xs :/ h) (h x)
forall a b. a -> Either a b
Left xs :/ h
t) (((xs :/ h) -> f (xs :/ h))
-> (f (h x) -> f (xs :/ h))
-> Either (xs :/ h) (f (h x))
-> f (xs :/ h)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (xs :/ h) -> f (xs :/ h)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ((h x -> xs :/ h) -> f (h x) -> f (xs :/ h)
forall a b. (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Membership xs x -> h x -> xs :/ h
forall {k} (xs :: [k]) (x :: k) (h :: k -> Type).
Membership xs x -> h x -> xs :/ h
EmbedAt Membership xs x
m))) (p (Either (xs :/ h) (h x)) (Either (xs :/ h) (f (h x)))
 -> p (xs :/ h) (f (xs :/ h)))
-> (p (h x) (f (h x))
    -> p (Either (xs :/ h) (h x)) (Either (xs :/ h) (f (h x))))
-> p (h x) (f (h x))
-> p (xs :/ h) (f (xs :/ h))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (h x) (f (h x))
-> p (Either (xs :/ h) (h x)) (Either (xs :/ h) (f (h x)))
forall a b c. p a b -> p (Either c a) (Either c b)
forall (p :: Type -> Type -> Type) a b c.
Choice p =>
p a b -> p (Either c a) (Either c b)
right'
  {-# INLINABLE pieceAt #-}