View Lens.v
(* Lens and compose definitions *)
Record lens (S A : Type) := {
get : S -> A;
put : S -> A -> S }.
Definition compose {S A B : Type} (ln1 : lens S A) (ln2 : lens A B) : lens S B :=
{| get := fun (s : S) => ln2.(get A B) (ln1.(get S A) s);
put := fun (s : S) (b : B) => ln1.(put S A) s (ln2.(put A B) (ln1.(get S A) s) b) |}.

Lens Composition Proofs


type Lens s a = (GET :: s -> a, PUT :: s -> a -> s)

Lens Laws

  • GetPut: PUT s (GET s) => s
  • PutGet: GET (PUT s a) => a
View ITraversal.scala
package monocle
import scalaz._, Scalaz._
import Indexable._
abstract class IPTraversal[I, S, T, A, B] {
def modifyF[
F[_]: Applicative,

Don't Fear the Profunctor Optics (Part 1/3)

It is said that profunctors are so easy. What about profunctor optics? They should be easy too, right? However, it might be a little bit scary and confusing to face a definition such as

type LensP s t a b = forall p . Cartesian p => p a b -> p s t

for the very first time. In this series, we'll try to introduce all the required concepts that you need to understand this alias (and other ones). To do so, we'll provide visual diagrams where profunctors are seen as boxes which take inputs and produce outputs and profunctor optics are just functions that transform those boxes into more complex ones. Prior to that, a brief introduction to optics will be supplied. We hope these resources help you to never ever fear the profunctor optics.

View UniversityControlLens.hs
{-# LANGUAGE RankNTypes #-}
module UniversityLens where
import Control.Lens
import Data.Char
import Data.Map
-- university data structures
View List2TupleProfunctor.hs
{-# LANGUAGE RankNTypes #-}
module List2TupleProfunctor where
import Control.Monad.State
import Data.Functor.Compose
import Data.Functor.Constant
import Mezzolens
View List2Tuple.hs
module List2Tuple where
import Control.Lens
import Text.Read
-- Record problem: given a record it is required to map it into a particular
-- ADT. Particularly, we'll be mapping `[String]` to `(String, String, Int)`.
-- Those fields correspond with a person with last name, first name and age.
-- Firstly, we describe a prism to extract a number out of a string. Notice that
View ProfunctorOpticsApi.hs
{-# LANGUAGE RankNTypes #-}
module ProfunctorOpticsApi where
-- Given profunctor type classes
class Profunctor p where
dimap :: (a'-> a) -> (b -> b') -> p a b -> p a' b'
class Bifunctor p where
View Algebra.hs
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeSynonymInstances #-}
module Algebra where
import Prelude hiding (Monoid, Monad)
View ConstraintAsParameter.hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
module ConstraintAsParameter where
import Control.Monad.Reader
import Control.Monad.State
type MyType ev a p = (ev a p) => p a