{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Data.Dependent.Sum where

import Control.Applicative

import Data.Constraint.Extras
import Data.Type.Equality ((:~:) (..))

import Data.GADT.Show
import Data.GADT.Compare

import Data.Maybe (fromMaybe)

import Text.Read

-- | A basic dependent sum type where the first component is a tag
-- that specifies the type of the second. For example, think of a GADT
-- such as:
--
-- > data Tag a where
-- >    AString :: Tag String
-- >    AnInt   :: Tag Int
-- >    Rec     :: Tag (DSum Tag Identity)
--
-- Then we can write expressions where the RHS of @(':=>')@ has
-- different types depending on the @Tag@ constructor used. Here are
-- some expressions of type @DSum Tag 'Identity'@:
--
-- > AString :=> Identity "hello!"
-- > AnInt   :=> Identity 42
--
-- Often, the @f@ we choose has an 'Applicative' instance, and we can
-- use the helper function @('==>')@. The following expressions all
-- have the type @Applicative f => DSum Tag f@:
--
-- > AString ==> "hello!"
-- > AnInt   ==> 42
--
-- We can write functions that consume @DSum Tag f@ values by
-- matching, such as:
--
-- > toString :: DSum Tag Identity -> String
-- > toString (AString :=> Identity str) = str
-- > toString (AnInt   :=> Identity int) = show int
-- > toString (Rec     :=> Identity sum) = toString sum
--
-- The @(':=>')@ constructor and @('==>')@ helper are chosen to
-- resemble the @(key => value)@ construction for dictionary entries
-- in many dynamic languages. The @:=>@ and @==>@ operators have very
-- low precedence and bind to the right, making repeated use of these
-- operators behave as you'd expect:
--
-- > -- Parses as: Rec ==> (AnInt ==> (3 + 4))
-- > -- Has type: Applicative f => DSum Tag f
-- > Rec ==> AnInt ==> 3 + 4
--
-- The precedence of these operators is just above that of '$', so
-- @foo bar $ AString ==> "eep"@ is equivalent to @foo bar (AString
-- ==> "eep")@.
--
-- To use the 'Eq', 'Ord', 'Read', and 'Show' instances for @'DSum'
-- tag f@, you will need an 'ArgDict' instance for your tag type. Use
-- 'Data.Constraint.Extras.TH.deriveArgDict' from the
-- @constraints-extras@ package to generate this
-- instance.
data DSum tag f = forall a. !(tag a) :=> f a

infixr 1 :=>, ==>

-- | Convenience helper. Uses 'pure' to lift @a@ into @f a@.
(==>) :: Applicative f => tag a -> a -> DSum tag f
k :: tag a
k ==> :: tag a -> a -> DSum tag f
==> v :: a
v = tag a
k tag a -> f a -> DSum tag f
forall k (tag :: k -> *) (f :: k -> *) (a :: k).
tag a -> f a -> DSum tag f
:=> a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
v

instance forall tag f. (GShow tag, Has' Show tag f) => Show (DSum tag f) where
    showsPrec :: Int -> DSum tag f -> ShowS
showsPrec p :: Int
p (tag :: tag a
tag :=> value :: f a
value) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 10)
        ( Int -> tag a -> ShowS
forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
gshowsPrec 0 tag a
tag
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString " :=> "
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. tag a -> (Show (f a) => ShowS) -> ShowS
forall k k' (c :: k -> Constraint) (g :: k' -> k) (f :: k' -> *)
       (a :: k') r.
Has' c f g =>
f a -> (c (g a) => r) -> r
has' @Show @f tag a
tag (Int -> f a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec 1 f a
value)
        )

instance forall tag f. (GRead tag, Has' Read tag f) => Read (DSum tag f) where
    readsPrec :: Int -> ReadS (DSum tag f)
readsPrec p :: Int
p = Bool -> ReadS (DSum tag f) -> ReadS (DSum tag f)
forall a. Bool -> ReadS a -> ReadS a
readParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1) (ReadS (DSum tag f) -> ReadS (DSum tag f))
-> ReadS (DSum tag f) -> ReadS (DSum tag f)
forall a b. (a -> b) -> a -> b
$ \s :: String
s ->
        [[(DSum tag f, String)]] -> [(DSum tag f, String)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            [ Some tag
-> (forall (a :: k). tag a -> [(DSum tag f, String)])
-> [(DSum tag f, String)]
forall k (tag :: k -> *) b.
Some tag -> (forall (a :: k). tag a -> b) -> b
getGReadResult Some tag
withTag ((forall (a :: k). tag a -> [(DSum tag f, String)])
 -> [(DSum tag f, String)])
-> (forall (a :: k). tag a -> [(DSum tag f, String)])
-> [(DSum tag f, String)]
forall a b. (a -> b) -> a -> b
$ \tag :: tag a
tag ->
                [ (tag a
tag tag a -> f a -> DSum tag f
forall k (tag :: k -> *) (f :: k -> *) (a :: k).
tag a -> f a -> DSum tag f
:=> f a
val, String
rest'')
                | (val :: f a
val, rest'' :: String
rest'') <- tag a -> (Read (f a) => [(f a, String)]) -> [(f a, String)]
forall k k' (c :: k -> Constraint) (g :: k' -> k) (f :: k' -> *)
       (a :: k') r.
Has' c f g =>
f a -> (c (g a) => r) -> r
has' @Read @f tag a
tag (Int -> ReadS (f a)
forall a. Read a => Int -> ReadS a
readsPrec 1 String
rest')
                ]
            | (withTag :: Some tag
withTag, rest :: String
rest) <- Int -> GReadS tag
forall k (t :: k -> *). GRead t => Int -> GReadS t
greadsPrec Int
p String
s
            , let (con :: String
con, rest' :: String
rest') = Int -> String -> (String, String)
forall a. Int -> [a] -> ([a], [a])
splitAt 5 String
rest
            , String
con String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== " :=> "
            ]

instance forall tag f. (GEq tag, Has' Eq tag f) => Eq (DSum tag f) where
    (t1 :: tag a
t1 :=> x1 :: f a
x1) == :: DSum tag f -> DSum tag f -> Bool
== (t2 :: tag a
t2 :=> x2 :: f a
x2)  = Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
False (Maybe Bool -> Bool) -> Maybe Bool -> Bool
forall a b. (a -> b) -> a -> b
$ do
        a :~: a
Refl <- tag a -> tag a -> Maybe (a :~: a)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq tag a
t1 tag a
t2
        Bool -> Maybe Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ tag a -> (Eq (f a) => Bool) -> Bool
forall k k' (c :: k -> Constraint) (g :: k' -> k) (f :: k' -> *)
       (a :: k') r.
Has' c f g =>
f a -> (c (g a) => r) -> r
has' @Eq @f tag a
t1 (f a
x1 f a -> f a -> Bool
forall a. Eq a => a -> a -> Bool
== f a
f a
x2)

instance forall tag f. (GCompare tag, Has' Eq tag f, Has' Ord tag f) => Ord (DSum tag f) where
    compare :: DSum tag f -> DSum tag f -> Ordering
compare (t1 :: tag a
t1 :=> x1 :: f a
x1) (t2 :: tag a
t2 :=> x2 :: f a
x2)  = case tag a -> tag a -> GOrdering a a
forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare tag a
t1 tag a
t2 of
        GLT -> Ordering
LT
        GGT -> Ordering
GT
        GEQ -> tag a -> (Eq (f a) => Ordering) -> Ordering
forall k k' (c :: k -> Constraint) (g :: k' -> k) (f :: k' -> *)
       (a :: k') r.
Has' c f g =>
f a -> (c (g a) => r) -> r
has' @Eq @f tag a
t1 ((Eq (f a) => Ordering) -> Ordering)
-> (Eq (f a) => Ordering) -> Ordering
forall a b. (a -> b) -> a -> b
$ tag a -> (Ord (f a) => Ordering) -> Ordering
forall k k' (c :: k -> Constraint) (g :: k' -> k) (f :: k' -> *)
       (a :: k') r.
Has' c f g =>
f a -> (c (g a) => r) -> r
has' @Ord @f tag a
t1 (f a
x1 f a -> f a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` f a
f a
x2)

{-# DEPRECATED ShowTag "Instead of 'ShowTag tag f', use '(GShow tag, Has' Show tag f)'" #-}
type ShowTag tag f = (GShow tag, Has' Show tag f)

showTaggedPrec :: forall tag f a. (GShow tag, Has' Show tag f) => tag a -> Int -> f a -> ShowS
showTaggedPrec :: tag a -> Int -> f a -> ShowS
showTaggedPrec tag :: tag a
tag = tag a -> (Show (f a) => Int -> f a -> ShowS) -> Int -> f a -> ShowS
forall k k' (c :: k -> Constraint) (g :: k' -> k) (f :: k' -> *)
       (a :: k') r.
Has' c f g =>
f a -> (c (g a) => r) -> r
has' @Show @f tag a
tag Show (f a) => Int -> f a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec

{-# DEPRECATED ReadTag "Instead of 'ReadTag tag f', use '(GRead tag, Has' Read tag f)'" #-}
type ReadTag tag f = (GRead tag, Has' Read tag f)

readTaggedPrec :: forall tag f a. (GRead tag, Has' Read tag f) => tag a -> Int -> ReadS (f a)
readTaggedPrec :: tag a -> Int -> ReadS (f a)
readTaggedPrec tag :: tag a
tag = tag a -> (Read (f a) => Int -> ReadS (f a)) -> Int -> ReadS (f a)
forall k k' (c :: k -> Constraint) (g :: k' -> k) (f :: k' -> *)
       (a :: k') r.
Has' c f g =>
f a -> (c (g a) => r) -> r
has' @Read @f tag a
tag Read (f a) => Int -> ReadS (f a)
forall a. Read a => Int -> ReadS a
readsPrec

{-# DEPRECATED EqTag "Instead of 'EqTag tag f', use '(GEq tag, Has' Eq tag f)'" #-}
type EqTag tag f = (GEq tag, Has' Eq tag f)

eqTaggedPrec :: forall tag f a. (GEq tag, Has' Eq tag f) => tag a -> tag a -> f a -> f a -> Bool
eqTaggedPrec :: tag a -> tag a -> f a -> f a -> Bool
eqTaggedPrec tag1 :: tag a
tag1 tag2 :: tag a
tag2 f1 :: f a
f1 f2 :: f a
f2 = case tag a
tag1 tag a -> tag a -> Maybe (a :~: a)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
`geq` tag a
tag2 of
  Nothing -> Bool
False
  Just Refl -> tag a -> (Eq (f a) => Bool) -> Bool
forall k k' (c :: k -> Constraint) (g :: k' -> k) (f :: k' -> *)
       (a :: k') r.
Has' c f g =>
f a -> (c (g a) => r) -> r
has' @Eq @f tag a
tag1 ((Eq (f a) => Bool) -> Bool) -> (Eq (f a) => Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ f a
f1 f a -> f a -> Bool
forall a. Eq a => a -> a -> Bool
== f a
f2

eqTagged :: forall tag f a. EqTag tag f => tag a -> tag a -> f a -> f a -> Bool
eqTagged :: tag a -> tag a -> f a -> f a -> Bool
eqTagged k :: tag a
k _ x0 :: f a
x0 x1 :: f a
x1 = tag a -> (Eq (f a) => Bool) -> Bool
forall k k' (c :: k -> Constraint) (g :: k' -> k) (f :: k' -> *)
       (a :: k') r.
Has' c f g =>
f a -> (c (g a) => r) -> r
has' @Eq @f tag a
k (f a
x0 f a -> f a -> Bool
forall a. Eq a => a -> a -> Bool
== f a
x1)

{-# DEPRECATED OrdTag "Instead of 'OrdTag tag f', use '(GCompare tag, Has' Eq tag f, Has' Ord tag f)'" #-}
type OrdTag tag f = (GCompare tag, Has' Eq tag f, Has' Ord tag f)

compareTaggedPrec :: forall tag f a. (GCompare tag, Has' Eq tag f, Has' Ord tag f) => tag a -> tag a -> f a -> f a -> Ordering
compareTaggedPrec :: tag a -> tag a -> f a -> f a -> Ordering
compareTaggedPrec tag1 :: tag a
tag1 tag2 :: tag a
tag2 f1 :: f a
f1 f2 :: f a
f2 = case tag a
tag1 tag a -> tag a -> GOrdering a a
forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
`gcompare` tag a
tag2 of
  GLT -> Ordering
LT
  GEQ -> tag a -> (Eq (f a) => Ordering) -> Ordering
forall k k' (c :: k -> Constraint) (g :: k' -> k) (f :: k' -> *)
       (a :: k') r.
Has' c f g =>
f a -> (c (g a) => r) -> r
has' @Eq @f tag a
tag1 ((Eq (f a) => Ordering) -> Ordering)
-> (Eq (f a) => Ordering) -> Ordering
forall a b. (a -> b) -> a -> b
$ tag a -> (Ord (f a) => Ordering) -> Ordering
forall k k' (c :: k -> Constraint) (g :: k' -> k) (f :: k' -> *)
       (a :: k') r.
Has' c f g =>
f a -> (c (g a) => r) -> r
has' @Ord @f tag a
tag1 ((Ord (f a) => Ordering) -> Ordering)
-> (Ord (f a) => Ordering) -> Ordering
forall a b. (a -> b) -> a -> b
$ f a
f1 f a -> f a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` f a
f2
  GGT -> Ordering
GT

compareTagged :: forall tag f a. OrdTag tag f => tag a -> tag a -> f a -> f a -> Ordering
compareTagged :: tag a -> tag a -> f a -> f a -> Ordering
compareTagged k :: tag a
k _ x0 :: f a
x0 x1 :: f a
x1 = tag a -> (Eq (f a) => Ordering) -> Ordering
forall k k' (c :: k -> Constraint) (g :: k' -> k) (f :: k' -> *)
       (a :: k') r.
Has' c f g =>
f a -> (c (g a) => r) -> r
has' @Eq @f tag a
k ((Eq (f a) => Ordering) -> Ordering)
-> (Eq (f a) => Ordering) -> Ordering
forall a b. (a -> b) -> a -> b
$ tag a -> (Ord (f a) => Ordering) -> Ordering
forall k k' (c :: k -> Constraint) (g :: k' -> k) (f :: k' -> *)
       (a :: k') r.
Has' c f g =>
f a -> (c (g a) => r) -> r
has' @Ord @f tag a
k (f a -> f a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare f a
x0 f a
x1)