diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,12 @@ +Changelog +========= + +Version 0.1.0.0 +--------------- + +*October 26, 2018* + + + +* Initial release. + diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,81 @@ +# [lens-typelevel][] + +[![lens-typelevel on Hackage](https://img.shields.io/hackage/v/lens-typelevel.svg?maxAge=86400)](https://hackage.haskell.org/package/lens-typelevel) +[![Build Status](https://travis-ci.org/mstksg/lens-typelevel.svg?branch=master)](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"] +``` diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/lens-typelevel.cabal b/lens-typelevel.cabal new file mode 100644 --- /dev/null +++ b/lens-typelevel.cabal @@ -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 diff --git a/src/Data/Type/Lens.hs b/src/Data/Type/Lens.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Lens.hs @@ -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 + diff --git a/src/Data/Type/Lens/Example.hs b/src/Data/Type/Lens/Example.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Lens/Example.hs @@ -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_ diff --git a/src/Data/Type/Lens/Internal.hs b/src/Data/Type/Lens/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Lens/Internal.hs @@ -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