diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -14,6 +14,9 @@ # Changelog +* 4.5.0.0 + - Replaced usages of `KnownNat` with a new `NatToInt` class to avoid inefficient Integer https://github.com/louispan/data-diverse/issues/8. + * 4.4.0.0 - Renamed `Unconstrained` to `C0`. Added `C2`, `C3`, `C4`, `C5`, `C6`. diff --git a/data-diverse.cabal b/data-diverse.cabal --- a/data-diverse.cabal +++ b/data-diverse.cabal @@ -1,5 +1,5 @@ name: data-diverse -version: 4.4.0.0 +version: 4.5.0.0 synopsis: Extensible records and polymorphic variants. description: "Data.Diverse.Many" is an extensible record for any size encoded efficiently as (Seq Any). "Data.Diverse.Which" is a polymorphic variant of possibilities encoded as (Int, Any). diff --git a/src/Data/Diverse/Many/Internal.hs b/src/Data/Diverse/Many/Internal.hs --- a/src/Data/Diverse/Many/Internal.hs +++ b/src/Data/Diverse/Many/Internal.hs @@ -327,7 +327,7 @@ => Many xs -> y -> Many (SnocUnique xs y) snocMany'(Many ls) y = if i /= 0 then Many ls else Many (ls S.|> unsafeCoerce y) where - i = fromInteger (natVal @(PositionOf y xs) Proxy) :: Int + i = natToInt @(PositionOf y xs) :: Int infixl 5 `snocMany'` -- | Infix version of 'snocMany'. @@ -418,9 +418,9 @@ grab :: forall x xs. UniqueMember x xs => Many xs -> x grab (Many xs) = unsafeCoerce $ grab_ @(IndexOf x xs) xs -grab_ :: forall n. KnownNat n => S.Seq Any -> Any +grab_ :: forall n. NatToInt n => S.Seq Any -> Any grab_ xs = let !x = S.index xs i in x -- forcing x to avoid storing Seq in thunk - where i = fromInteger (natVal @n Proxy) + where i = natToInt @n -------------------------------------------------- @@ -464,9 +464,9 @@ replace' :: forall x xs. UniqueMember x xs => Many xs -> x -> Many xs replace' (Many xs) x = Many $ replace_ @(IndexOf x xs) xs (unsafeCoerce x) -replace_ :: forall n. KnownNat n => S.Seq Any -> Any -> S.Seq Any +replace_ :: forall n. NatToInt n => S.Seq Any -> Any -> S.Seq Any replace_ xs x = S.update i x xs - where i = fromInteger (natVal @n Proxy) + where i = natToInt @n -- | Polymorphic setter by unique type. Set the field with type @x@, and replace with type @y@ -- @@ -768,7 +768,7 @@ 0 -> Nothing i' -> Just (i' - 1, WrappedAny v) where - i = fromInteger (natVal @(PositionOf x smaller) Proxy) + i = natToInt @(PositionOf x smaller) ----------------------------------------------------------------------- @@ -832,7 +832,7 @@ 0 -> Nothing i' -> Just (i' - 1, WrappedAny v) where - i = fromInteger (natVal @n' Proxy) + i = natToInt @n' ----------------------------------------------------------------------- @@ -864,7 +864,7 @@ CaseAny (CaseAmend' larger (Int, WrappedAny)) (x ': xs) where caseAny _ v = (i, WrappedAny v) where - i = fromInteger (natVal @(IndexOf x larger) Proxy) + i = natToInt @(IndexOf x larger) ----------------------------------------------------------------------- @@ -916,7 +916,7 @@ CaseAny (CaseAmend larger (Int, WrappedAny)) ((x, y) ': zs) where caseAny _ v = (i, WrappedAny v) where - i = fromInteger (natVal @(IndexOf x larger) Proxy) + i = natToInt @(IndexOf x larger) ----------------------------------------------------------------------- @@ -982,7 +982,7 @@ CaseAny (CaseAmendN' indices larger (Int, WrappedAny) n) (x ': xs) where caseAny _ v = (i, WrappedAny v) where - i = fromInteger (natVal @n' Proxy) + i = natToInt @n' ----------------------------------------------------------------------- @@ -1015,7 +1015,7 @@ CaseAny (CaseAmendN indices larger (Int, WrappedAny) n) ((x, y) ': zs) where caseAny _ v = (i, WrappedAny v) where - i = fromInteger (natVal @n' Proxy) + i = natToInt @n' ----------------------------------------------------------------------- diff --git a/src/Data/Diverse/TypeLevel.hs b/src/Data/Diverse/TypeLevel.hs --- a/src/Data/Diverse/TypeLevel.hs +++ b/src/Data/Diverse/TypeLevel.hs @@ -1,9 +1,12 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} @@ -16,25 +19,40 @@ import Data.Kind import GHC.TypeLits --- | Ensures that @x@ is a unique member of @xs@, and that 'natVal' can be used. -type UniqueMember x xs = (Unique x xs, KnownNat (IndexOf x xs)) +-- | Produce a runtime 'Int' value corresponding to a 'Nat' type. +-- Based on https://github.com/VinylRecords/Vinyl/blob/a5ffd10fbc747c5366ae9806e61bf45f78c3eb33/Data/Vinyl/TypeLevel.hs +-- This is used instead of 'KnownNat' because to avoid inefficient 'Integer' https://github.com/louispan/data-diverse/issues/8 +-- AllowsAmbiguousTypes! Uses @TypeApplication@ instead of 'Proxy' +class NatToInt (n :: Nat) where + natToInt :: Int +instance {-# OVERLAPPING #-} NatToInt 0 where + natToInt = 0 + {-# INLINE natToInt #-} + +instance {-# OVERLAPPABLE #-} (NatToInt m, n ~ (m + 1)) => NatToInt n where + natToInt = 1 + natToInt @m + {-# INLINE natToInt #-} + +-- | Ensures that @x@ is a unique member of @xs@, and that 'natToInt' can be used. +type UniqueMember x xs = (Unique x xs, NatToInt (IndexOf x xs)) + -- | Every x in @xs@ is a `UniqueMember x ys` type family UniqueMembers (xs :: [k]) (ys :: [k]) :: Constraint where UniqueMembers '[] ys = () UniqueMembers (x ': xs) ys = (UniqueMember x ys, UniqueMembers xs ys) --- | Ensures that @x@ is a unique member of @xs@, and that 'natVal' can be used. -type UniqueLabelMember l xs = (UniqueLabel l xs, KnownNat (IndexOf (KindAtLabel l xs) xs)) +-- | Ensures that @x@ is a unique member of @xs@, and that 'natToInt' can be used. +type UniqueLabelMember l xs = (UniqueLabel l xs, NatToInt (IndexOf (KindAtLabel l xs) xs)) --- | Ensures that @x@ is a unique member of @xs@ if it exists, and that 'natVal' can be used. -type MaybeUniqueMember x xs = (Unique x xs, KnownNat (PositionOf x xs)) +-- | Ensures that @x@ is a unique member of @xs@ if it exists, and that 'natToInt' can be used. +type MaybeUniqueMember x xs = (Unique x xs, NatToInt (PositionOf x xs)) --- | Ensures that @x@ is a member of @xs@ at @n@, and that 'natVal' can be used. -type MemberAt n x xs = (KnownNat n, x ~ KindAtIndex n xs) +-- | Ensures that @x@ is a member of @xs@ at @n@, and that 'natToInt' can be used. +type MemberAt n x xs = (NatToInt n, x ~ KindAtIndex n xs) --- | Ensures that @x@ is a member of @xs@ at @n@ if it exists, and that 'natVal' can be used. -type MaybeMemberAt n x xs = (KnownNat n, KindAtPositionIs n x xs) +-- | Ensures that @x@ is a member of @xs@ at @n@ if it exists, and that 'natToInt' can be used. +type MaybeMemberAt n x xs = (NatToInt n, KindAtPositionIs n x xs) -- | Snoc @x@ to end of @xs@ if @x@ doesn't already exist in @xs@ type family SnocUnique (xs :: [k]) (x :: k) :: [k] where diff --git a/src/Data/Diverse/Which/Internal.hs b/src/Data/Diverse/Which/Internal.hs --- a/src/Data/Diverse/Which/Internal.hs +++ b/src/Data/Diverse/Which/Internal.hs @@ -93,7 +93,6 @@ import Data.Diverse.Reiterate import Data.Diverse.TypeLevel import Data.Kind -import Data.Proxy import Data.Semigroup (Semigroup(..)) import Data.Tagged import Data.Void @@ -204,8 +203,8 @@ pick :: forall x xs. 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 +pick_ :: forall x xs n. (NatToInt n, n ~ IndexOf x xs) => x -> Which xs +pick_ = Which (natToInt @n) . unsafeCoerce -- | A variation of 'pick' where @x@ is specified via a label -- @@ -245,7 +244,7 @@ -- 'pickN' \@4 (5 :: Int) :: Which '[Bool, Int, Char, Bool, Int, Char] -- @ pickN :: forall n x xs. MemberAt n x xs => x -> Which xs -pickN = Which (fromInteger (natVal @n Proxy)) . unsafeCoerce +pickN = Which (natToInt @n) . unsafeCoerce -- | It is 'obvious' what value is inside a 'Which' of one type. -- @@ -258,9 +257,9 @@ trial_ :: forall n x xs. - (KnownNat n, n ~ IndexOf x xs) + (NatToInt n, n ~ IndexOf x xs) => Which xs -> Either (Which (Remove x xs)) x -trial_ (Which n v) = let i = fromInteger (natVal @n Proxy) +trial_ (Which n v) = let i = natToInt @n in if n == i then Right (unsafeCoerce v) else if n > i @@ -277,7 +276,7 @@ :: forall n x xs. (MemberAt n x xs) => Which xs -> Either (Which (RemoveIndex n xs)) x -trialN (Which n v) = let i = fromInteger (natVal @n Proxy) +trialN (Which n v) = let i = natToInt @n in if n == i then Right (unsafeCoerce v) else if n > i @@ -314,9 +313,9 @@ trial_' :: forall n x xs. - (KnownNat n, n ~ IndexOf x xs) + (NatToInt n, n ~ IndexOf x xs) => Which xs -> Maybe x -trial_' (Which n v) = let i = fromInteger (natVal @n Proxy) +trial_' (Which n v) = let i = natToInt @n in if n == i then Just (unsafeCoerce v) else Nothing @@ -333,7 +332,7 @@ :: forall n x xs. (MemberAt n x xs) => Which xs -> Maybe x -trialN' (Which n v) = let i = fromInteger (natVal @n Proxy) +trialN' (Which n v) = let i = natToInt @n in if n == i then Just (unsafeCoerce v) else Nothing @@ -516,8 +515,8 @@ ) => Case (CaseReinterpret branch tree (Either (Which comp) (Which branch))) (x ': tree') where case' CaseReinterpret a = - case fromInteger (natVal @(PositionOf x branch) Proxy) of - 0 -> let j = fromInteger (natVal @(PositionOf x comp) Proxy) + case natToInt @(PositionOf x branch) of + 0 -> let j = natToInt @(PositionOf x comp) -- 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) @@ -544,7 +543,7 @@ ) => Case (CaseReinterpret' branch tree (Maybe (Which branch))) (x ': tree') where case' CaseReinterpret' a = - case fromInteger (natVal @(PositionOf x branch) Proxy) of + case natToInt @(PositionOf x branch) of 0 -> Nothing i -> Just $ Which (i - 1) (unsafeCoerce a) @@ -621,7 +620,7 @@ instance (MaybeMemberAt n' x branch, n' ~ PositionOf n indices) => Case (CaseReinterpretN' indices (Maybe (Which branch)) n) (x ': tree) where case' CaseReinterpretN' a = - case fromInteger (natVal @n' Proxy) of + case natToInt @n' of 0 -> Nothing i -> Just $ Which (i - 1) (unsafeCoerce a) diff --git a/test/Data/Diverse/ManySpec.hs b/test/Data/Diverse/ManySpec.hs --- a/test/Data/Diverse/ManySpec.hs +++ b/test/Data/Diverse/ManySpec.hs @@ -35,7 +35,7 @@ -- it "Test user friendly compile errors" $ do -- let y = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nil -- -- ghc 8.0.2: IndexOf error: ‘Maybe Bool’ is not a member of ... - -- -- ghc 8.0.1 has terrible error message: "No instance for (GHC.TypeLits.KnownNat" + -- -- ghc 8.0.1 has terrible error message: "No instance for NatToInt" -- grab @(Maybe Bool) y `shouldBe` (Just False) -- -- Not unique error: ‘Maybe Char’ is a duplicate in ... diff --git a/test/Data/Diverse/TypeSpec.hs b/test/Data/Diverse/TypeSpec.hs --- a/test/Data/Diverse/TypeSpec.hs +++ b/test/Data/Diverse/TypeSpec.hs @@ -10,7 +10,6 @@ import Data.Diverse import Data.Typeable -import GHC.TypeLits import Test.Hspec -- `main` is here so that this module can be run from GHCi on its own. It is @@ -22,11 +21,11 @@ spec = do describe "TypeLevel" $ do it "PositionOf" $ do - fromIntegral (natVal @(PositionOf String '[Bool, Int]) Proxy) `shouldBe` (0 :: Int) - fromIntegral (natVal @(PositionOf Bool '[Bool, Int]) Proxy) `shouldBe` (1 :: Int) - fromIntegral (natVal @(PositionOf Int '[Bool, Int]) Proxy) `shouldBe` (2 :: Int) - fromIntegral (natVal @(PositionOf Int '[Bool, Int, Char]) Proxy) `shouldBe` (2 :: Int) - fromIntegral (natVal @(PositionOf Int '[Bool, String, Char]) Proxy) `shouldBe` (0 :: Int) + natToInt @(PositionOf String '[Bool, Int]) `shouldBe` (0 :: Int) + natToInt @(PositionOf Bool '[Bool, Int]) `shouldBe` (1 :: Int) + natToInt @(PositionOf Int '[Bool, Int]) `shouldBe` (2 :: Int) + natToInt @(PositionOf Int '[Bool, Int, Char]) `shouldBe` (2 :: Int) + natToInt @(PositionOf Int '[Bool, String, Char]) `shouldBe` (0 :: Int) it "ComplementOf" $ do let complementTest :: Proxy xs -> Proxy ys -> Proxy (Complement xs ys) -> Proxy (Complement xs ys)