https://ucsd-progsys.slack.com/archives/DU17X62Q5/p1621006535008300
DISCO full full GHC+LH build = 120s vs Z3 ... 7s (!)
$ stack build --dependencies-only
$ time stack build
develop
Executed in 166.60 secs fish external usr time 156.04 secs 66.80 millis 155.98 secs sys time 7.46 secs 9.35 millis 7.45 secs
#1150 -- FUNCTION ucsd-progsys#1149 -- ??? ucsd-progsys#1120
--fullcheck --checkderived --noclasscheck
<<<<<<< HEAD
#1150 -- FUNCTION ucsd-progsys#1149 -- ??? ucsd-progsys#1120
Don't encode non-encodable ADTs (by default)
=======
102b3384caff33c1d722dcbb96eb20913bcbb064
- Implement
Bare.SpecDep - Use
sliceto pre-filter theBareSpecprior to resolution
-- | This module has datatypes and code for building a Specification Dependency Graph
-- whose vertices are 'names' that need to be resolve, and edges are 'dependencies'.
module SpecDep (slice) where
-- | A datatype for the different kinds of names we have to resolve
data Label
= Sign -- ^ identifier signature
| Func -- ^ measure or reflect
| DCon -- ^ data constructor
| TCon -- ^ type constructor
-- | A datatype for nodes which are pairs of names and labels
data Node = MkNode
{ nodeName :: LocSymbol
, nodeLabel :: Label
}
type Graph = Map Node [Node]
-- | A way to combine graphs of multiple modules
instance Semigroup Graph where
TODO
instance Monoid Graph where
TODO
-- | A function to build the dependencies for each module
specDepGraph :: BareSpec -> Graph
specDepGraph = _TODO
mkDepGraph :: [BareSpec] -> Graph
mkDepGraph specs = mconcat [specDepGraph sp | sp <- specs]
-- | 'reachable roots g' returns the list of Node transitively reachable from roots
reachable :: [Node] -> Graph -> [Node]
reachable roots g = _TODO
-- | Top-level "slicing" function
slice :: (ModName, BareSpec) -> [(ModName, BareSpec)] -> [(ModName, BareSpec)]
slice (tgt, tgtSpec) specs = _TODOThe use of Prelude.error gives a crazy performance hit
apparently even without cut-vars being generated, this is
because of some bizarro GHC transforms, that thwart eliminate.
This is because GHC now threads callstack through such
computations, which make a top-level signature no longer top-level.
Prelude.error -> dummyError (no call-stack)
LambdaEval.hs 11 -> 4 -> 4
Map0.hs 27 -> 13 -> 13
Map2.hs ""
Map.hs ""
Base 103 -> 76.18 -> 68
Not clear
Does all that PatSelfBind stuff help at all with these benchmarks?
-
NO.
-
Or do we need to really use a different
error? -
If not, REMOVE IT.
-
ES:fix Target
-
ES:bring back bench
-
NV: Termination requires Haskell signature in
tests/pos/Term.hs -
NV: bound syntax
tests/todo/dropWhile.hs -
NV: bound
icfp/pos/FindRec.hs -
NV: HACK IO TyCon lookup, it appears as a data con (in Lookup)
The below gives a nice SORT error
import Data.Set
data RBTree a = Leaf | Node
{-@ measure isB :: RBTree a -> (Set a)
isB (Leaf) = 1
isB (Node) = (Set_empty 0)
@-}rjhala@borscht ~/r/s/liquidhaskell (prune-unsorted-error)> stack exec -- liquid tests/todo/prune.hs
/Users/rjhala/research/stack/liquidhaskell/tests/todo/prune.hs:7:13-15: Error: Bad Type Specification measure isB :: (RBTree a b) -> (Set a) Type constructor Prune.RBTree expects a maximum 1 arguments but was given 2 arguments
/Users/rjhala/research/stack/liquidhaskell/tests/todo/prune.hs:14:13: Error: Bad Measure Specification measure isB The sort (Set_Set @(42)) is not numeric because Cannot unify (Set_Set @(42)) with int in expression: 1 because Cannot cast 1 of sort int to incompatible sort func(1, [(Set_Set @(0))])
now put another SORT CHECK for measures:
-
Input type should be "isGeneric"
isGeneric T if
- T is a TyConApp
c [t1...tn]
where t1 .. tn are DISTINCT type variables.
- T is a TyConApp
If the above SORT CHECK fails for any measure print an ERROR message saying:
please rerun with --prune-unsorted
(:) :: Int -> [Int] -> [Int]
sum :: [Int] -> Int
sum [] = 0
sum (x:xs) = x + sum xs
sum :: Tree Int a -> Int
sum Leaf = 0
sum Node k _ l r = k + sum l + sum rSee https://github.com/ucsd-progsys/liquidhaskell/blob/master/tests/todo/kmpMonad.hs#L55 It is safe is 100 is changed to 0. WHY?
Restore LAZYVARS in Data/Text.hs, Data/Text/Unsafe.hs
Proposed by Valentine: in dependent languages (Coq)
inductors (like our loop for natural numbers)
automatically get types abstracted over properties.
Traversal should create such functions.
Maybe we can automatically refine them.
-
benchmarks: Data.Bytestring ? readsPrec ? big constants issue : _word64 34534523452134213524525 due to (deriving Typeable)
- see others below
-
hmatrix
-
error messages (see issues on github)
time(O|N|C) TOTAL(O|N) solve (O|N) refines iterfreq
Map.hs : 54/50/32/10 21/15/8.7 14/8/4.3 9100/4900/2700 16/28/7
ListSort.hs : */7.5/5.5/2 */2.5/1.8 */1.5/1.0 */1100/600 */9/7
GhcListSort.hs : 23/22/17/5 7.3/7.8/5 4.5/5.0/2.7 3700/4400/1900 10/23/6
LambdaEval.hs : 36/32/25/12 17/12/10 11.7/6.0/5 8500/3100/2400 12/5/5
Base.hs : 26mi/2m
[OK] Data.KMeans [OK] GHC.List (../benchmarks/ghc-7.4.1/List.lhs) [OK] bytestring [OK] text
[??-PP] Data.Map (supersedes set) - ordering [OK] - size - key-set-properties - key-dependence - balance (NO)
-
vector-algorithms "vector bounds checking"
- e.g. "unsafeSlice"
- maybe only specify types for Vector?
-
vector
-
repa
-
repa-algorithms
-
xmonad (stackset)
-
snap/security
-
hmatrix
http://hackage.haskell.org/packages/archive/hmatrix/0.12.0.1/doc/html/src/Data-Packed-Internal-Matrix.html#Matrix http://hackage.haskell.org/packages/archive/hmatrix/0.12.0.1/doc/html/src/Data-Packed-Internal-Vector.html#fromList
-> FingerTrees (containers / Data.Seq) -> Union-Find (PLDI09 port if necessary?) -> BDD (PLDI09 port if necessary?)
[NO] Data.Set (Map redux) > ordering > size > set-properties > balance (NO)
[NO] Data.IntSet > tricky bit-level operations/invariants
Paper #2
-> Haskell + DB / Yesod / Snap -> NDM/catch benchmarks (with refinements)
-> tests/todo/fft.hs
-> binsearch crashes because you have chains like:
x1 = 2
x2 = x1
x3 = x2
z = x3 / 2
so I guess you need some constprop inside the constraint simplification.
- tests/pos/data-mono0.hs
partial pattern match desugars into exception syntax with unhandled
casts. Throws an error in fixpoint. At least throw error in Constraint Gen?
(\ _ ->
(Control.Exception.Base.irrefutPatError
@ () "pos/data-mono0.hs:8:9-23|(Test.Cons x _)")
cast(UnsafeCo () GHC.Types.Int :: () ~ GHC.Types.Int)) GHC.Prim.realWorld#;
Theorems (from Wouter Swierstra's Coq Development)
- Invariant: NoDuplicates
- prop_empty_I : new : ? -> {v | invariant(v)}
- prop_view_I : view : ? -> {v | invariant(v)}
- prop_greedyView_I : view : ? -> {v | invariant(v)}
- prop_focusUp_I
- prop_focusMaster_I
- prop_focusDown_I
- prop_focus_I
- prop_insertUp_I
- prop_delete_I
- prop_swap_master_I
- prop_swap_left_I
- prop_swap_right_I
- prop_shift_I
- prop_shift_win_I
[prop_FOO_I] check that various functions outputs satisfy "invariant"
FOO :: ??? -> {v: StackSet | invariant(v)}
> Theorem prop_swap_master_I (s : StackSet.stackSet i l a sd) :
> Theorem prop_view_I (l a sd : Set) (n : nat) (s : StackSet.stackSet nat l a sd) :
> Theorem prop_greedyView_I (l a sd : Set) (n : nat) (s : StackSet.stackSet nat l a sd) :
> Theorem prop_focusUp_I (l a sd : Set) (n : nat) (s : StackSet.stackSet nat l a sd) :
> Theorem prop_focusDown_I (l a sd : Set) (n : nat) (s : StackSet.stackSet nat l a sd) :
> Theorem prop_focusMaster_I (l a sd : Set) (n : nat) (s : StackSet.stackSet nat l a sd) :
> Theorem prop_empty_I (m : l) (wids : {wids : list i | wids <> nil})
> Theorem prop_empty (m : l) (wids : {wids : list i | wids <> nil})
> Theorem prop_differentiate (xs : list a) :
[prop_FOO_local] check that various functions preserve a [hidden_spaces] MEASURE
FOO :: x: StackSet -> {v: StackSet | hidden_spaces(v) = hidden_spaces(x) }
> Theorem prop_focus_down_local (s : stackSet i l a sd) :
> Theorem prop_focus_up_local (s : stackSet i l a sd) :
> Theorem prop_focus_master_local (s : stackSet i l a sd) :
> Theorem prop_delete_local (s : stackSet i l a sd) (eq_dec : forall x y, {x = y} + {x <> y}) :
> Theorem prop_swap_master_local (s : stackSet i l a sd) :
> Theorem prop_swap_left_local (s : stackSet i l a sd) :
> Theorem prop_swap_right_local (s : stackSet i l a sd) :
> Theorem prop_shift_master_local (s : stackSet i l a sd) :
> Theorem prop_insert_local (x : stackSet i l a sd) (eq_dec : forall x y, {x = y} + {x <> y}) :
BAD: these check that: forall x: foo (bar x) == x
> Theorem prop_focus_right (s : StackSet.stackSet i l a sd) :
> Theorem prop_focus_left (s : StackSet.stackSet i l a sd) :
[prop_swap_*_focus] check that various functions preserve a [peek] MEASURE > Theorem prop_swap_master_focus (x : StackSet.stackSet i l a sd) : > Theorem prop_swap_left_focus (x : StackSet.stackSet i l a sd) : > Theorem prop_swap_right_focus (x : StackSet.stackSet i l a sd) :
BAD? forall x. swapMaster (swapMaster x) == x > Theorem prop_swap_master_idempotent (x : StackSet.stackSet i l a sd) :
BAD? forall x. view i (view i x) == (view i x) > Theorem prop_focusMaster_idem (x : StackSet.stackSet i l a sd) :
NO. Prove: view :: i -> x -> {v: focus(v) = i}
:: i -> x -> {v: focus(x) = i => x = v }
To prove foo_IDEMPOTENT, find a property P such that:
foo :: x:t -> {v:t | P(v)}
foo :: x:t -> {v:t | P(x) => v = x }
SETS: > Theorem prop_screens (s : stackSet i l a sd) :
TRIV/HARD: (function definition) > [TRIV] Theorem prop_screens_work (x : stackSet i l a sd) : > Theorem prop_mapWorkspaceId (x : stackSet i l a sd) : > Theorem prop_mapLayoutId (s : stackSet i l a sd) : > Theorem prop_mapLayoutInverse (s : stackSet i nat a sd) : > Theorem prop_mapWorkspaceInverse (s : stackSet nat l a sd) :
Theorem prop_lookup_current (x : stackSet i l a sd) : Theorem prop_lookup_visible (x : stackSet i l a sd) :
- Useful for DIGRAPH VIZ: http://arborjs.org/halfviz/#
- LIQUIDFAIL : impossible to do verify the spec here
- LIQUIDTODO : possible with some further hacking
http://www.cs.st-andrews.ac.uk/~eb/writings/fi-cbc.pdf
McBride's Stack Machine youtube mcbride icfp 2012 monday keynote agda-curious
data Instr = Push Val | Add
type Val = Int
measure needs :: [Instr] -> Int
needs (Add : is) = min (2, 1 + needs(is))
needs (Push v : is) = 0
run :: is:[Instr] -> {v:[Val] | len(v) >= needs(is)} -> [Val]
run (Add:is) (x1:x2:vs) = run is (x1 + x2 : vs)
run (Push v : is) vs = run is (v : vs)
btw, did you guys see this:
http://www.reddit.com/r/haskell/comments/1okcmh/odd_space_leak_when_using_parsec/
the poster probably feels silly, but I have, on several occasions, hit this issue with parsec. Wonder whether our termination checker could be used... hmm...
Sure! You just have to give
type GenParser tok st = Parsec [tok] st
a size, I guess (len [tok]). The hard part will be to prove it when the size is actually decreasing...
Hmm... Surely we need to track somehow the "effect" of executing a single parsing action.
For example,
chars :: Char -> Parser [Char]
chars c = do z <- char c
zs <- chars c
return (z:zs)
What is the machinery by which the "recursive call" is run on a "smaller" GenParser?
Does it help if we remove the do block?
chars :: Char -> Parser [Char]
chars c = char c >>= \z ->
chars c >>= \zs ->
return (z:zs)
I guess the question becomes, how/where do we specify (let alone verify) that the function
char c consumes one character, hence causing the chars to run on a smaller input?
Phew, after banging my head against this all day, this is what I came up with.
You need a measure
measure eats :: Parser a -> Nat
which describes (a lower bound) on the number of tokens consumed by the action Parser a.
Now, you give
return :: a -> {v: Parser a | (eats v) = 0}
and most importantly,
(>>=) :: forall <Q :: Parser b -> Prop>
x: Parser a
-> f:{v: a -> Parser b | (rec v) => (eats x) > 0}
-> exists z:Parser b
. {v:Parser b | (eats v) = (eats z) + (eats x)}
(Of course you have to give appropriate signatures for the parsec combinators
-- perhaps one can even PROVE the eats measure. However, note that
type Parser a = [Char] -> (a, [Char])
roughly speaking, and here eats is actually the DIFFERENCE of the lengths of
the input and output [Char] ... so I'm not sure how exactly we would reason about
the IMPLEMENTATION of eats but certainly we should be able to USE it in clients
of parsec.
Note that you need a refinement ON the function type, the idea being that:
-
the BODY of a recursive function is checked in the termination-strengthened environment that constrains the function to satisfy the predicate
rec -
whenever you use >>= on a recursive function, the PRECEDING action must have consumed some tokens.
-
the number of tokens consumed by the combined action equals the sum of the two actions (all the business about exists z and Q is to allow us to depend on the output value of
f(c.f. tests/pos/cont1.hs)
-
Create a test case:
tests/todo/Eff*.hs -
Introduce a new sort of refinement
Ref(with aliasRTProp)- Types.hs: Add to
Ref-- in addition toRMono[--->RPropP] andRPoly[--->RProp] - Types.hs: Add a
World tfor SL formulas...
- Types.hs: Add to
-
Allow
PVarto have the sortHProp- CHANGE
ptype :: PVKind twheredata PVKind t = PVProp t | PVHProp - Can we reuse
RAllPto encodeHProp-quantification? (YES) - Update
RTyConto storeHPropvars
- CHANGE
-
Update consgen
- Can we reuse type-application sites for
HProp-instantiation? (Yes)
- Constraint.hs :1642: = errorstar "TODO:EFFECTS:freshPredRef"
- PredType.hs : go _ (_, RHProp _ _) = errorstar "TODO:EFFECTS:replacePreds"
- Can we reuse type-application sites for
-
Write cons-solve
- eliminate/solve
HPropconstraints prior to subtype splitting.
- eliminate/solve
-
Index
IOorStatebyHProp- Parse.hs: Update
dataparser to allowTyConto be indexed by abstractHProp - Bare.hs :482 : addSymSortRef _ (RHProp _ _) = errorstar "TODO:EFFECTS:addSymSortRef"
- Parse.hs: Update
TODO:EFFECTS:ASKNIKI
- What is
isBind,pushConsBindin Constraint.hs?
- Suitable signatures for monadic operators
a. Following RProp we should have
- RHProp := x1:t1,...,xn:tn -> World
b. Where World is a spatial conjunction of
- WPreds : (h v1 ... vn), h2, ...
- Wbinds : x1 := T1, x2 := T2, ...
c. Such that each World has at most one WPred (that is not rigid i.e. can be solved for.)
Problem: rejigger inference to account for parameters in heap variables.
Per Niki:
RProp := x1:t1,...,xn:tn -> RType
with the 'predicate' application implicitly buried as a ur_pred inside the RType
For example, we represent
[a]
as
RApp [] a (RPoly [(h:a)] {v:a
}) true
which is the RTycon for lists [] applied to:
-
Tyvar
a -
RPoly with:
- params
h:a - body
{v:a<p> | true}which is really,RVar a {ur_reft = true, ur_pred = (Predicate 'p' with params 'h')}
- params
-
Outer refinement
true
Heap Propositions HProp
CP := l :-> T * CP -- Concrete Heap
| emp
HP := CP
| CP * H -- Heap VariableThat is, an HProp is of the form:
H * l1 |-> T1 * ... * ln |-> Tn
or
l1 |-> T1 * ... * ln |-> Tn
I am disallowing multiple variables because it causes problems...
Abstractly Refined ST/IO
data IO a <Pre :: HProp, Post :: a -> HProp>Refined Monadic Operators
return :: forall a, <H :: HProp>.
a -> IO <H, \_ -> H> a
(>>=) :: forall a, b, <P :: HProp, Q :: a -> HProp, R :: b -> HProp>.
IO<P, Q> a -> (x:a -> IO<Q x, R> b) -> IO<P, R> bQ1. How does LH reason about HProp?
Via subtyping as always, so:
forall i. Γ |- Ti <: Ti'
-----------------------------------
Γ |- *_i li :-> Ti <: *_i li -> Ti'
For this, we need to put in explicit HProp instantiations, just like
tyvar (α) and predvar (π) instinstatntiations. This is doable with a
pre-pass that generates and solves HProp constraints as follows:
- At each instantiation, make up fresh variables
h - Treat bound heap-variables as constants
- Instantiation yields a set of constraints over
h - Solve constraints via algorithm below.
Q2. Can you name values inside HProp?
Nope. There's no reason for this, but its tedious to have to make up new heap binders and what not. Clutters stuff. This is slightly problematic. For example, how do you write a function of the form:
incr :: p:IORef Int -> IO Intwhich increments the value stored at the reference? Solution is slightly clunky: rather than the implicit heap binder, add an explicit pure parameter:
incr :: p:IORef Int -> i:Int -> IO {v:Int| v = i} <p |-> {v = i}, p |-> {v = i + 1}>Q3. How to relate Post-condition to the Pre-conditions?
Note that the Post-condition is a unary predicate -- i.e. does not
refer to the input world. How then do we relate the input and output heaps?
As above: name the values of the input heap that you care about, and then
relate Post to Pre via the name.
Q4. How to read values off the heap?
Given that we don't have heap binders, this might seem like a problem? Not really. Just write signatures like:
read :: IORef a -> IO a
aha, but there's a problem: the a is too coarse or flow-insensitive: it
holds a supertype of all the values written at the location, as opposed to the
current value. No matter, abstract refinements to the rescue:
read :: forall <I :: a -> Prop>.
p:IORef a -> IO <p |-> a<I>, p |-> a<I>> a<I>
Q5. How do you do subtyping on heaps/frame rule?
Wait, how do I write compositional signatures that only talk about a particular part of the state but allow me to say other parts are unmodified etc? Don't you need heap subtyping? No: we can make the frame rule explicit by abstracting over heaps:
read :: forall <I :: a -> Prop, H :: HProp>.
p:IORef a -> IO <p |-> a<I> * H, p |-> a<I> * H> a<I>
Q6. How to solve heap constraints?
Heap constraints are of the form:
- (C0)
ch1 = ch2-- constants - (C1)
H1 * ch1 = ch2-- 1-variable - (C2)
H1 * ch1 = H2 * ch2-- 2-variable
Here, each ch is of the form:
l1 |-> τ1 * ... * ln -> τn * A1 * ... * An
where each Ai is a rigid or quantified heap var that is atomic,
i.e. cannot be further solved for. For solving, we throw away all
refinements, and just use the shape τ.
solve :: Sol -> [Constraint] -> Maybe Sol
solve σ []
= Just σ
solve σ (c:cs)
= case c of
C0 ch1 ch2 ->
if ch1 `equals` ch2 then
-- c is trivially SAT,
solve σ cs
else
-- c and hence all constraints are unsat
Nothing
C1 (H1 * ch1) ch2 ->
if ch1 `subset` ch2 then
let σ' = [H1 := c2 `minus` c1]
solve (σ . σ') (σ' <$> cs)
else
-- c and hence all constraints are unsat
Nothing
C2 (H1 * ch1) (H2 * ch2) ->
let H = fresh heap variable
let σ' = [H1 := H * ch2, H2 := H * ch1]
solve (σ . σ') (σ' <$> cs)
Can we use abstract refinements to do "stateful reasoning",
e.g. about stuff in IO ? For example, to read files, this
is the API:
open :: FilePath -> IO Handle
read :: Handle -> IO String
write :: Handle -> String -> IO ()
close :: Handle -> IO ()
The catch is that:
readandwriterequire theHandleto be in an "open" state,- which is the state of the
Handlereturned byopen, - while
closepresumably puts theHandlein a "closed" state.
So, suppose we parameterize IO with two predicates a Pre and Post condition
data IO a <Pre :: World -> Prop> <Post :: a -> World -> World -> Prop>
where World is some abstract type denoting the global machine state.
Now, it should be possible to give types like:
(>>=) :: IO a <P, Q> -> (x:a -> IO b<Q x, R>) -> IO b<P, R> return :: a -> IO a <P, P>
which basically state whats going on with connecting the conditions, and then, give types to the File API:
open :: FilePath -> IO Handle <_ -> True> <\h _ w -> (IsOpen h w)> read :: h:Handle -> IO String <\w -> (IsOpen h w)> <_ _ w -> (IsOpen h w)> close :: h:Handle -> IO () <\w -> (IsOpen h w)> <_ _ w -> not (IsOpen h w)>
Wonder if something like this would work?
Niki: My question is how do you make Q from a post-condition (Q :: a -> Word -> Word -> Prop) to a pre-condition. I guess you need to apply a value x :: a and a w :: Word to write (a -> IO b<Q x w, R>).
I think the problem is that the "correct" values x and w are not "in scope"
So assume
data IO a <P :: Word -> Prop, Q: a -> Word -> Word -> Prop>
= IO (x:Word<P> -> (y:a, Word<Q y x>))
and you want to type
bind :: IO a <P,Q> -> (a -> IO b <Q x w, R>) -> IO b <P,R>
bind (IO m) k = IO $ \s -> case m s of
(a, s') -> unIO (k a) s'
You have
IO m :: IO a <P. Q> => m :: xx:Word <P> -> (y:a, Word <Q y xx>)
you can assume
s:: Word <P>
so
m s :: (y:a, Word <Q y s>)
k a :: IO b <Q x w, R>
uniIO (k a) :: z:Word <Q x w> -> (xx:b, Word <R xx z>)
and we want
(uniIO k a) s :: (xx:b , Word <R xx s>)
so basically we need
P => Q x w
to be able to make the final application
Ranjit You are right. We need to convert the "post" of the first action into the "pre" of the second, which is a problem since the former takes three, parameters while the latter takes only one.
BUT, how about this (basically, all you need is an EXISTS).
-- | the type for return says that the output world satisfies
-- whatever predicate the input world satisfied.
return :: a -> IO a <P, {_ _ w' -> (P w')}>
-- | the type for bind says that its action requires as input a world that satisfies
-- Q (for SOME input world w0) and produces as output an R world.
(>>=) :: IO a <P, Q>
-> (x:a -> \exists w0:World. IO b<{\w -> (Q x w0 w)}, R>)
-> IO b<P, {\xb w w' -> \exists xa:a w0:World.(R xb w0 w')}>
Basically, I am using exists in the same way as in the "compose"
https://github.com/ucsd-progsys/liquidhaskell/blob/master/tests/pos/funcomposition.hs
to name the intermediate worlds and results (after all, this seems
like a super fancy version of . ) -- may have not put them in the
right place...
Btw, the existential is also how the HOARE rule for strongest postcondition works, if you recall:
{P} x := e {exists x'. P[x'/x] /\ x = e[x'/x]}
One of the hardest steps seem to type the monad function (>>=):
So, suppose we parameterize IO with two predicates a Pre and Post condition
data IO a <Pre :: World -> Prop> <Post :: a -> World -> World -> Prop>
where World is some abstract type denoting the global machine state.
Now, it should be possible to give types like:
(>>=) :: IO a <P, Q> -> (a -> IO b<Q, R>) -> IO b<P, R> return :: a -> IO a <P, P>
My question is how do you make Q from a post-condition (Q :: a -> Word -> Word -> Prop) to a pre-condition. I guess you need to apply a value x :: a and a w :: Word to write (a -> IO b<Q x w, R>).
I think the problem is that the "correct" values x and w are not "in scope"
So assume data IO a <P :: Word -> Prop, Q: a -> Word -> Word -> Prop> = IO (x:Word
-> (y:a, Word))
and you want to type
bind :: IO a <P,Q> -> (a -> IO b <Q x w, R>) -> IO b <P,R> bind (IO m) k = IO $ \s -> case m s of (a, s') -> (unIO (k a)) s'
You have
IO m :: IO a <P. Q>
=> m :: xx:Word
-> (y:a, Word )
you can assume s:: Word
so
m s :: (y:a, Word )
k a :: IO b <Q x w, R>
uniIO (k a) :: z:Word -> (xx:b, Word )
and we want (uniIO k a) s :: (xx:b , Word )
so basically we need P => Q x w to be able to make the final application
bind :: ST a <P,Q> -> (a -> ST b <Q x w, R>) -> ST b <P,R>
bind (ST f1) k = ST $ \s0 -> let (x, s1) = f1 s0
ST f2 = k x
(y, s2) = f2 s1
in
(y, s2)
Haskell has a class (and related functions)
toDyn :: (Typeable a) => a -> Dynamic
fromDyn :: (Typeable a) => Dynamic -> Maybe a
Q: How to encode heterogeneous maps like:
d1 = { "name" : "Ranjit"
, "age" : 36
, "alive" : True
}
and also:
d2 = { "name" : "Jupiter"
, "position": 5
}
so that you can write generic duck-typed functions like
showName :: Dict -> String
and write
showName d1
showName d2
or even
map showName [d1, d2]
Step 1: Encode dictionary as vanilla Haskell type
type Dict <Q :: String -> Dynamic -> Prop> = Map String Dynamic <Q>
empty :: Dict
put :: (Dynamic a) => String -> a -> Dict -> Dict
get :: (Dynamic a) => String -> Dict -> Dict
Step 2: Create dictionaries
d1 = put "name" "RJ"
$ put "age" 36
$ put "alive" True
$ empty
d1 = put "name" "Jupiter"
$ put "pos" 5
$ empty
Step 3: Lookup dictionaries
showName :: Dict -> String
showName d = get "name" d
-- TODO: how to support
showName :: Dict -> Dict
incrAge d = put "age" (n + 1) d
where
n = get "age" d
-- TODO: how to support
concat :: Dict -> Dict -> Dict
Step 4: Can directly, without any casting nonsense, call
showName d1
showName d2
Need to reflect Haskell Type (or at least, TypeRep values)
inside logic, so you can write measures like
measure TypeOf :: a -> Type
and use it to define refinements like
(TypeOf v = Int)
(TODO: too bad we don't have relational measures... or multi-param measures ... yet!)
which we can macro up thus.
predicate HasType V T = (TypeOf V = T)
predicate Fld K V N T = (K = N => (HasType V T))
Step 5: Refined Signatures for Dict API
put :: (Dynamic a) => key:String
-> {value:a | (Q key value)}
-> d:Dict <Q /\ {\k _ -> k /= key}>
-> Dict <Q /\ {\k v -> (Fld k v key a)}>
get :: (Dynamic a) => key:String
-> d:Dict <{\k v -> (Fld k v key a)}>
-> a
Step 6: Now, for example, we should be able to type our dictionaries as
{-@ d1 :: Dict<Q1> @-}
where
Q1 == \k v -> Fld k v "name" String /\
Fld k v "age" Int /\
Fld k v "alive" Bool
and
{-@ d2 :: Dict<Q2> @-}
where
Q2 == \k v -> Fld k v "name" String /\
Fld k v "pos" Int /\
TODO:
-
add support for
Typeinside logic- needed for
TypeOfmeasure, equality checks - requires doing type-substitutions inside refinements
- needed for
-
add support for
- update [isn't that just
put?] - concat
- update [isn't that just
-
add support traversals (cf. Ur)
- Fold (over all fields, eg. to serialize into a String)
- Map? (transform all fields to serialize) toDB?
- Filter (takes a predicate that should only read valid columns of the record)
e.g. Type class laws.
Many type-classes come with a set of laws that instances are expected to abide by, e.g.
fmap id == id
fmap (f . g) == fmap f . fmap g
mappend mempty x = x
mappend x mempty = x
mappend x (mappend y z) = mappend (mappend x y) z
Strategy
1. Representing Proofs
data Proof = Proof -- void, pure refinement
type Pf P = {v:Proof | P}
type Eq X Y = Pf (X == Y)
2. Combining Proofs
bound Imp P Q R = P => Q => R
eq, imp :: (Imp P Q R) => Pf P -> Pf Q -> Pf R
refl :: x:a -> Eq a x x
3. Axiomatizing arithmetic
add :: x:Int -> y:Int -> {z:Int | z = x + y} -> Eq (x + y) z
add x y z = auto
Example 1: Arithmetic
Lets drill in: how to represent the following "equational" proof in LH?
(1 + 2) + (3 + 4) -- e0
{ 1 + 2 == 3}
== 3 + (3 + 4) -- e1
{ 3 + 4 == 7}
== 3 + 7 -- e2
{ 3 + 7 == 10}
== 10 -- e3
Now the above proof looks like this:
e0 :: Int
e0 = (1 + 2) + (3 + 4)
prop :: Eq e0 10
prop = (((refl e0 `imp` (add 1 2 3)) -- :: Eq e0 (3 + (3 + 4))
`imp` (add 3 4 7)) -- :: Eq e0 (3 + 7)
`imp` (add 3 7 10)) -- :: Eq e0 10
Example 2: Lists
A more interesting example: Lets prove prop_app_nil:
prop_app_nil: forall xs. append xs [] = xs
The definition of
append [] ys = ys
append (x:xs) ys = x : append xs ys
yields the axioms
append_nil :: ys:_ -> Eq (append [] ys) ys
append_cons :: x:_ -> xs:_ -> ys:_ -> Eq (append (x:xs) ys) (x : append xs ys)
Code on left, "equations" on right.
prop_app_nil :: xs:[a] -> Eq (append xs []) xs
prop_app_nil [] = refl (append [] [])
-- append [] []
`by` (append_nil []) -- { append_nil [] }
-- == []
prop_app_nil (x:xs) = refl (append (x:xs) [])
-- append (x:xs) []
`by` (append_cons x xs []) -- { append_cons x xs [] }
-- == x : append xs []
`by` (prop_app_nil xs) -- { IH: prop_app xs }
-- == x : xs
Example 4: Append Associates
prop_app_assoc :: xs:_ -> ys:_ -> zs:_ ->
Eq ((xs ++ ys) ++ zs) (xs ++ (ys ++ zs))
prop_app_assoc [] ys zs
([] ++ ys) ++ zs
{ append_nil _ }
== ys ++ zs
{ append_nil _ }
== [] ++ (ys ++ zs)
prop_app_assoc (x:xs) ys zs
((x:xs) ++ ys) ++ zs
{ append_cons _ _ _ }
== (x : (xs ++ ys)) ++ zs
{ append_cons _ _ _ }
== x : ((xs ++ ys) ++ zs)
{ prop_app_assoc _ _ _ }
== x : (xs ++ (ys ++ zs))
{ append_cons _ _ _ }
== (x : xs) ++ (ys ++ zs)
Example 4: Map Fusion
Lets go fancier:
forall xs. map (f . g) xs = (map f . map g) xs
Here's the classical (?) equational proof:
map (f . g) []
{ map_nil (f . g) }
== []
{ map_nil f }
== map f []
{ map_nil g }
== map f (map g [])
{ dot f g }
== (map f . map g) []
map (f . g) (x:xs)
{ map_cons (f . g) x xs }
== (f . g) x : map (f . g) xs
{ map_dot f g xs }
== (f . g) x : (map f . map g) xs
{ dot (map f) (map g) }
== (f . g) x : map f (map g xs)
{ dot f g }
== f (g x) : map f (map g xs)
{map_cons f (g x) (map g xs) }
== map f (g x : map g xs)
{map_cons g x xs}
== map f (map g (x : xs))
{ dot (map f) (map g) }
== (map f . map g) (x : xs)
Formalize thus (with functions/axioms)
map f [] = [] -- map_nil
map f (x:xs) = f x : map f xs -- map_cons
(f . g) x = f (g x) -- dot
Now, we formalize map-fusion as:
map_fusion :: f:_ -> g:_ -> xs:_ ->
Eq (map (f . g) xs) (map f . map g) xs
map_fusion f g [] = map_dot_nil f g
map_fusion f g (x:xs) = map_dot_cons f g x xs
The hard work happens in the two "lemmas"
map_dot_nil :: f:_ -> g:_ ->
Eq (map (f . g) []) ((map f . map g) [])
map_dot_nil f g
= refl (map (f . g) [])
-- map (f . g) []
`by` (map_nil (f . g))
-- == []
`by` (map_nil f)
-- == map f []
`by` (map_nil g)
-- == map f (map g [])
`by` (dot f g)
-- == (map f . map g) []
and
map_dot_cons :: f:_ -> g:_ -> x:_ -> xs:_ ->
Eq (map (f . g) (x:xs)) ((map f . map g) (x:xs))
map_dot_cons f g x xs
= refl (map (f . g) (x:xs))
-- map (f . g) (x : xs)
`by` (map_cons (f . g) x xs)
-- == (f . g) x : map (f . g) xs
`by` (map_dot f g xs)
-- == (f . g) x : (map f . map g) xs
`by` (dot (map f) (map g))
-- == (f . g) x : map f (map g xs)
`by` (dot f g)
-- == f (g x) : map f (map g xs)
`by` (map_cons f (g x) (map g xs))
-- == map f (g x : map g xs)
`by` (map_cons g x xs)
-- == map f (map g (x : xs))
`by` (dot (map f) (map g))
-- == (map f . map g) (x : xs)
-
DONE singleton type classes represented by newtype
-
tried to work around by translating
foo
cast(co :: a -> b ~ Foo)to
D:Foo foo
but it still breaks when we don't have an LH class decl
-
without LH class decl we never see D:Foo, so it doesn't go in CGEnv
-
SOLUTION: put ALL visible dict constructors in CGEnv
-
-
casts are used more often and we seem to lose information..- seems particularly problematic with ST
-
srcloc annotations
- -g adds SourceNotes, but the html output is borked
- in particular, infix operators aren't annotated correctly (at all?)
- are we missing some SrcLocs??
-
clearly not, if you look at the output of
ghc -g -ddump-ds -dppr-ticks <file.hs>somewhere along our pipeline the ticks are either being dropped, or the SrcSpans don't quite match the way they used to...
-
-
termination metrics are required in a few places where they were not previously
- my guess is that ghc's behaviour for grouping functions in a
Recbinder have changed
- my guess is that ghc's behaviour for grouping functions in a