lens-typelevel: Type-level lenses using singletons

[ bsd3, dependent-types, lenses, library ] [ Propose Tags ]

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.


[Skip to Readme]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.1.0.0, 0.1.0.1, 0.1.1.0
Change log CHANGELOG.md
Dependencies base (>=4.12 && <5), singletons (>=2.5) [details]
License BSD-3-Clause
Copyright (c) Justin Le 2018
Author Justin Le
Maintainer justin@jle.im
Category Dependent Types, Lenses
Home page https://github.com/mstksg/lens-typelevel#readme
Bug tracker https://github.com/mstksg/lens-typelevel/issues
Source repo head: git clone https://github.com/mstksg/lens-typelevel
Uploaded by jle at 2018-10-29T21:57:37Z
Distributions
Reverse Dependencies 1 direct, 0 indirect [details]
Downloads 1722 total (3 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs uploaded by user
Build status unknown [no reports yet]

Readme for lens-typelevel-0.1.1.0

[back to package description]

lens-typelevel

lens-typelevel on Hackage Build Status

(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 lactual 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)