Last active
August 29, 2015 14:18
-
-
Save japesinator/673b52e09acf1972eb65 to your computer and use it in GitHub Desktop.
They work!
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Main | |
import Data.Profunctor | |
import Data.Profunctor.Lens | |
-- This is an unpleasant helper function because type inference is Hard | |
myLens : Lensing p => Simple (Lens {p}) (String, String) String | |
myLens = _1 | |
-- hello : String | |
-- hello = view _1 ("hello", "world") | |
-- ----------------------------------------------------------- | |
-- When elaborating right hand side of hello: | |
-- When elaborating argument a to constructor Builtins.MkPair: | |
-- Can't unify | |
-- String (Type of "hello") | |
-- with | |
-- a (Expected type) | |
-- :( | |
hello : String | |
hello = view myLens ("hello", "world") -- "hello" | |
goodbyeworld : (String, String) | |
goodbyeworld = set myLens "goodbye" ("hello", "world") -- ("goodbye", "world") | |
ollehworld : (String, String) | |
ollehworld = over myLens reverse ("hello", "world") -- ("olleh", "world") | |
-- This is the same problem as with myLens | |
myPrism : Prisming p => Simple (Prism {p}) (Either String String) String | |
myPrism = _l | |
jhi : Maybe String | |
jhi = preview myPrism (Left "hi") -- Just "hi" | |
lhi: Either String String | |
lhi= review myPrism "hi" -- Left "hi" |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment