{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE DataKinds #-}
module Data.Summer
(
Sum
, pattern Inj
, tag
, inject
, inspect
, consider
, considerFirst
, Match(match, override, unmatch)
, Unmatch
, TagIn
, HasTagIn
, Delete
, HaveSameTagsIn
, Matcher
, Weaken(weaken)
, noOpWeaken
, inmap
, smap
, ApplyFunction(apply)
, type ForAll
) where
import Control.Exception (catch, SomeException)
import Unsafe.Coerce (unsafeCoerce)
import GHC.Exts (Any, Constraint)
import GHC.TypeLits (Nat, KnownNat, natVal, type (+))
import Data.Proxy (Proxy(Proxy))
import Data.Kind (Type)
import Control.Monad (unless)
import Generics.SOP (Generic(..))
import qualified Generics.SOP as SOP
import Data.ForAll (type ForAll)
data Sum (xs :: [*]) = UnsafeInj {-# UNPACK #-} !Word Any
instance Generic (Sum '[]) where
type Code (Sum '[]) = '[]
from :: Sum '[] -> Rep (Sum '[])
from Sum '[]
a = [Char] -> SOP I '[]
forall a. HasCallStack => [Char] -> a
error [Char]
"Generics.SOP.from: Impossible to create an empty sum"
to :: Rep (Sum '[]) -> Sum '[]
to Rep (Sum '[])
a = [Char] -> Sum '[]
forall a. HasCallStack => [Char] -> a
error [Char]
"Generics.SOP.to: Impossible to create an empty sum"
instance Generic (Sum xs) => Generic (Sum (x ': xs)) where
type Code (Sum (x ': xs)) = '[x] ': Code (Sum xs)
from :: Sum (x : xs) -> Rep (Sum (x : xs))
from (UnsafeInj Word
0 Any
x) = NS (NP I) ('[x] : Code (Sum xs)) -> SOP I ('[x] : Code (Sum xs))
forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
SOP.SOP (NP I '[x] -> NS (NP I) ('[x] : Code (Sum xs))
forall k (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
SOP.Z (x -> I x
forall a. a -> I a
SOP.I (Any -> x
forall a b. a -> b
unsafeCoerce Any
x) I x -> NP I '[] -> NP I '[x]
forall k (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
SOP.:* NP I '[]
forall k (a :: k -> *). NP a '[]
SOP.Nil))
from Sum (x : xs)
xs = NS (NP I) ('[x] : Code (Sum xs)) -> SOP I ('[x] : Code (Sum xs))
forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
SOP.SOP (NS (NP I) (Code (Sum xs)) -> NS (NP I) ('[x] : Code (Sum xs))
forall k (a :: k -> *) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
SOP.S NS (NP I) (Code (Sum xs))
ns) where
SOP.SOP NS (NP I) (Code (Sum xs))
ns = Sum xs -> SOP I (Code (Sum xs))
forall a. Generic a => a -> Rep a
from (Sum (x : xs) -> Sum xs
forall x (xs :: [*]). Sum (x : xs) -> Sum xs
unsafeForgetFirst Sum (x : xs)
xs)
to :: Rep (Sum (x : xs)) -> Sum (x : xs)
to (SOP.SOP NS (NP I) (Code (Sum (x : xs)))
ns) = case NS (NP I) (Code (Sum (x : xs)))
ns of
SOP.Z (SOP.I x
x SOP.:* NP I xs
SOP.Nil) -> Word -> Any -> Sum (x : xs)
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj Word
0 (x -> Any
forall a b. a -> b
unsafeCoerce x
x)
SOP.S NS (NP I) xs
s -> Sum xs -> Sum (x : xs)
recall (SOP I (Code (Sum xs)) -> Sum xs
forall a. Generic a => Rep a -> a
to (NS (NP I) xs -> SOP I xs
forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
SOP.SOP NS (NP I) xs
s))
where
recall :: Sum xs -> Sum (x ': xs)
recall :: Sum xs -> Sum (x : xs)
recall (UnsafeInj Word
i Any
a) = Word -> Any -> Sum (x : xs)
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (Word
i Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1) Any
a
type role Sum representational
pattern Inj :: forall x xs. (x `HasTagIn` xs) => x -> Sum xs
pattern $bInj :: x -> Sum xs
$mInj :: forall r x (xs :: [*]).
HasTagIn x xs =>
Sum xs -> (x -> r) -> (Void# -> r) -> r
Inj x <- (inspect -> Just x)
where
Inj x
x = x -> Sum xs
forall x (xs :: [*]). HasTagIn x xs => x -> Sum xs
inject x
x
type family TagIn (x :: k) (xs :: [k]) where
TagIn x (x ': xs) = 0
TagIn x (y ': xs) = 1 + TagIn x xs
class KnownNat (x `TagIn` xs) => x `HasTagIn` xs
instance KnownNat (x `TagIn` xs) => x `HasTagIn` xs
tag :: forall x xs. x `HasTagIn` xs => Word
tag :: Word
tag = Integer -> Word
forall a. Num a => Integer -> a
fromInteger (Integer -> Word) -> Integer -> Word
forall a b. (a -> b) -> a -> b
$ Proxy (TagIn x xs) -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (TagIn x xs)
forall k (t :: k). Proxy t
Proxy @(TagIn x xs))
{-# INLINE CONLIKE tag #-}
inject :: forall x xs. (x `HasTagIn` xs) => x -> Sum xs
inject :: x -> Sum xs
inject x
x = Word -> Any -> Sum xs
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs) (x -> Any
forall a b. a -> b
unsafeCoerce x
x)
{-# INLINE CONLIKE inject #-}
inspect :: forall x xs. (x `HasTagIn` xs) => Sum xs -> Maybe x
inspect :: Sum xs -> Maybe x
inspect (UnsafeInj Word
tag' Any
x) = if HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
tag' then x -> Maybe x
forall a. a -> Maybe a
Just (Any -> x
forall a b. a -> b
unsafeCoerce Any
x) else Maybe x
forall a. Maybe a
Nothing
{-# INLINE CONLIKE inspect #-}
type family Delete (x :: k) (xs :: [k]) :: [k] where
Delete x (x ': xs) = xs
Delete x (y ': xs) = y ': Delete x xs
Delete x '[] = '[]
consider :: forall x xs. (x `HasTagIn` xs) => Sum xs -> Either (Sum (Delete x xs)) x
consider :: Sum xs -> Either (Sum (Delete x xs)) x
consider (UnsafeInj Word
tag' Any
x) =
if Word
tag' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs
then x -> Either (Sum (Delete x xs)) x
forall a b. b -> Either a b
Right (Any -> x
forall a b. a -> b
unsafeCoerce Any
x)
else Sum (Delete x xs) -> Either (Sum (Delete x xs)) x
forall a b. a -> Either a b
Left (Word -> Any -> Sum (Delete x xs)
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (if Word
tag' Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
>= HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs then Word
tag' Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1 else Word
tag') Any
x)
{-# INLINE CONLIKE consider #-}
considerFirst :: forall x xs. Sum (x ': xs) -> Either (Sum xs) x
considerFirst :: Sum (x : xs) -> Either (Sum xs) x
considerFirst = Sum (x : xs) -> Either (Sum xs) x
forall x (xs :: [*]).
HasTagIn x xs =>
Sum xs -> Either (Sum (Delete x xs)) x
consider
{-# INLINE CONLIKE considerFirst #-}
inmap :: forall x y xs. (x `HasTagIn` xs, y `HasTagIn` xs) => (x -> y) -> Sum xs -> Sum xs
inmap :: (x -> y) -> Sum xs -> Sum xs
inmap x -> y
f uv :: Sum xs
uv@(UnsafeInj Word
tag' Any
x) = if Word
tag' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs then Word -> Any -> Sum xs
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (HasTagIn y xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @y @xs) (y -> Any
forall a b. a -> b
unsafeCoerce (x -> y
f (Any -> x
forall a b. a -> b
unsafeCoerce Any
x))) else Sum xs
uv
{-# INLINE CONLIKE inmap #-}
smap :: forall x y xs ys. (Weaken (Delete x xs) ys, x `HasTagIn` xs, y `HasTagIn` ys) => (x -> y) -> Sum xs -> Sum ys
smap :: (x -> y) -> Sum xs -> Sum ys
smap x -> y
f uv :: Sum xs
uv@(UnsafeInj Word
tag' Any
x) = if Word
tag' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs then Word -> Any -> Sum ys
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (HasTagIn y ys => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @y @ys) (y -> Any
forall a b. a -> b
unsafeCoerce (x -> y
f (Any -> x
forall a b. a -> b
unsafeCoerce Any
x))) else Sum (Delete x xs) -> Sum ys
forall (xs :: [*]) (ys :: [*]). Weaken xs ys => Sum xs -> Sum ys
weaken (Sum xs -> Sum (Delete x xs)
forall x (xs :: [*]). HasTagIn x xs => Sum xs -> Sum (Delete x xs)
unsafeForget @x Sum xs
uv)
{-# INLINE CONLIKE smap #-}
class HaveSameTagsIn xs ys
instance {-# OVERLAPPABLE #-} HaveSameTagsIn '[] ys
instance {-# OVERLAPPABLE #-} HaveSameTagsIn xs ys => HaveSameTagsIn (x ': xs) (x ': ys)
noOpWeaken :: forall xs ys. (xs `HaveSameTagsIn` ys) => Sum xs -> Sum ys
noOpWeaken :: Sum xs -> Sum ys
noOpWeaken = Sum xs -> Sum ys
forall a b. a -> b
unsafeCoerce
{-# INLINE CONLIKE noOpWeaken #-}
unsafeForget :: forall x xs. x `HasTagIn` xs => Sum xs -> Sum (Delete x xs)
unsafeForget :: Sum xs -> Sum (Delete x xs)
unsafeForget (UnsafeInj Word
tag' Any
x) = if Word
tag' Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs then Word -> Any -> Sum (Delete x xs)
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj Word
tag' Any
x
else if Word
tag' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== HasTagIn x xs => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @xs then [Char] -> Sum (Delete x xs)
forall a. HasCallStack => [Char] -> a
error [Char]
"unsafeForget: you can't forget the truth"
else Word -> Any -> Sum (Delete x xs)
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (Word
tag' Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1) Any
x
unsafeForgetFirst :: Sum (x ': xs) -> Sum xs
unsafeForgetFirst :: Sum (x : xs) -> Sum xs
unsafeForgetFirst (UnsafeInj Word
tag' Any
x) = Word -> Any -> Sum xs
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (Word
tag' Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1) Any
x
{-# INLINE CONLIKE unsafeForget #-}
instance (Eq (Sum xs), Eq x) => Eq (Sum (x ': xs)) where
uv :: Sum (x : xs)
uv@(UnsafeInj Word
tag' Any
x) == :: Sum (x : xs) -> Sum (x : xs) -> Bool
== uv' :: Sum (x : xs)
uv'@(UnsafeInj Word
tag'' Any
x')
| Word
tag' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
tag'' =
if Word
tag' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0
then Any -> x
forall a b. a -> b
unsafeCoerce @_ @x Any
x x -> x -> Bool
forall a. Eq a => a -> a -> Bool
== Any -> x
forall a b. a -> b
unsafeCoerce @_ @x Any
x'
else Sum (x : xs) -> Sum xs
forall x (xs :: [*]). Sum (x : xs) -> Sum xs
unsafeForgetFirst Sum (x : xs)
uv Sum xs -> Sum xs -> Bool
forall a. Eq a => a -> a -> Bool
== Sum (x : xs) -> Sum xs
forall x (xs :: [*]). Sum (x : xs) -> Sum xs
unsafeForgetFirst Sum (x : xs)
uv'
| Bool
otherwise = Bool
False
{-# INLINE CONLIKE (==) #-}
instance Eq (Sum '[]) where
== :: Sum '[] -> Sum '[] -> Bool
(==) = [Char] -> Sum '[] -> Sum '[] -> Bool
forall a. HasCallStack => [Char] -> a
error [Char]
"(==) base case: impossible by construction"
class Weaken xs ys where
weaken :: Sum xs -> Sum ys
instance (Weaken xs ys, x `HasTagIn` ys) => Weaken (x ': xs) ys where
weaken :: Sum (x : xs) -> Sum ys
weaken uv :: Sum (x : xs)
uv@(UnsafeInj Word
tag' Any
x) =
if Word
tag' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0
then Word -> Any -> Sum ys
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (HasTagIn x ys => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @ys) Any
x
else let UnsafeInj Word
tag'' Any
_ = Sum xs -> Sum ys
forall (xs :: [*]) (ys :: [*]). Weaken xs ys => Sum xs -> Sum ys
weaken @xs @ys (Sum (x : xs) -> Sum xs
forall x (xs :: [*]). Sum (x : xs) -> Sum xs
unsafeForgetFirst Sum (x : xs)
uv) in Word -> Any -> Sum ys
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj Word
tag'' Any
x
{-# INLINE CONLIKE weaken #-}
instance Weaken '[] ys where
weaken :: Sum '[] -> Sum ys
weaken = [Char] -> Sum '[] -> Sum ys
forall a. HasCallStack => [Char] -> a
error [Char]
"weaken base case: impossible by construction"
{-# INLINE CONLIKE weaken #-}
type family Matcher xs r :: Type where
Matcher '[] r = r
Matcher (x ': xs) r = (x -> r) -> Matcher xs r
class Match xs where
match :: forall r. Sum xs -> Matcher xs r
unmatch :: (forall r. Matcher xs r) -> Sum xs
override :: forall r. r -> Matcher xs r -> Matcher xs r
instance Match '[] where
match :: Sum '[] -> Matcher '[] r
match = [Char] -> Sum '[] -> r
forall a. HasCallStack => [Char] -> a
error [Char]
"match base case: impossible by construction"
{-# INLINE CONLIKE match #-}
unmatch :: (forall r. Matcher '[] r) -> Sum '[]
unmatch forall r. Matcher '[] r
r = Sum '[]
forall r. Matcher '[] r
r
{-# INLINE CONLIKE unmatch #-}
override :: r -> Matcher '[] r -> Matcher '[] r
override = r -> Matcher '[] r -> Matcher '[] r
forall a b. a -> b -> a
const
{-# INLINE CONLIKE override #-}
instance (Unmatch xs (x ': xs), Match xs) => Match (x ': xs) where
match :: forall r. Sum (x ': xs) -> (x -> r) -> Matcher xs r
match :: Sum (x : xs) -> (x -> r) -> Matcher xs r
match uv :: Sum (x : xs)
uv@(UnsafeInj Word
tag' Any
x) x -> r
f =
if Word
tag' Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0
then r -> Matcher xs r -> Matcher xs r
forall (xs :: [*]) r. Match xs => r -> Matcher xs r -> Matcher xs r
override @xs @r (x -> r
f (Any -> x
forall a b. a -> b
unsafeCoerce Any
x)) (Matcher xs r -> Matcher xs r) -> Matcher xs r -> Matcher xs r
forall a b. (a -> b) -> a -> b
$ Sum xs -> Matcher xs r
forall (xs :: [*]) r. Match xs => Sum xs -> Matcher xs r
match @xs @r (Sum (x : xs) -> Sum xs
forall x (xs :: [*]). Sum (x : xs) -> Sum xs
unsafeForgetFirst Sum (x : xs)
uv)
else Sum xs -> Matcher xs r
forall (xs :: [*]) r. Match xs => Sum xs -> Matcher xs r
match @xs @r (Sum (x : xs) -> Sum xs
forall x (xs :: [*]). Sum (x : xs) -> Sum xs
unsafeForgetFirst Sum (x : xs)
uv)
{-# INLINE CONLIKE match #-}
unmatch :: (forall r. (x -> r) -> Matcher xs r) -> Sum (x ': xs)
unmatch :: (forall r. (x -> r) -> Matcher xs r) -> Sum (x : xs)
unmatch forall r. (x -> r) -> Matcher xs r
g = forall (ys :: [*]). Unmatch xs ys => Matcher xs (Sum ys) -> Sum ys
forall (xs :: [*]) (ys :: [*]).
Unmatch xs ys =>
Matcher xs (Sum ys) -> Sum ys
unmatchGo @xs (Matcher xs (Sum (x : xs)) -> Sum (x : xs))
-> Matcher xs (Sum (x : xs)) -> Sum (x : xs)
forall a b. (a -> b) -> a -> b
$ (x -> Sum (x : xs)) -> Matcher xs (Sum (x : xs))
forall r. (x -> r) -> Matcher xs r
g @(Sum (x ': xs)) (Word -> Any -> Sum (x : xs)
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj Word
0 (Any -> Sum (x : xs)) -> (x -> Any) -> x -> Sum (x : xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b. x -> b
forall a b. a -> b
unsafeCoerce @x)
{-# INLINE CONLIKE unmatch #-}
override :: r -> Matcher (x : xs) r -> Matcher (x : xs) r
override r
r Matcher (x : xs) r
m = (Matcher xs r -> Matcher xs r)
-> ((x -> r) -> Matcher xs r) -> (x -> r) -> Matcher xs r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (r -> Matcher xs r -> Matcher xs r
forall (xs :: [*]) r. Match xs => r -> Matcher xs r -> Matcher xs r
override @xs r
r) Matcher (x : xs) r
(x -> r) -> Matcher xs r
m
{-# INLINE CONLIKE override #-}
class Unmatch xs ys where
unmatchGo :: Matcher xs (Sum ys) -> Sum ys
instance Unmatch '[] ys where
unmatchGo :: Matcher '[] (Sum ys) -> Sum ys
unmatchGo = Matcher '[] (Sum ys) -> Sum ys
forall a. a -> a
id
{-# INLINE CONLIKE unmatchGo #-}
instance (Unmatch xs ys, x `HasTagIn` ys) => Unmatch (x ': xs) ys where
unmatchGo :: Matcher (x : xs) (Sum ys) -> Sum ys
unmatchGo Matcher (x : xs) (Sum ys)
f = Matcher xs (Sum ys) -> Sum ys
forall (xs :: [*]) (ys :: [*]).
Unmatch xs ys =>
Matcher xs (Sum ys) -> Sum ys
unmatchGo @xs (Matcher (x : xs) (Sum ys)
(x -> Sum ys) -> Matcher xs (Sum ys)
f (Word -> Any -> Sum ys
forall (xs :: [*]). Word -> Any -> Sum xs
UnsafeInj (HasTagIn x ys => Word
forall k (x :: k) (xs :: [k]). HasTagIn x xs => Word
tag @x @ys) (Any -> Sum ys) -> (x -> Any) -> x -> Sum ys
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b. x -> b
forall a b. a -> b
unsafeCoerce @x))
{-# INLINE CONLIKE unmatchGo #-}
class ForAll c xs => ApplyFunction c xs where
apply :: (forall a. c a => a -> y) -> Sum xs -> y
instance ApplyFunction c '[] where
apply :: (forall a. c a => a -> y) -> Sum '[] -> y
apply forall a. c a => a -> y
_f Sum '[]
x = [Char] -> y
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: empty sum"
instance (c x, ApplyFunction c xs) => ApplyFunction c (x ': xs) where
apply :: (forall a. c a => a -> y) -> Sum (x : xs) -> y
apply forall a. c a => a -> y
f Sum (x : xs)
x = case Sum (x : xs) -> Either (Sum xs) x
forall x (xs :: [*]). Sum (x : xs) -> Either (Sum xs) x
considerFirst Sum (x : xs)
x of
Right x
x' -> x -> y
forall a. c a => a -> y
f x
x'
Left Sum xs
xs -> (forall a. c a => a -> y) -> Sum xs -> y
forall (c :: * -> Constraint) (xs :: [*]) y.
ApplyFunction c xs =>
(forall a. c a => a -> y) -> Sum xs -> y
apply @c forall a. c a => a -> y
f Sum xs
xs