{-# 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
, Match(match, override, unmatch)
, Unmatch
, TagIn
, HasTagIn
, Delete
, HaveSameTagsIn
, Matcher
, Weaken(weaken)
, noOpWeaken
, inmap
, smap
) 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)
data Sum (xs :: [*]) = UnsafeInj {-# UNPACK #-} !Word Any
type role Sum representational
pattern Inj :: forall x xs. (x `HasTagIn` xs) => x -> Sum xs
pattern Inj x <- (inspect -> Just x)
where
Inj x = inject 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 = fromInteger $ natVal (Proxy @(TagIn x xs))
{-# INLINE CONLIKE tag #-}
inject :: forall x xs. (x `HasTagIn` xs) => x -> Sum xs
inject x = UnsafeInj (tag @x @xs) (unsafeCoerce x)
{-# INLINE CONLIKE inject #-}
inspect :: forall x xs. (x `HasTagIn` xs) => Sum xs -> Maybe x
inspect (UnsafeInj tag' x) = if tag @x @xs == tag' then Just (unsafeCoerce x) else 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 (UnsafeInj tag' x) =
if tag' == tag @x @xs
then Right (unsafeCoerce x)
else Left (UnsafeInj (if tag' >= tag @x @xs then tag' - 1 else tag') x)
{-# INLINE CONLIKE consider #-}
considerFirst :: forall x xs. Sum (x ': xs) -> Either (Sum xs) x
considerFirst = consider
{-# INLINE CONLIKE considerFirst #-}
inmap :: forall x y xs. (x `HasTagIn` xs, y `HasTagIn` xs) => (x -> y) -> Sum xs -> Sum xs
inmap f uv@(UnsafeInj tag' x) = if tag' == tag @x @xs then UnsafeInj (tag @y @xs) (unsafeCoerce (f (unsafeCoerce x))) else uv
{-# INLINE CONLIKE inmap #-}
smap :: forall x y xs ys. (Weaken xs ys, x `HasTagIn` xs, y `HasTagIn` ys) => (x -> y) -> Sum xs -> Sum ys
smap f uv@(UnsafeInj tag' x) = if tag' == tag @x @xs then UnsafeInj (tag @y @ys) (unsafeCoerce (f (unsafeCoerce x))) else weaken 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 = unsafeCoerce
{-# INLINE CONLIKE noOpWeaken #-}
unsafeForget :: Sum (x ': xs) -> Sum xs
unsafeForget (UnsafeInj tag' x) = UnsafeInj (tag' - 1) x
{-# INLINE CONLIKE unsafeForget #-}
instance (Eq (Sum xs), Eq x) => Eq (Sum (x ': xs)) where
uv@(UnsafeInj tag' x) == uv'@(UnsafeInj tag'' x')
| tag' == tag'' =
if tag' == 0
then unsafeCoerce @_ @x x == unsafeCoerce @_ @x x'
else unsafeForget uv == unsafeForget uv'
| otherwise = False
{-# INLINE CONLIKE (==) #-}
instance Eq (Sum '[]) where
(==) = error "(==) 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 uv@(UnsafeInj tag' x) =
if tag' == 0
then UnsafeInj (tag @x @ys) x
else let UnsafeInj tag'' _ = weaken @xs @ys (unsafeForget uv) in UnsafeInj tag'' x
{-# INLINE CONLIKE weaken #-}
instance Weaken '[] ys where
weaken = error "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 = error "match base case: impossible by construction"
{-# INLINE CONLIKE match #-}
unmatch = id
{-# INLINE CONLIKE unmatch #-}
override = 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 uv@(UnsafeInj tag' x) f =
if tag' == 0
then override @xs @r (f (unsafeCoerce x)) $ match @xs @r (unsafeForget uv)
else match @xs @r (unsafeForget uv)
{-# INLINE CONLIKE match #-}
unmatch :: (forall r. (x -> r) -> Matcher xs r) -> Sum (x ': xs)
unmatch g = unmatchGo @xs $ g @(Sum (x ': xs)) (UnsafeInj 0 . unsafeCoerce @x)
{-# INLINE CONLIKE unmatch #-}
override r m = fmap (override @xs r) m
{-# INLINE CONLIKE override #-}
class Unmatch xs ys where
unmatchGo :: Matcher xs (Sum ys) -> Sum ys
instance Unmatch '[] ys where
unmatchGo = id
{-# INLINE CONLIKE unmatchGo #-}
instance (Unmatch xs ys, x `HasTagIn` ys) => Unmatch (x ': xs) ys where
unmatchGo f = unmatchGo @xs (f (UnsafeInj (tag @x @ys) . unsafeCoerce @x))
{-# INLINE CONLIKE unmatchGo #-}