lens-typelevel alternatives and similar packages
Based on the "Dependent Types" category.
Alternatively, view lens-typelevel alternatives based on common mentions on social networks and blogs.
-
agda-snippets-hakyll
Library and tool to render the snippets in literate Agda files to hyperlinked HTML, leaving the rest of the text untouched.
SaaSHub - Software Alternatives and Reviews
Do you think we are missing an alternative of lens-typelevel or a related project?
README
lens-typelevel
(Rendered off-hackage documentation)
van Laarhoven lenses at the type level using singletons defunctionalization.
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
:
ghci> type CloneExample l = ('( 'True, 'False ) & CloneLens_ l %~ NotSym0)
^. CloneLens_ l
ghci> :kind! CloneExample L1_
'False
ghci> :kind! CloneExample L2_
'True
Using prefix function names:
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"]
Defining lenses
There are two main ways to define optics.
First, you can write them by hand using singletonsOnly
:
$(singletonsOnly [d|
l1 :: Functor f => LensLike (a, c) (b, c) a b
l1 f (x, y) = (\x' -> (x', y)) <$> f x
l1Alt :: Functor f => LensLike (a, c) (b, c) a b
l1Alt = mkLens fst (\(_, y) x -> (x', y))
getFirst :: Getting a (a, b) a
getFirst = to fst
|])
This creates the type families L1
, L1Alt
, and GetFirst
; however, these
aren't lenses, because they aren't partially applied. The actual lenses are
L1Sym0
, L1AltSym0
, and GetFirstSym0
. As a convention, I
recommend aliasing the actual lenses with an underscore suffix:
-- L1_ :: Functor f => LensLike f (a, c) (b, c) a b
type L1_ = L1Sym0
-- L1Alt_ :: Functor f => LensLike f (a, c) (b, c) a b
type L1Alt_ = L1AltSym0
-- GetFirst_ :: Getting a (a, b) a
type GetFirst_ = GetFirstSym0
The number after the Sym
is determined by how many arguments you need to
apply to your function before you get to the actual lens. For example,
IxList
requires one argument (the index) to get to the actual traversal, so
the definition in the library is:
type IxList_ i = IxListSym1 i
Second, you can write them directly at the type level using combinators like
MkLens_
and To_
:
type GetFirst_ = To_ FstSym0
(FstSym0
is the promotion of fst
from the singletons library)