lens-typelevel (empty) → 0.1.0.0
raw patch · 8 files changed
+761/−0 lines, 8 filesdep +basedep +singletonssetup-changed
Dependencies added: base, singletons
Files
- CHANGELOG.md +12/−0
- LICENSE +30/−0
- README.md +81/−0
- Setup.hs +2/−0
- lens-typelevel.cabal +46/−0
- src/Data/Type/Lens.hs +380/−0
- src/Data/Type/Lens/Example.hs +112/−0
- src/Data/Type/Lens/Internal.hs +98/−0
+ CHANGELOG.md view
@@ -0,0 +1,12 @@+Changelog+=========++Version 0.1.0.0+---------------++*October 26, 2018*++<https://github.com/mstksg/lens-typelevel/releases/tag/v0.1.0.0>++* Initial release.+
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Justin Le (c) 2018++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Justin Le nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,81 @@+# [lens-typelevel][]++[](https://hackage.haskell.org/package/lens-typelevel)+[](https://travis-ci.org/mstksg/lens-typelevel)++van Laarhoven lenses at the type level using *[singletons][]* defunctionalization.++[lens-typelevel]: http://hackage.haskell.org/package/lens-typelevel+[singletons]: https://hackage.haskell.org/package/singletons++```haskell+ghci> :kind! '("hello", 6 ) & L1_ .~ 'True+'( 'True, 6 )++ghci> :kind! '("hello", 6 ) ^. L2_+6++ghci> :kind! '("hello", 6 ) ^. To_ SndSym0+6++ghci> :kind! '("hello", 'True ) & L2_ %~ NotSym0+'("hello", 'False )++ghci> :kind! '[ 'True, 'False, 'False ] & Traverse_ %~ NotSym0+'[ 'False, 'True, 'True ]++ghci> :kind! '("hello", '(6, 'False ) ) ^. L2_ .@ L1_+6++ghci> type TestList = '[ '("hello", 'True), '("world", 'False), '("curry", 'False)]+ghci> :kind! TestLst ^.. Traverse_ .@ L1_+'["hello", "world", "curry"]++ghci> :kind! '[] ^?! Traverse_+Error "Failed indexing into empty traversal"++ghci> :kind! '["hello", "world", "curry"] & IxList_ ('S 'Z) .~ "haskell"+'["hello", "haskell", "curry"]+```++It's pretty much the exact same representation as the *lens* library; it's+essentially an API-faithful port with the same representation and essentially+the same implementation. We even have `CloneLens_` and `CloneTraversal_`+implemented using type-level versions of `Context` and `Bazaar`:++```haskell+ghci> :kind! '("hello", 6) ^. CloneLens_ L1_+"hello"+```++Using prefix function names:++```haskell+ghci> :kind! Set L1_ 'True '("hello", 6 )+'( 'True, 6 )++ghci> :kind! View L2_ '("hello", 6 )+6++ghci> :kind! View (To_ SndSym0) '("hello", 6 )+6++ghci> :kind! Over L2_ NotSym0 '("hello", 'True )+'("hello", 'False )++ghci> :kind! Over Traverse_ NotSym0 '[ 'True, 'False, 'False ]+'[ 'False, 'True, 'True ]++ghci> :kind! View (L2_ .@ L1_) '("hello", '(6, 'False ) )+6++ghci> type TestList = '[ '("hello", 'True), '("world", 'False), '("curry", 'False)]+ghci> :kind! ToListOf (Traverse_ .@ L1_) TestList+'["hello", "world", "curry"]++ghci> :kind! UnsafePreview Traverse_ '[]+Error "Failed indexing into empty traversal"++ghci> :kind! Set (IxList_ ('S 'Z)) "haskell" '["hello", "world", "curry"]+'["hello", "haskell", "curry"]+```
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ lens-typelevel.cabal view
@@ -0,0 +1,46 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.31.0.+--+-- see: https://github.com/sol/hpack+--+-- hash: 32f70c034e55d2e4260473946cb22d88f640b361e30facad3d2b1c3fbcc524fe++name: lens-typelevel+version: 0.1.0.0+synopsis: Type-level lenses using singletons+description: Type-level lenses using singletons and its defunctionalization system,+ implemented using the same van Laarhoven encoding as the /lens/ package.+ See README for more information.+category: Dependent Types, Lenses+homepage: https://github.com/mstksg/lens-typelevel#readme+bug-reports: https://github.com/mstksg/lens-typelevel/issues+author: Justin Le+maintainer: justin@jle.im+copyright: (c) Justin Le 2018+license: BSD3+license-file: LICENSE+tested-with: GHC >= 8.6 && < 8.8+build-type: Simple+extra-source-files:+ README.md+ CHANGELOG.md++source-repository head+ type: git+ location: https://github.com/mstksg/lens-typelevel++library+ exposed-modules:+ Data.Type.Lens+ Data.Type.Lens.Example+ Data.Type.Lens.Internal+ other-modules:+ Paths_lens_typelevel+ hs-source-dirs:+ src+ ghc-options: -Wall -Wcompat+ build-depends:+ base >=4.12 && <5+ , singletons >=2.5+ default-language: Haskell2010
+ src/Data/Type/Lens.hs view
@@ -0,0 +1,380 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE UndecidableInstances #-}++-- |+-- Module : Data.Type.Lens+-- Copyright : (c) Justin Le 2018+-- License : BSD3+--+-- Maintainer : justin@jle.im+-- Stability : experimental+-- Portability : non-portable+--+-- Lenses and optics for manipulating DataKind-based types, powered by+-- /singletons/ defunctionalization.+--+-- See "Data.Type.Lens.Examples" for example usage and syntax.+--+-- For the most part, you should be able to use them just like you'd use+-- the functions from the /lens/ or /microlens/ libraries; just remember+-- to capitalize names like 'Over' and 'Set', since they are type families.+--+-- Note that the ways of "creating" a lens or optic ('Sets_', 'Traverse_',+-- 'To_', 'MkLens_', etc. are all suffixed with @_@ for convenience, to+-- reserve the underscoreless identifiers for the fully applied type family+-- as per /singletons/ library convention.+module Data.Type.Lens (+ LensLike, LensLike'+ -- * Setting+ , ASetter+ -- ** Using+ -- | Ways of consuming a setter.+ , Over, type (%~), sOver+ , Set, type (.~), sSet+ -- ** Making+ -- | Ways of creating a setter-only.+ , Sets_, Sets, sSets+ -- * Getting+ , Getting+ -- ** Using+ -- | Ways of consuming a getter+ , View, type (^.), sView+ -- ** Making+ -- | Ways of creating a getter-only.+ , To_, To, sTo+ -- * Lenses+ , ALens+ -- ** Making+ -- | Ways of creating a lens+ , MkLens_, MkLens, sMkLens+ -- ** Cloning+ , CloneLens_, CloneLens, sCloneLens+ -- * Traversals and Folds+ , ATraversal+ -- ** Using+ -- | Ways of consuming traversals and folds+ , Preview, type (^?), sPreview+ , ToListOf, type (^..), sToListOf+ , UnsafePreview, type (^?!), sUnsafePreview+ -- ** Making+ -- | Ways of creating traversals and folds+ , Folding_, Folding, sFolding+ , Folded_, Folded, sFolded+ , Traverse_, Traverse, sTraverse+ -- ** Cloning+ , CloneTraversal_, CloneTraversal, sCloneTraversal+ -- * Samples+ -- | Some sample lenses and traversals+ --+ -- ** Tuple+ , L1_, L1, sL1+ , L2_, L2, sL2+ -- ** List+ , N(..), SN+ , IxList_, IxList, sIxList+ -- * Util+ , type (.@)+ , Sing (SZ, SS, SMkContext)+ -- * Defunctionalization Symbols+ , ASetterSym0, ASetterSym1, ASetterSym2, ASetterSym3, ASetterSym4+ , OverSym0, OverSym1, OverSym2, OverSym3+ , SetSym0, SetSym1, SetSym2, SetSym3+ , SetsSym0, SetsSym1, SetsSym2, SetsSym3+ , GettingSym0, GettingSym1, GettingSym2, GettingSym3+ , ViewSym0, ViewSym1, ViewSym2+ , ToSym0, ToSym1, ToSym2, ToSym3+ , ToListOfSym0, ToListOfSym1, ToListOfSym2+ , LensLikeSym0, LensLikeSym1, LensLikeSym2, LensLikeSym3, LensLikeSym4, LensLikeSym5+ , LensLike'Sym0, LensLike'Sym1, LensLike'Sym2, LensLike'Sym3+ , MkLensSym0, MkLensSym1, MkLensSym2, MkLensSym3, MkLensSym4+ , CloneLensSym0, CloneLensSym1, CloneLensSym2, CloneLensSym3+ , FoldingSym0, FoldingSym1, FoldingSym2, FoldingSym3+ , FoldedSym0, FoldedSym1, FoldedSym2+ , L1Sym0, L1Sym1, L1Sym2+ , L2Sym0, L2Sym1, L2Sym2+ , ZSym0, SSym0, SSym1+ , IxListSym0, IxListSym1, IxListSym2, IxListSym3+ ) where++import Control.Applicative+import Data.Foldable+import Data.Functor.Identity+import Data.Monoid+import Data.Singletons.Prelude.Const+import Data.Singletons.Prelude.Foldable hiding (Traverse_)+import Data.Singletons.Prelude.Function hiding (Const, ConstSym0)+import Data.Singletons.Prelude.Functor+import Data.Singletons.Prelude.Identity+import Data.Singletons.Prelude.Maybe+import Data.Singletons.Prelude.Monoid+import Data.Singletons.TH+import Data.Type.Lens.Internal++-- | The general shape of optics in this library. ("van Laarhoven")+--+-- For different levels of polymorphism on @f@, you get different types of+-- optics:+--+-- * If @f@ can be any 'Functor', you have a Lens (see 'ALens')+-- * If @f@ is only 'Identity', you have a setter (see 'ASetter')+-- * If @f@ is only @'Const' R@ for a specific @R@, you have a getter+-- of @R@ (see 'Getting')+-- * If @f@ can be @'Const' r@ for any 'Monoid' @r@, you have a Fold.+-- * If @f@ can be any 'Applicative', you have a Traversal (see+-- 'ATraversal')+--+-- Normal lens libraries implement the constraints for lenses, folds, and+-- traversals using RankN types, but we don't do that here to avoid working+-- with RankN kinds.+type LensLike f s t a b = (a -> f b) -> (s -> f t)++-- | A 'LensLike' that does not change any types.+type LensLike' f s a = LensLike f s s a a++-- | A settable "lens". Usable with 'Over' ('%~'), constructable with 'To'+-- or any of the general lens constructors.+--+-- See 'LensLike' for more information.+type ASetter s t a b = LensLike Identity s t a b++-- | A retrieving "lens". If @r@ is fixed to a type, it's a Getter for+-- that type. If @r@ is polymorphic over all 'Monoid', then it's a Fold+-- over @a@s.+--+-- As a Getter, usable with 'View' ('^.'); as a Fold, usable with+-- 'ToListOf' ('^..'), 'Preview' ('^?'), etc.+--+-- Normal lens libraries implement the constraints for folds using RankN+-- types, but we don't do that here to avoid working with RankN kinds.+--+-- See 'LensLike' for more information.+type Getting r s a = LensLike (Const r) s s a a++-- | Peano nats, used for implementation of list index traversals in+-- a termination-sane way.+data N = Z | S N++genSingletons [''LensLike, ''LensLike', ''ASetter, ''Getting, ''N]++-- | If a function expects an 'ALens', it can be given any Lens (a+-- @'LensLike' f@ that works for any 'Functor' f).+--+-- You can use an 'ALens' as a normal lens by using 'CloneLens_'.+type ALens s t a b = LensLike (Context a b) s t a b++-- | If a function expects an 'ATraversal', it can be given any Traversal+-- (a @'LensLike' f@ that works for any 'Applicative' f).+--+-- You can use an 'ATraversal' as a normal traversal by using+-- 'CloneTraversal_'.+type ATraversal s t a b = LensLike (Bazaar a b) s t a b++$(singletonsOnly [d|+ over :: ASetter s t a b -> (a -> b) -> (s -> t)+ over l f x = case l (Identity . f) x of+ Identity y -> y++ set :: ASetter s t a b -> b -> s -> t+ set l y = over l (\_ -> y)++ view :: Getting a s a -> s -> a+ view l x = case l Const x of+ Const y -> y++ sets :: ((a -> b) -> (s -> t)) -> ASetter s t a b+ sets f g = Identity . f (\x -> case g x of Identity y -> y)++ to :: (s -> a) -> Getting r s a+ to f g x = case g (f x) of+ Const y -> Const y++ mkLens+ :: Functor f+ => (s -> a)+ -> (s -> b -> t)+ -> LensLike f s t a b+ mkLens v s f x = s x <$> f (v x)++ cloneLens+ :: Functor f+ => LensLike (Context a b) s t a b+ -> LensLike f s t a b+ cloneLens l f x = case l (\y -> MkContext id y) x of+ MkContext g y -> g <$> f y++ toListOf :: Getting [a] s a -> s -> [a]+ toListOf l x = case l (Const . (:[])) x of+ Const ys -> ys++ preview :: Getting (First a) s a -> s -> Maybe a+ preview l x = case l (Const . First . Just) x of+ Const (First y) -> y++ unsafePreview :: Getting (First a) s a -> s -> a+ unsafePreview l x = case preview l x of+ Just y -> y+ Nothing -> error "Failed indexing into empty traversal"++ folding :: (Foldable f, Monoid r) => (s -> f a) -> Getting r s a+ folding f g x = case traverse_ g (f x) of+ Const y -> Const y++ folded :: (Foldable f, Monoid r) => Getting r (f a) a+ folded f x = case traverse_ f x of+ Const y -> Const y++ cloneTraversal+ :: Applicative f+ => LensLike (Bazaar a b) s t a b+ -> LensLike f s t a b+ cloneTraversal l f xs = unBazaar f $ l (`More` Done id) xs++ l1 :: Functor f => LensLike f (a, c) (b, c) a b+ l1 f (x, y) = (\x' -> (x', y)) <$> f x++ l2 :: Functor f => LensLike f (a, b) (a, c) b c+ l2 f (x, y) = (\y' -> (x, y')) <$> f y++ ixList :: Applicative f => N -> LensLike' f [a] a+ ixList _ _ [] = pure []+ ixList Z f (x:xs) = (:xs) <$> f x+ ixList (S i) f (x:xs) = (x:) <$> ixList i f xs+ |])++-- | Infix application of 'Over'+type l %~ f = OverSym2 l f++-- | Infix application of 'Set'+type l .~ x = SetSym2 l x++-- | Infix application of 'View'+type x ^. l = View l x++-- | Infix application of 'Preview'+type x ^? l = Preview l x++-- | Infix application of 'UnsafePreview'+type x ^?! l = UnsafePreview l x++-- | Infix application of 'ToListOf'+type x ^.. l = ToListOf l x++-- | Shorter name for type-level function composition+type f .@ g = f .@#@$$$ g++infixr 4 %~+infixr 4 .~+infixl 8 ^.+infixl 8 ^?+infixl 8 ^?!+infixl 8 ^..+infixr 9 .@++-- | Create a Getter from a getting function.+--+-- @+-- 'To_' :: (a ~> b) -> 'Getting' b a b+-- @+type To_ f = ToSym1 f++-- | Create a Setter from a setting function.+--+-- @+-- 'Sets_' :: ((a ~> b) ~> (s ~> t)) -> 'ASetter' s t a b+-- @+type Sets_ f = SetsSym1 f++-- | Create a Lens from a setter and a getter.+--+-- @+-- 'MkLens_'+-- :: 'Functor' f+-- => (s ~> a)+-- -> (s ~> b ~> t)+-- -> 'LensLike' f s t a b+-- @+type MkLens_ f g = MkLensSym2 f g++-- | "Clone" a polymorphic lens so it can be used as more than one type of+-- thing (getter or setter).+--+-- @+-- 'CloneLens_'+-- :: 'Functor' f+-- => 'LensLike' (Context a b) s t a b+-- -> 'LensLike' f s t a b+-- @+--+-- Useful for writing a function that takes a lens and uses it in more than+-- one way; if you have it take an 'ALens', you can then use 'CloneLens_' to+-- use it as a getter or setter.+type CloneLens_ l = CloneLensSym1 l++-- | "Clone" a polymorphic traversal so it can be used as more than one type of+-- thing (fold, traversal, getter, setter...).+--+-- @+-- 'CloneTraversal_'+-- :: 'Functor' f+-- => 'LensLike' (Bazaar a b) s t a b+-- -> 'LensLike' f s t a b+-- @+--+-- Useful for writing a function that takes a traversal and uses it in more+-- than one way; if you have it take an 'ATraversal', you can then use+-- 'CloneTraversal_' to use it as a fold or traversal or anything else.+type CloneTraversal_ l = CloneTraversalSym1 l++-- | The canonical Traversal for any instance of 'Traversable'.+--+-- @+-- 'Traverse_'+-- :: 'Applicative' f+-- => 'LensLike' f (t a) (t b) a b+-- @+type Traverse_ = TraverseSym0++-- | Create a Fold from a "folding function":+--+-- @+-- 'Folding_'+-- :: ('Foldable' f, 'Monoid' r)+-- => (s ~> f a)+-- -> 'Getting' r s a+-- @+type Folding_ f = FoldingSym1 f++-- | The canonical Fold for any instance of 'Foldable'.+--+-- @+-- 'Folded_'+-- :: 'Monoid' r+-- => 'Getting' r (t a) a+-- @+type Folded_ = FoldedSym0++-- | Lens into the first field of a tuple+type L1_ = L1Sym0++-- | Lens into the second field of a tuple+type L2_ = L2Sym0++-- | @'IxList' i@ is a Traversal into the i-th item into a list. Defined+-- in terms of 'N' to allow for sane termination guaruntees.+--+-- @+-- 'IxList_'+-- :: 'Applicative' f+-- => 'N'+-- -> 'LensLike'' f [a] a+-- @+type IxList_ i = IxListSym1 i+
+ src/Data/Type/Lens/Example.hs view
@@ -0,0 +1,112 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeOperators #-}++-- |+-- Module : Data.Type.Lens.Example+-- Copyright : (c) Justin Le 2018+-- License : BSD3+--+-- Maintainer : justin@jle.im+-- Stability : experimental+-- Portability : non-portable+--+-- See source for examples of using type-level lenses from+-- "Data.Type.Lens".+module Data.Type.Lens.Example (+ -- * Prefix functions+ SetExample+ , ViewExample+ , ToExample+ , OverExample+ , TraversalExample+ , NestedExample+ , FoldExample+ , UnsafeExample+ , IxExample+ , CloneExample+ -- * Operators+ , SetExample'+ , ViewExample'+ , ToExample'+ , OverExample'+ , TraversalExample'+ , NestedExample'+ , FoldExample'+ , IxExample'+ , UnsafeExample'+ , CloneExample'+ ) where++import Data.Singletons.Prelude+import Data.Singletons.Prelude.Function+import Data.Type.Lens++-- |+-- >>> :kind! SetExample+-- '( 'True, 6 )+type SetExample = Set L1_ 'True '("hello", 6 )++-- |+-- >>> :kind! ViewExample+-- 6+type ViewExample = View L2_ '("hello", 6 )++-- |+-- >>> :kind! ToExample+-- 6+type ToExample = View (To_ SndSym0) '("hello", 6 )++-- |+-- >>> :kind! TraversalExample+-- '( "hello", 'False )+type OverExample = Over L2_ NotSym0 '("hello", 'True )++-- |+-- >>> :kind! TraversalExample+-- '[ 'False, 'True, 'True ]+type TraversalExample = Over Traverse_ NotSym0 '[ 'True, 'False, 'False ]++-- |+-- >>> :kind! NestedExample+-- 6+type NestedExample = View (L2_ .@ L1_) '("hello", '(6, 'False ) )++-- |+-- >>> :kind! FoldExample+-- '["hello", "world", "curry"]+type FoldExample = ToListOf (Traverse_ .@ L1_)+ '[ '("hello", 'True )+ , '("world", 'False)+ , '("curry", 'False)+ ]++-- |+-- >>> :kind! UnsafeExample+-- Error "Failed indexing into empty traversal"+type UnsafeExample = UnsafePreview Traverse_ '[]++-- |+-- >>> :kind! IxExample+-- '["hello", "haskell", "curry"]+type IxExample = Set (IxList_ ('S 'Z)) "haskell"+ '["hello", "world", "curry"]++-- |+-- >>> :kind! CloneExample+-- "hello"+type CloneExample = View (CloneLens_ L1_) '("hello", 6 )+++type SetExample' = '("hello", 6 ) & L1_ .~ 'True+type ViewExample' = '("hello", 6 ) ^. L2_+type ToExample' = '("hello", 6 ) ^. To_ SndSym0+type OverExample' = '("hello", 'True ) & L2_ %~ NotSym0+type TraversalExample' = '[ 'True, 'False, 'False ] & Traverse_ %~ NotSym0+type NestedExample' = '("hello", '(6, 'False ) ) ^. L2_ .@ L1_+type FoldExample' = '[ '("hello", 'True )+ , '("world", 'False)+ , '("curry", 'False)+ ] ^.. Traverse_ .@ L1_+type UnsafeExample' = '[] ^?! Traverse_+type IxExample' = '["hello","world","curry"] & IxList_ ('S 'Z) .~ "haskell"+type CloneExample' = '("hello", 6 ) ^. CloneLens_ L1_
+ src/Data/Type/Lens/Internal.hs view
@@ -0,0 +1,98 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE UndecidableInstances #-}++module Data.Type.Lens.Internal (+ Context(..)+ , Bazaar(..)+ , UnBazaar, sUnBazaar+ , Sing (SMkContext, SDone, SMore)+ -- * Defunctionalization Symbols+ , MkContextSym0, MkContextSym1, MkContextSym2+ , DoneSym0, DoneSym1, MoreSym0, MoreSym1, MoreSym2+ , UnBazaarSym0, UnBazaarSym1, UnBazaarSym2+ ) where++import Data.Kind+import Data.Singletons.Prelude.Const+import Data.Singletons.Prelude.Function hiding (Const, ConstSym0)+import Data.Singletons.Prelude.Functor+import Data.Singletons.TH++-- | A partially applied lens+data Context a b t = MkContext (b ~> t) a++type MkContextSym0 = TyCon2 'MkContext+type MkContextSym1 f = TyCon1 ('MkContext f)+type MkContextSym2 f x = 'MkContext f x++data instance Sing :: forall a b t. Context a b t -> Type where+ SMkContext+ :: Sing f+ -> Sing x+ -> Sing ('MkContext f x)++$(singletonsOnly [d|+ fmapContext :: (t -> q) -> Context a b t -> Context a b q+ fmapContext f (MkContext g x) = MkContext (f . g) x+ |])++instance PFunctor (Context a b) where+ type Fmap f c = FmapContext f c++instance SFunctor (Context a b) where+ sFmap = sFmapContext++-- | A partially applied traversal+data Bazaar a b t = Done t+ | More a (Bazaar a b (b ~> t))++type DoneSym0 = TyCon1 'Done+type DoneSym1 x = 'Done x++type MoreSym0 = TyCon2 'More+type MoreSym1 x = TyCon1 ('More x)+type MoreSym2 x b = 'More x b++data instance Sing :: forall a b t. Bazaar a b t -> Type where+ SDone :: Sing x -> Sing ('Done x)+ SMore :: Sing x -> Sing b -> Sing ('More x b)++$(singletonsOnly [d|+ fmapBazaar :: (t -> q) -> Bazaar a b t -> Bazaar a b q+ fmapBazaar f (Done t ) = Done (f t)+ fmapBazaar f (More x b) = More x (fmapBazaar (f .) b)++ pureBazaar :: t -> Bazaar a b t+ pureBazaar = Done++ liftA2Bazaar :: (t -> r -> s) -> Bazaar a b t -> Bazaar a b r -> Bazaar a b s+ liftA2Bazaar f (Done x ) c = fmapBazaar (f x) c+ liftA2Bazaar f (More x b) c = More x (liftA2Bazaar (\g r y -> f (g y) r) b c)++ unBazaar :: Applicative f => (a -> f b) -> Bazaar a b t -> f t+ unBazaar _ (Done x ) = pure x+ unBazaar f (More x b) = liftA2 (&) (f x) (unBazaar f b)+ |])++instance PFunctor (Bazaar a b) where+ type Fmap f c = FmapBazaar f c++instance SFunctor (Bazaar a b) where+ sFmap = sFmapBazaar++instance PApplicative (Bazaar a b) where+ type Pure x = PureBazaar x+ type LiftA2 f x y = LiftA2Bazaar f x y++instance SApplicative (Bazaar a b) where+ sPure = sPureBazaar+ sLiftA2 = sLiftA2Bazaar