47 lines
1.4 KiB
JavaScript
47 lines
1.4 KiB
JavaScript
// @flow
|
|
|
|
/*
|
|
$Pred<N> is an "abstract predicate type", i.e. denotes a (function) type that
|
|
refines N variables. So if `cb` is a function, then it should be refining
|
|
exactly N argument. It is abstract in that we do not need to specify:
|
|
(a) which variables are going to be refined (just the number), or (b) what
|
|
exactly the refinement (predicate) is going to be.
|
|
|
|
$Refine<T,P,k> is a refinement type, that refines type T with the k-th
|
|
argument that gets refined by an abstract preficate type P.
|
|
*/
|
|
declare function refine<T, P: $Pred<1>>(v: T, cb: P): $Refine<T,P,1>;
|
|
// function refine(v, cb)
|
|
// { if (cb(v)) { return v; } else { throw new Error(); } }
|
|
|
|
/*
|
|
Use case
|
|
*/
|
|
declare var a: mixed;
|
|
var b = refine(a, is_string);
|
|
(b: string);
|
|
|
|
declare function refine_fst<T, P: $Pred<2>>(v: T, w: T, cb: P): $Refine<T,P,1>;
|
|
// function refine_fst(v, w, cb)
|
|
// { if (cb(v, w)) { return v; } else { throw new Error(); } }
|
|
|
|
declare var c: mixed;
|
|
declare var d: mixed;
|
|
|
|
var e = refine2(c, d, is_string_and_number);
|
|
(e: string);
|
|
|
|
|
|
declare function refine2<T, P: $Pred<2>>(v: T, w: T, cb: P): $Refine<T,P,1>;
|
|
|
|
// function refine_fst(v, w, cb)
|
|
// { if (cb(v, w)) { return w; } else { throw new Error(); } }
|
|
|
|
function is_string(x): boolean %checks {
|
|
return typeof x === "string";
|
|
}
|
|
|
|
function is_string_and_number(x, y): %checks {
|
|
return typeof x === "string" && typeof y === "number";
|
|
}
|