{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Data.Diverse.Which.Internal ( -- * 'Which' type Which(..) -- exporting constructor unsafely! -- * Single type -- ** Construction , impossible , pick , pick0 , pickOnly , pickL , pickN -- ** Destruction , obvious , trial , trial0 , trialL , trialN -- * Multiple types -- ** Injection , Diversify , diversify , diversify0 , diversifyL , DiversifyN , diversifyN -- ** Inverse Injection , Reinterpret , reinterpret , reinterpretL , ReinterpretN , reinterpretN -- * Catamorphism , Switch(..) , which , switch , SwitchN(..) , whichN , switchN ) where import Control.Applicative import Control.Monad import Data.Diverse.Case import Data.Diverse.Reduce import Data.Diverse.Reiterate import Data.Diverse.TypeLevel import Data.Kind import Data.Proxy import qualified GHC.Generics as G import GHC.Prim (Any, coerce) import GHC.TypeLits import Text.ParserCombinators.ReadPrec import Text.Read import qualified Text.Read.Lex as L import Unsafe.Coerce -- | A 'Which' is an anonymous sum type (also known as a polymorphic variant, or co-record) -- which can only contain one of the types in the typelist. -- This is essentially a typed version of 'Data.Dynamic'. -- -- The following functions are available can be used to manipulate unique types in the typelist -- -- * constructor: 'pick' -- * destructor: 'trial' -- * injection: 'diversify' and 'reinterpret' -- * catamorphism: 'which' or 'switch' -- -- These functions are type specified. This means labels are not required because the types themselves can be used to access the 'Which'. -- It is a compile error to use those functions for duplicate fields. -- -- For duplicate types in the list of possible types, Nat-indexed version of the functions are available: -- -- * constructor: 'pickN' -- * destructor: 'trialN' -- * inejction: 'diversifyN' and 'reinterpretN' -- * catamorphism: 'whichN' or 'switchN' -- -- Encoding: The variant contains a value whose type is at the given position in the type list. -- This is the same encoding as and . -- -- The constructor is only exported in the "Data.Diverse.Which.Internal" module data Which (xs :: [Type]) = Which {-# UNPACK #-} !Int Any -- Just like Haskus and HList versions, inferred type is phantom which is wrong -- representational means: -- @ -- Coercible '[Int] '[IntLike] => Coercible (Which '[Int]) (Which '[IntLike]) -- @ type role Which representational ---------------------------------------------- -- | A terminating 'G.Generic' instance for no types encoded as a 'impossible'. -- The 'G.C1' and 'G.S1' metadata are not encoded. instance G.Generic (Which '[]) where type Rep (Which '[]) = G.U1 from _ = {- G.U1 -} G.U1 to G.U1 = impossible -- | A terminating 'G.Generic' instance for one type encoded with 'pick''. -- The 'G.C1' and 'G.S1' metadata are not encoded. instance G.Generic (Which '[x]) where type Rep (Which '[x]) = G.Rec0 x from v = {- G.Rec0 -} G.K1 (obvious v) to ({- G.Rec0 -} G.K1 a) = pickOnly a -- | A 'G.Generic' instance encoded as either the 'x' value ('G.:+:') or the 'diversify0'ed remaining 'Which xs'. -- The 'G.C1' and 'G.S1' metadata are not encoded. instance G.Generic (Which (x ': x' ': xs)) where type Rep (Which (x ': x' ': xs)) = (G.Rec0 x) G.:+: (G.Rec0 (Which (x' ': xs))) from v = case trial0 v of Right x -> G.L1 ({- G.Rec0 -} G.K1 x) Left v' -> G.R1 ({- G.Rec0 -} G.K1 v') to {- G.Rec0 -} x = case x of G.L1 ({- G.Rec0 -} G.K1 a) -> pick0 a G.R1 ({- G.Rec0 -} G.K1 v) -> diversify0 v ----------------------------------------------------------------------- -- | A 'Which' with no alternatives. You can't do anything with 'impossible' -- except Eq, Read, and Show it. -- Using functions like 'switch' and 'trial' with 'impossible' is a compile error. -- 'impossible' is only useful as a 'Left'-over from 'trial'ing a @Which '[x]@ with one type. impossible :: Which '[] impossible = Which (-1) (unsafeCoerce ()) -- | Lift a value into a 'Which' of possibly other types @xs@. -- @xs@ can be inferred or specified with TypeApplications. -- NB. forall is used to specify @xs@ first, so TypeApplications can be used to specify @xs@ first -- -- @ -- 'pick' \'A' \@'[Int, Bool, Char, Maybe String] :: Which '[Int, Bool, Char, Maybe String] -- @ pick :: forall xs x. UniqueMember x xs => x -> Which xs pick = pick_ pick_ :: forall x xs n. (KnownNat n, n ~ IndexOf x xs) => x -> Which xs pick_ = Which (fromInteger (natVal @n Proxy)) . unsafeCoerce -- | A variation of 'pick' where @x@ is specified via a label -- -- @ -- let y = 'pickL' \@Foo Proxy (Tagged (5 :: Int)) :: Which '[Bool, Tagged Foo Int, Tagged Bar Char] -- x = 'trialL' \@Foo Proxy y -- x `shouldBe` (Right (Tagged 5)) -- @ pickL :: forall l xs x proxy. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> x -> Which xs pickL _ = pick_ @x -- | A variation of 'pick' into a 'Which' of a single type. -- -- @ -- 'pickOnly' \'A' :: Which '[Char] -- @ pickOnly :: x -> Which '[x] pickOnly = pick0 -- | A variation of 'pick' into a 'Which' where @x@ is the first type. -- -- @ -- 'pick0' \'A' :: Which '[Char, Int, Bool] -- @ pick0 :: x -> Which (x ': xs) pick0 = Which 0 . unsafeCoerce -- | Lift a value into a 'Which' of possibly other (possibley indistinct) types, where the value is the @n@-th type. -- -- @ -- 'pickN' (Proxy \@4) (5 :: Int) :: Which '[Bool, Int, Char, Bool, Int, Char] -- @ pickN :: forall n xs x proxy. MemberAt n x xs => proxy n -> x -> Which xs pickN _ = Which (fromInteger (natVal @n Proxy)) . unsafeCoerce -- | It is 'obvious' what value is inside a 'Which' of one type. -- -- @ -- let x = 'pick'' \'A' :: Which '[Char] -- 'obvious' x \`shouldBe` \'A' -- @ obvious :: Which '[a] -> a obvious (Which _ v) = unsafeCoerce v -- | 'trial' a type in a 'Which' and 'Either' get the 'Right' value or the 'Left'-over possibilities. -- -- @ -- let x = 'pick' \'A' \@'[Int, Bool, Char, Maybe String] :: 'Which' '[Int, Bool, Char, Maybe String] -- 'trial' \@Char x \`shouldBe` Right \'A' -- 'trial' \@Int x \`shouldBe` Left ('pick' \'A') :: 'Which' '[Bool, Char, Maybe String] -- @ trial :: forall x xs. (UniqueMember x xs) => Which xs -> Either (Which (Without x xs)) x trial = trial_ trial_ :: forall x xs n. (KnownNat n, n ~ IndexOf x xs) => Which xs -> Either (Which (Without x xs)) x trial_ (Which n v) = let i = fromInteger (natVal @n Proxy) in if n == i then Right (unsafeCoerce v) else if n > i then Left (Which (n - 1) v) else Left (Which n v) -- | A variation of 'trial' where x is specified via a label -- -- @ -- let y = 'pickL' \@Foo Proxy (Tagged (5 :: Int)) :: Which '[Bool, Tagged Foo Int, Tagged Bar Char] -- x = 'trialL' \@Foo Proxy y -- x `shouldBe` (Right (Tagged 5)) -- @ trialL :: forall l xs x proxy. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> Which xs -> Either (Which (Without x xs)) x trialL _ = trial_ @x -- | A variation of a 'Which' 'trial' which 'trial's the first type in the type list. -- -- @ -- let x = 'pick' \'A' \@'[Int, Bool, Char, Maybe String] :: 'Which' '[Int, Bool, Char, Maybe String] -- 'trial0' x \`shouldBe` Left ('pick' \'A') :: 'Which' '[Bool, Char, Maybe String] -- @ trial0 :: Which (x ': xs) -> Either (Which xs) x trial0 (Which n v) = if n == 0 then Right (unsafeCoerce v) else Left (Which (n - 1) v) -- | 'trialN' the n-th type of a 'Which', and get 'Either' the 'Right' value or the 'Left'-over possibilities. -- -- @ -- let x = 'pick' \'A' \@'[Int, Bool, Char, Maybe String] :: 'Which' '[Int, Bool, Char, Maybe String] -- 'trialN' @1 Proxy x \`shouldBe` Left ('pick' \'A') :: 'Which' '[Int, Char, Maybe String] -- @ trialN :: forall n xs x proxy. (MemberAt n x xs) => proxy n -> Which xs -> Either (Which (WithoutIndex n xs)) x trialN _ (Which n v) = let i = fromInteger (natVal @n Proxy) in if n == i then Right (unsafeCoerce v) else if n > i then Left (Which (n - 1) v) else Left (Which n v) ----------------------------------------------------------------- -- | A friendlier constraint synonym for 'diversify'. type Diversify (tree :: [Type]) (branch :: [Type]) = Reduce (Which branch) (Switch (CaseDiversify tree branch) branch) (Which tree) -- | Convert a 'Which' to another 'Which' that may include other possibilities. -- That is, @branch@ is equal or is a subset of @tree@. -- -- This can also be used to rearrange the order of the types in the 'Which'. -- -- It is a compile error if @tree@ has duplicate types with @branch@. -- -- NB. forall is used to @tree@ is ordered first, so TypeApplications can be used to specify @tree@ first. -- -- @ -- let a = 'pick'' (5 :: Int) :: 'Which' '[Int] -- b = 'diversify' \@[Int, Bool] a :: 'Which' '[Int, Bool] -- c = 'diversify' \@[Bool, Int] b :: 'Which' '[Bool, Int] -- @ diversify :: forall tree branch. Diversify tree branch => Which branch -> Which tree diversify = which (CaseDiversify @tree @branch @branch) data CaseDiversify (tree :: [Type]) (branch :: [Type]) (branch' :: [Type]) r = CaseDiversify instance Reiterate (CaseDiversify tree branch) branch' where reiterate CaseDiversify = CaseDiversify -- | The @Unique x branch@ is important to get a compile error if the from @branch@ doesn't have a unique x instance (UniqueMember x tree, Unique x branch) => Case (CaseDiversify tree branch) (x ': branch') (Which tree) where case' CaseDiversify = pick -- | A simple version of 'diversify' which add another type to the front of the typelist. diversify0 :: forall x xs. Which xs -> Which (x ': xs) diversify0 (Which n v) = Which (n + 1) v ------------------------------------------------------------------ -- | A variation of 'diversify' where @branch@is additionally specified by a labels list. -- -- @ -- let y = 'pickOnly' (5 :: Tagged Bar Int) -- y' = 'diversifyL' \@'[Bar] Proxy y :: 'Which' '[Tagged Bar Int, Tagged Foo Bool] -- y'' = 'diversifyL' \@'[Bar, Foo] Proxy y' :: 'Which' '[Tagged Foo Bool, Tagged Bar Int] -- 'switch' y'' ('Data.Diverse.CaseTypeable.CaseTypeable' (show . typeRep . (pure \@Proxy))) \`shouldBe` \"Tagged * Bar Int" -- @ diversifyL :: forall ls tree branch proxy. ( Diversify tree branch , branch ~ KindsAtLabels ls tree , UniqueLabels ls tree , IsDistinct ls ) => proxy ls -> Which branch -> Which tree diversifyL _ = which (CaseDiversify @tree @branch @branch) ------------------------------------------------------------------ -- | A friendlier constraint synonym for 'diversifyN'. type DiversifyN (indices :: [Nat]) (tree :: [Type]) (branch :: [Type]) = ( Reduce (Which branch) (SwitchN (CaseDiversifyN indices) 0 branch) (Which tree) , KindsAtIndices indices tree ~ branch) -- | A variation of 'diversify' which uses a Nat list @indices@ to specify how to reorder the fields, where -- -- @ -- indices[branch_idx] = tree_idx -- @ -- -- This variation allows @tree@ to contain duplicate types with @branch@ since -- the mapping is specified by @indicies@. -- -- @ -- let y = 'pickOnly' (5 :: Int) -- y' = 'diversifyN' \@'[0] \@[Int, Bool] Proxy y -- y'' = 'diversifyN' \@[1,0] \@[Bool, Int] Proxy y' -- 'switch' y'' ('Data.Diverse.CaseTypeable.CaseTypeable' (show . typeRep . (pure \@Proxy))) \`shouldBe` \"Int" -- @ diversifyN :: forall indices tree branch proxy. (DiversifyN indices tree branch) => proxy indices -> Which branch -> Which tree diversifyN _ = whichN (CaseDiversifyN @indices @0 @branch) data CaseDiversifyN (indices :: [Nat]) (n :: Nat) (branch' :: [Type]) r = CaseDiversifyN instance ReiterateN (CaseDiversifyN indices) n branch' where reiterateN CaseDiversifyN = CaseDiversifyN instance MemberAt (KindAtIndex n indices) x tree => Case (CaseDiversifyN indices n) (x ': branch') (Which tree) where case' CaseDiversifyN v = pickN (Proxy @(KindAtIndex n indices)) v ------------------------------------------------------------------ -- | A friendlier constraint synonym for 'reinterpret'. type Reinterpret branch tree = Reduce (Which tree) (Switch (CaseReinterpret branch tree) tree) (Either (Which (Complement tree branch)) (Which branch)) -- | Convert a 'Which' into possibly another 'Which' with a totally different typelist. -- Returns either a 'Which' with the 'Right' value, or a 'Which' with the 'Left'over @compliment@ types. -- -- It is a compile error if @branch@ or @compliment@ has duplicate types with @tree@. -- -- NB. forall used to specify @branch@ first, so TypeApplications can be used to specify @branch@ first. -- -- @ -- let a = 'pick' \@[Int, Char, Bool] (5 :: Int) :: 'Which' '[Int, Char, Bool] -- let b = 'reinterpret' @[String, Char] y -- b \`shouldBe` Left ('pick' (5 :: Int)) :: 'Which' '[Int, Bool] -- let c = 'reinterpret' @[String, Int] a -- c \`shouldBe` Right ('pick' (5 :: Int)) :: 'Which' '[String, Int] -- @ reinterpret :: forall branch tree. Reinterpret branch tree => Which tree -> Either (Which (Complement tree branch)) (Which branch) reinterpret = which (CaseReinterpret @branch @tree @tree) data CaseReinterpret (branch :: [Type]) (tree :: [Type]) (tree' :: [Type]) r = CaseReinterpret instance Reiterate (CaseReinterpret branch tree) tree' where reiterate CaseReinterpret = CaseReinterpret instance ( MaybeUniqueMemberAt n x branch , comp ~ Complement tree branch , MaybeUniqueMemberAt n' x comp , Unique x tree -- Compile error to ensure reinterpret only works with unique fields ) => Case (CaseReinterpret branch tree) (x ': tree') (Either (Which comp) (Which branch)) where case' CaseReinterpret a = case fromInteger (natVal @n Proxy) of 0 -> let j = fromInteger (natVal @n' Proxy) -- safe use of partial! j will never be zero due to check above in Left $ Which (j - 1) (unsafeCoerce a) i -> Right $ Which (i - 1) (unsafeCoerce a) ------------------------------------------------------------------ -- | A variation of 'reinterpret' where the @branch@ is additionally specified with a labels list. -- -- @ -- let y = 'pick' \@[Tagged Bar Int, Tagged Foo Bool, Tagged Hi Char, Tagged Bye Bool] (5 :: Tagged Bar Int) -- y' = 'reinterpretL' \@[Foo, Bar] Proxy y -- x = 'pick' \@[Tagged Foo Bool, Tagged Bar Int] (5 :: Tagged Bar Int) -- y' \`shouldBe` Right x -- @ reinterpretL :: forall ls branch tree proxy. ( Reinterpret branch tree , branch ~ KindsAtLabels ls tree , UniqueLabels ls tree , IsDistinct ls ) => proxy ls -> Which tree -> Either (Which (Complement tree branch)) (Which branch) reinterpretL _ = which (CaseReinterpret @branch @tree @tree) ------------------------------------------------------------------ -- | A friendlier constraint synonym for 'reinterpretN'. type ReinterpretN (indices :: [Nat]) (branch :: [Type]) (tree :: [Type]) = ( Reduce (Which tree) (SwitchN (CaseReinterpretN indices) 0 tree) (Maybe (Which branch)) , KindsAtIndices indices tree ~ branch) -- | A limited variation of 'reinterpret' which uses a Nat list @n@ to specify how to reorder the fields, where -- -- @ -- indices[branch_idx] = tree_idx -- @ -- -- This variation allows @tree@ to contain duplicate types with @branch@ -- since the mapping is specified by @indicies@. -- -- However, unlike 'reinterpert', in this variation, -- @branch@ must be a subset of @tree@ instead of any arbitrary Which. -- Also it returns a Maybe instead of Either. -- -- This is so that the same @indices@ can be used in 'narrowN'. reinterpretN :: forall (indices :: [Nat]) branch tree proxy. (ReinterpretN indices branch tree) => proxy indices -> Which tree -> Maybe (Which branch) reinterpretN _ = whichN (CaseReinterpretN @indices @0 @tree) data CaseReinterpretN (indices :: [Nat]) (n :: Nat) (tree' :: [Type]) r = CaseReinterpretN instance ReiterateN (CaseReinterpretN indices) n tree' where reiterateN CaseReinterpretN = CaseReinterpretN instance (MaybeMemberAt n' x branch, n' ~ PositionOf n indices) => Case (CaseReinterpretN indices n) (x ': tree) (Maybe (Which branch)) where case' CaseReinterpretN a = case fromInteger (natVal @n' Proxy) of 0 -> Nothing i -> Just $ Which (i - 1) (unsafeCoerce a) ------------------------------------------------------------------ -- | 'Switch' is an instance of 'Reduce' for which __'reiterate'__s through the possibilities in a 'Which', -- delegating handling to 'Case', ensuring termination when 'Which' only contains one type. newtype Switch c (xs :: [Type]) r = Switch (c xs r) -- | 'trial0' each type in a 'Which', and either handle the 'case'' with value discovered, or __'reiterate'__ -- trying the next type in the type list. instance (Case c (x ': x' ': xs) r, Reduce (Which (x' ': xs)) (Switch c (x' ': xs)) r, Reiterate c (x : x' : xs)) => Reduce (Which (x ': x' ': xs)) (Switch c (x ': x' ': xs)) r where reduce (Switch c) v = case trial0 v of Right a -> case' c a Left v' -> reduce (Switch (reiterate c)) v' -- GHC compilation is SLOW if there is no pragma for recursive typeclass functions for different types -- Using INLINEABLE instead of NOLINE so that ghc 8.2.1 can optimize to single case statement -- See https://ghc.haskell.org/trac/ghc/ticket/12877 {-# INLINEABLE reduce #-} -- | Terminating case of the loop, ensuring that a instance of @Case '[]@ -- with an empty typelist is not required. -- You can't reduce 'impossible' instance (Case c '[x] r) => Reduce (Which '[x]) (Switch c '[x]) r where reduce (Switch c) v = case obvious v of a -> case' c a -- | Catamorphism for 'Which'. This is equivalent to @flip 'switch'@. which :: Reduce (Which xs) (Switch case' xs) r => case' xs r -> Which xs -> r which = reduce . Switch -- | A switch/case statement for 'Which'. This is equivalent to @flip 'which'@ -- -- Use 'Case' instances like 'Data.Diverse.Cases.Cases' to apply a 'Which' of functions to a variant of values. -- -- @ -- let y = 'Data.Diverse.Which.pick' (5 :: Int) :: 'Data.Diverse.Which.Which' '[Int, Bool] -- 'Data.Diverse.Which.switch' y ( -- 'Data.Diverse.Cases.cases' (show \@Bool -- 'Data.Diverse.Many../' show \@Int -- 'Data.Diverse.Many../' 'Data.Diverse.Many.nil')) \`shouldBe` "5" -- @ -- -- Or 'Data.Diverse.CaseTypeable.CaseTypeable' to apply a polymorphic function that work on all 'Typeables'. -- -- @ -- let y = 'Data.Diverse.Which.pick' (5 :: Int) :: 'Data.Diverse.Which.Which' '[Int, Bool] -- 'Data.Diverse.Which.switch' y ('CaseTypeable' (show . typeRep . (pure \@Proxy))) \`shouldBe` "Int" -- @ -- -- Or you may use your own custom instance of 'Case'. switch :: Reduce (Which xs) (Switch case' xs) r => Which xs -> case' xs r -> r switch = flip which ------------------------------------------------------------------ -- | 'SwitchN' is a variation of 'Switch' which __'reiterateN'__s through the possibilities in a 'Which', -- delegating work to 'CaseN', ensuring termination when 'Which' only contains one type. newtype SwitchN c (n :: Nat) (xs :: [Type]) r = SwitchN (c n xs r) -- | 'trial0' each type in a 'Which', and either handle the 'case'' with value discovered, or __'reiterateN'__ -- trying the next type in the type list. instance (Case (c n) (x ': x' ': xs) r, Reduce (Which (x' ': xs)) (SwitchN c (n + 1) (x' ': xs)) r, ReiterateN c n (x : x' : xs)) => Reduce (Which (x ': x' ': xs)) (SwitchN c n (x ': x' ': xs)) r where reduce (SwitchN c) v = case trial0 v of Right a -> case' c a Left v' -> reduce (SwitchN (reiterateN c)) v' -- GHC compilation is SLOW if there is no pragma for recursive typeclass functions for different types -- Using INLINEABLE instead of NOLINE so that ghc 8.2.1 can optimize to single case statement -- See https://ghc.haskell.org/trac/ghc/ticket/12877 {-# INLINEABLE reduce #-} -- | Terminating case of the loop, ensuring that a instance of @Case '[]@ -- with an empty typelist is not required. -- You can't reduce 'impossible' instance (Case (c n) '[x] r) => Reduce (Which '[x]) (SwitchN c n '[x]) r where reduce (SwitchN c) v = case obvious v of a -> case' c a -- | Catamorphism for 'Which'. This is equivalent to @flip 'switchN'@. whichN :: Reduce (Which xs) (SwitchN case' n xs) r => case' n xs r -> Which xs -> r whichN = reduce . SwitchN -- | A switch/case statement for 'Which'. This is equivalent to @flip 'whichN'@ -- -- Use 'Case' instances like 'Data.Diverse.Cases.CasesN' to apply a 'Which' of functions to a variant of values -- in index order. -- -- @ -- let y = 'pickN' \@0 Proxy (5 :: Int) :: 'Which' '[Int, Bool, Bool, Int] -- 'switchN' y ( -- 'Data.Diverse.Cases.casesN' (show \@Int -- 'Data.Diverse.Many../' show \@Bool -- 'Data.Diverse.Many../' show \@Bool -- 'Data.Diverse.Many../' show \@Int -- 'Data.Diverse.Many../' 'Data.Diverse.Many.nil')) \`shouldBe` "5" -- @ -- -- Or you may use your own custom instance of 'Case'. switchN :: Reduce (Which xs) (SwitchN case' n xs) r => Which xs -> case' n xs r -> r switchN = flip whichN ----------------------------------------------------------------- -- | Two 'Which'es are only equal iff they both contain the equivalnet value at the same type index. instance (Reduce (Which (x ': xs)) (Switch CaseEqWhich (x ': xs)) Bool) => Eq (Which (x ': xs)) where l@(Which i _) == (Which j u) = if i /= j then False else switch l (CaseEqWhich u) -- | @('impossible' == 'impossible') == True@ instance Eq (Which '[]) where _ == _ = True -- | Do not export constructor -- Stores the right Any to be compared when the correct type is discovered newtype CaseEqWhich (xs :: [Type]) r = CaseEqWhich Any instance Reiterate CaseEqWhich (x ': xs) where reiterate (CaseEqWhich r) = CaseEqWhich r instance (Eq x) => Case CaseEqWhich (x ': xs) Bool where case' (CaseEqWhich r) l = l == unsafeCoerce r ----------------------------------------------------------------- -- | A 'Which' with a type at smaller type index is considered smaller. instance ( Reduce (Which (x ': xs)) (Switch CaseEqWhich (x ': xs)) Bool , Reduce (Which (x ': xs)) (Switch CaseOrdWhich (x ': xs)) Ordering ) => Ord (Which (x ': xs)) where compare l@(Which i _) (Which j u) = if i /= j then compare i j else switch l (CaseOrdWhich u) -- | @('compare' 'impossible' 'impossible') == EQ@ instance Ord (Which '[]) where compare _ _ = EQ -- | Do not export constructor -- Stores the right Any to be compared when the correct type is discovered newtype CaseOrdWhich (xs :: [Type]) r = CaseOrdWhich Any instance Reiterate CaseOrdWhich (x ': xs) where reiterate (CaseOrdWhich r) = CaseOrdWhich r instance (Ord x) => Case CaseOrdWhich (x ': xs) Ordering where case' (CaseOrdWhich r) l = compare l (unsafeCoerce r) ------------------------------------------------------------------ -- | @show ('pick'' \'A') == "pick \'A'"@ instance (Reduce (Which (x ': xs)) (Switch CaseShowWhich (x ': xs)) ShowS) => Show (Which (x ': xs)) where showsPrec d v = showParen (d > app_prec) (which (CaseShowWhich 0) v) where app_prec = 10 -- | @read "impossible" == 'impossible'@ instance Show (Which '[]) where showsPrec d _ = showParen (d > app_prec) (showString "impossible") where app_prec = 10 newtype CaseShowWhich (xs :: [Type]) r = CaseShowWhich Int instance Reiterate CaseShowWhich (x ': xs) where reiterate (CaseShowWhich i) = CaseShowWhich (i + 1) instance Show x => Case CaseShowWhich (x ': xs) ShowS where case' (CaseShowWhich i) v = showString "pickN @" . showString (show i) . showString " Proxy " . showsPrec (app_prec + 1) v where app_prec = 10 ------------------------------------------------------------------ class WhichRead v where whichReadPrec :: Int -> Int -> ReadPrec v data Which_ (xs ::[Type]) = Which_ Int Any diversify0' :: forall x xs. Which_ xs -> Which_ (x ': xs) diversify0' = coerce readWhich_ :: forall x xs. Read x => Int -> Int -> ReadPrec (Which_ (x ': xs)) readWhich_ i j = guard (i == j) >> parens (prec app_prec $ (Which_ i . unsafeCoerce) <$> readPrec @x) where app_prec = 10 instance Read x => WhichRead (Which_ '[x]) where whichReadPrec = readWhich_ instance (Read x, WhichRead (Which_ (x' ': xs))) => WhichRead (Which_ (x ': x' ': xs)) where whichReadPrec i j = readWhich_ i j <|> (diversify0' <$> (whichReadPrec i (j + 1) :: ReadPrec (Which_ (x' ': xs)))) -- GHC compilation is SLOW if there is no pragma for recursive typeclass functions for different types -- Using INLINEABLE instead of NOLINE so that ghc 8.2.1 can optimize to single case statement -- See https://ghc.haskell.org/trac/ghc/ticket/12877 {-# INLINEABLE whichReadPrec #-} -- | This 'Read' instance tries to read using the each type in the typelist, using the first successful type read. instance WhichRead (Which_ (x ': xs)) => Read (Which (x ': xs)) where readPrec = parens $ prec app_prec $ do lift $ L.expect (Ident "pickN") lift $ L.expect (Punc "@") i <- lift L.readDecP lift $ L.expect (Ident "Proxy") Which_ n v <- whichReadPrec i 0 :: ReadPrec (Which_ (x ': xs)) pure $ Which n v where app_prec = 10 -- | @read "impossible" == 'impossible'@ instance Read (Which '[]) where readPrec = parens $ prec app_prec $ do lift $ L.expect (Ident "impossible") pure impossible where app_prec = 10