In an ideal world, Sprite is supposed to cover all of Vazou–Rondon–Jhala's ESOP-13 paper Abstract Refinement Types.
But I am having difficulty with foldr on p.10:
foldr :: forall <p :: [a] -> b -> Bool>.
(xs:[a] -> x:a -> b <p xs> -> <p (x:xs)>)
-> b<p []>
-> ys:[a]
-> b<p ys>
foldr op b [] = b
foldr op b (x:xs) = op xs x (foldr op b xs)
This would naïvely transliterate into Sprite like this:
type list('a) =
| Nil
| Cons (x:'a, xs:list('a))
;
/*@ val foldr : forall (p: list('a) => 'b => bool).
(xs:list('a) => x:'a => acc:'b[v|p xs v] => 'b[v|p (Cons x xs) v]) =>
seed:'b[v|p (Nil) v] =>
ys:list('a) =>
'b[v|p ys v] */
let rec foldr = (op, seed, ys) => {
switch (ys) {
| Nil => seed
| Cons(h, t) => let nextb = foldr(op, seed, t);
op(t, h, nextb)
}
};
which is of course not even well-formed Sprite, because args in ($p ... ) can only be variables, not anywhich Exprs. And for sure, the above crashes Sprite in rvarArgSymbol:
$ stack exec --profile -- sprite 6 listFoldr.re
Unexpected argument in ref-variable: p (Cons x xs) v EApp (EApp (EVar "Cons") (EVar "x")) (EVar "xs")
CallStack (from -prof):
Language.Sprite.L6.Types.rvarArgSymbol (src/Language/Sprite/L6/Types.hs:(467,1)-(468,124))
Language.Sprite.L6.Types.isRVarApp (src/Language/Sprite/L6/Types.hs:(461,1)-(464,36))
Language.Fixpoint.Misc.mapEither (src/Language/Fixpoint/Misc.hs:(330,1)-(335,48))
Language.Sprite.L6.Types.refactorAppP.(...) (src/Language/Sprite/L6/Types.hs:458:5-58)
Language.Sprite.L6.Types.refactorAppP (src/Language/Sprite/L6/Types.hs:(455,1)-(458,58))
Language.Sprite.L6.Types.refactorAppR (src/Language/Sprite/L6/Types.hs:(450,1)-(451,33))
Language.Sprite.L6.Types.fmap (src/Language/Sprite/L6/Types.hs:57:23-29)
Language.Sprite.L6.Types.refactorApp (src/Language/Sprite/L6/Types.hs:(428,1)-(432,30))
Language.Sprite.L6.Types.generalize (src/Language/Sprite/L6/Types.hs:326:1-41)
Language.Sprite.L6.Parse.mkDecl (src/Language/Sprite/L6/Parse.hs:(249,1)-(255,24))
This seems reasonable, so I went a bit further and tried to get around this limitation by introducing two additional ghosts, nil:list('a)[v| nil = Nil] and cns:list('a)[v | cns = Cons(x,xs) ] — the idea being that the offending applications ($p (Consx,xs) v) would become ($p cns v) — but this only kicks the can down the road because you can't use (Cons x xs) in a predicate like that either (so this crashes Sprite too).
So I went another step and tried to generalize ($p ... ) to take arbitrary Exprs under the hypothesis that those H.Vars ultimately all become PKVars, like in shingarov@84d2ea6 which doesn't work either because those ($p ... ) H.Vars do NOT become PKVars but get picked out into $k##1 etc.
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent