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]

Modules

[Last Documentation]

  • Data
    • Type
      • Data.Type.Lens
        • Data.Type.Lens.Example
        • Data.Type.Lens.Internal

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-26T20:27:11Z
Distributions
Reverse Dependencies 1 direct, 0 indirect [details]
Downloads 1720 total (1 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
All reported builds failed as of 2018-10-26 [all 3 reports]

Readme for lens-typelevel-0.1.0.0

[back to package description]

lens-typelevel

lens-typelevel on Hackage Build Status

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> :kind! '("hello", 6) ^. CloneLens_ L1_
"hello"

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"]