git.iko.soy/generic-lens
on master help sign in
Optimise positional lens and use ghc-proofs for testing
3fddfc5Csongor Kiss
generic-lens.cabal+5−2
compare with master
unifiedsplit
@@ -41,6 +41,10 @@ library
41 , Data.Generics.Sum.Internal.Typed
41 , Data.Generics.Sum.Internal.Typed
42 , Data.Generics.Sum.Internal.Subtype
42 , Data.Generics.Sum.Internal.Subtype
43
43
44+ , Data.Generics.Internal.Families
45+ , Data.Generics.Internal.Families.Count
46+ , Data.Generics.Internal.Families.Has
47+ , Data.Generics.Internal.HList
44 , Data.Generics.Product.Internal.Fields
48 , Data.Generics.Product.Internal.Fields
45 , Data.Generics.Product.Internal.Positions
49 , Data.Generics.Product.Internal.Positions
46 , Data.Generics.Product.Internal.Subtype
50 , Data.Generics.Product.Internal.Subtype
@@ -63,9 +67,8 @@ test-suite generic-lens-test
63 main-is: Spec.hs
67 main-is: Spec.hs
64
68
65 build-depends: base >= 4.9 && <= 5.0
69 build-depends: base >= 4.9 && <= 5.0
66− , QuickCheck
67− , hspec
68 , generic-lens
70 , generic-lens
71+ , ghc-proofs >= 0.1.1
69
72
70 default-language: Haskell2010
73 default-language: Haskell2010
71 ghc-options: -Wall
74 ghc-options: -Wall
src/Data/Generics/Product/Positions.hs+1−1
@@ -93,7 +93,7 @@ instance
93 , GHasPosition 1 i (Rep s) a
93 , GHasPosition 1 i (Rep s) a
94 ) => HasPosition i a s where
94 ) => HasPosition i a s where
95
95
96− position = repIso . gposition @1 @i
96+ position = ravel (repIso . gposition @1 @i)
97
97
98type family ErrorUnless (i :: Nat) (s :: Type) (hasP :: Bool) :: Constraint where
98type family ErrorUnless (i :: Nat) (s :: Type) (hasP :: Bool) :: Constraint where
99 ErrorUnless i s 'False
99 ErrorUnless i s 'False
stack.yaml+3−3
@@ -1,10 +1,10 @@
1−
2−resolver: lts-8.17
1+resolver: nightly-2017-09-06
3
2
4packages:
3packages:
5- '.'
4- '.'
6
5
7−extra-deps: []
6+extra-deps:
7+- 'ghc-proofs-0.1.1'
8
8
9flags: {}
9flags: {}
10
10
test/Spec.hs+57−1
@@ -1 +1,57 @@
1−{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
1+{-# OPTIONS_GHC -O -fplugin GHC.Proof.Plugin #-}
2+
3+{-# LANGUAGE AllowAmbiguousTypes #-}
4+{-# LANGUAGE DataKinds #-}
5+{-# LANGUAGE DeriveGeneric #-}
6+{-# LANGUAGE DuplicateRecordFields #-}
7+{-# LANGUAGE ExistentialQuantification #-}
8+{-# LANGUAGE RankNTypes #-}
9+{-# LANGUAGE ScopedTypeVariables #-}
10+{-# LANGUAGE TypeApplications #-}
11+
12+module Main where
13+
14+import GHC.Generics
15+import Data.Generics.Product
16+import GHC.Proof
17+
18+main :: IO ()
19+main = putStrLn "Hello world"
20+
21+data Record = MkRecord
22+ { fieldA :: Int
23+ , fieldB :: Bool
24+ } deriving Generic
25+
26+data Record2 = MkRecord2
27+ { fieldA :: Int
28+ } deriving Generic
29+
30+type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s
31+
32+fieldALensManual :: Lens' Record Int
33+fieldALensManual f (MkRecord a b) = (\a' -> MkRecord a' b) <$> f a
34+
35+newtype L s a = L (Lens' s a)
36+
37+subtypeLensManual :: Lens' Record Record2
38+subtypeLensManual f record
39+ = fmap (\ds -> case record of
40+ MkRecord _ b -> MkRecord (case ds of {MkRecord2 g1 -> g1}) b
41+ ) (f (MkRecord2 (case record of {MkRecord a _ -> a})))
42+
43+--------------------------------------------------------------------------------
44+-- * Tests
45+-- The ghc-proofs plugin checks that the following equalities hold, by checking
46+-- that the LHSs and the RHSs are CSEd. This also means that the runtime
47+-- characteristics of the derived lenses is the same as the manually written
48+-- ones above.
49+
50+fieldP :: Proof
51+fieldP = L fieldALensManual === L (field @"fieldA")
52+
53+posP :: Proof
54+posP = L fieldALensManual === L (position @1)
55+
56+subtypeP :: Proof
57+subtypeP = L subtypeLensManual === L super