Last active
March 20, 2018 16:23
-
-
Save themattchan/28f3c615c435a476fcbf3cc9d1a7166d to your computer and use it in GitHub Desktop.
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
{-# LANGUAGE ExistentialQuantification, RankNTypes #-} | |
module Main where | |
{-@ LIQUID "--higherorder" @-} | |
import Language.Haskell.Liquid.ProofCombinators | |
import Data.Functor.Const | |
import Data.Functor.Identity | |
type Lens s t a b = forall f. Functor f => (a -> f b) -> (s -> f t) | |
{-@ reflect lens @-} | |
lens :: (s -> a) -> (s -> b -> t) -> Lens s t a b | |
lens f g = \afb s -> g s <$> afb (f s) | |
{-@ reflect view @-} | |
view :: Lens s t a b -> s -> a | |
view l s = getConst (l Const s) | |
{-@ reflect set @-} | |
set :: Lens s t a b -> b -> s -> t | |
set l b s = runIdentity (l (\_ -> Identity b) s) | |
-- originally tried to prove this, but realised that you need | |
-- to inspect under binders to get the component functions of the lens | |
view_update :: Lens s s a a -> s -> a -> Proof | |
{-@ view_update :: l:_ -> s:_ -> a:_ -> { view l (set l s a) = a } @-} | |
-- maybe this can be used as a lemma?? | |
view_elim :: (s -> a) -> (s -> b -> t) -> Proof | |
{-@ view_elim :: f:_ -> g:_ -> { view (lens f g) = f } @-} | |
-- ... to prove this reformulation of view_update | |
view_update' :: (s -> a) -> (s -> a -> s) -> s -> a -> Proof | |
{-@ view_update' :: f:_ -> g:_ -> s:_ -> a:_ | |
-> { view (lens f g) (set (lens f g) s a) = a } | |
@-} | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Getting the following error on
view_elim
after definingConst
andIdentity
in the file (using the latest build fromdevelop
)