liquidlens.hs

{-# 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 }
@-}

This code has a lot of external deps; unfortunately if you reflect foo then you have to reflect everything foo can depend on (i.e. in the body of foo...) -- so that we can have the complete definitions of foo (and everything it may call...)

Getting the following error on view_elim after defining Const and Identity in the file (using the latest build from develop)

view_elim :: (s -> a) -> (s -> b -> t) -> Proof
{-@ view_elim :: f:_ -> g:_ -> { view (lens f g) = f } @-}
view_elim f g
  = view (lens f g)
  ==. getConst . (lens f g) Const
  ==. getConst . (\afb s -> g s <$> afb (f s)) Const
  ==. getConst . (\s -> g s <$> Const (f s))
  ==. getConst . (\s -> Const (f s))
  ==. getConst . Const . f
  ==. f
  *** QED

/Users/matt/.local/bin/liquid liquidlens.hs                                                                                                                                         ⏎
LiquidHaskell Version 0.8.2.4, Git revision 8927debaf7b7cd166981ef4bb3f05ac81d22559f (dirty)
Copyright 2013-18 Regents of the University of California. All Rights Reserved.


**** DONE:  A-Normalization ****************************************************


Trace: [coercion-type-eq-1: Sym (Main.N:Identity[0] <b>_R)] : b ~ Main.Identity b

Trace: [TYPE-EQ-TO-LOGIC] : b##a3mi : (Main.Identity b##a3mi)

Trace: [coercion-type-eq-1: Sym (Main.N:Const[0] <a>_R <b>_P)] : a ~ Main.Const a b

Trace: [TYPE-EQ-TO-LOGIC] : a##a3mr : (Main.Const a##a3mr b##a3ms)

**** DONE:  Extracted Core using GHC *******************************************


**** DONE:  Transformed Core ***************************************************

liquid:
**** ERROR *********************************************************************
**** ERROR *********************************************************************
**** ERROR *********************************************************************
safeFromList with duplicates ["s##a3mB"] mkCoSub
**** ERROR *********************************************************************
**** ERROR *********************************************************************
**** ERROR *********************************************************************

CallStack (from HasCallStack):
  error, called at src/Language/Fixpoint/Misc.hs:146:14 in liquid-fixpoint-0.7.0.7-LnTlLgskv0s1jewmtbvTmj:Language.Fixpoint.Misc
  errorstar, called at src/Language/Fixpoint/Misc.hs:263:24 in liquid-fixpoint-0.7.0.7-LnTlLgskv0s1jewmtbvTmj:Language.Fixpoint.Misc
  safeFromList, called at src/Language/Fixpoint/Solver/Instantiate.hs:425:19 in liquid-fixpoint-0.7.0.7-LnTlLgskv0s1jewmtbvTmj:Language.Fixpoint.Solver.Instantiate```