tweag/nickel
1
1
Fork 0
mirror of https://github.com/tweag/nickel.git synced 2024-09-20 16:08:14 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #219 from tweag/syntax/typing-promise

Browse Source 
[Syntax]Use colon as the static typing operator
This commit is contained in:
Eelco Dolstra 2020-11-30 12:13:42 +01:00 committed by GitHub
commit 209b9ef62d
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
17 changed files with 249 additions and 254 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/error.rs
View File

@ -148,7 +148,7 @@ pub enum TypecheckError {
/// argument of a wrong type in some cases:
///
/// ```
/// Promise(Num, let id_mono = fun x => x in let _ign = id_mono true in id_mono 0)
/// let id_mono = fun x => x in let _ign = id_mono true in id_mono 0 : Num
/// ```
///
/// This specific error stores additionally the [type path](../label/ty_path/index.html) that

8
src/examples/fibo.ncl
View File

@ -1,8 +1,8 @@
let Y = Assume(((Num -> Num) -> Num -> Num) -> Num -> Num, fun f => (fun x => f (x x)) (fun x => f (x x))) in
let dec = Promise(Num -> Num, fun x => x + (-1)) in
let dec : Num -> Num = fun x => x + (-1) in
let or = Assume(Bool -> Bool -> Bool, fun x y => if x then x else y) in
let fibo = Promise(Num -> Num, Y (fun fibo =>
(fun x => if or (isZero x) (isZero (dec x)) then 1 else (fibo (dec x)) + (fibo (dec (dec x)))))) in
let val = Promise(Num, 6) in
let fibo : Num -> Num = Y (fun fibo =>
(fun x => if or (isZero x) (isZero (dec x)) then 1 else (fibo (dec x)) + (fibo (dec (dec x))))) in
let val : Num = 6 in
fibo val

4
src/examples/flatPromise.ncl
View File

@ -1,4 +1,4 @@
let alwaysTrue = fun l t => let boolT = Assume(Bool, t) in
if boolT then boolT else blame l in
let id = Promise(#alwaysTrue -> Bool -> #alwaysTrue, fun b x => if x then b else b) in
Promise(#alwaysTrue -> Bool -> #alwaysTrue, id ) false true
let id : #alwaysTrue -> Bool -> #alwaysTrue = fun b x => if x then b else b in
(id : #alwaysTrue -> Bool -> #alwaysTrue) false true

4
src/examples/flatPromise2.ncl
View File

@ -1,4 +1,4 @@
let alwaysTrue = fun l t => let boolT = Assume(Bool, t) in
if boolT then boolT else blame l in
let id = Promise(#alwaysTrue -> Bool -> #alwaysTrue, fun b x => if x then Assume(#alwaysTrue, true) else b) in
Promise(Bool -> #alwaysTrue, id Assume(#alwaysTrue, false) ) true
let id : #alwaysTrue -> Bool -> #alwaysTrue = fun b x => if x then Assume(#alwaysTrue, true) else b in
(id Assume(#alwaysTrue, false) : Bool -> #alwaysTrue) true

2
src/examples/forall.ncl
View File

@ -1,2 +1,2 @@
let f = Promise(forall a. (forall b. a -> b -> a), fun x y => x) in
let f : forall a. (forall b. a -> b -> a) = fun x y => x in
f

4
src/examples/forall2.ncl
View File

@ -1,2 +1,2 @@
let f = Promise(forall a. (forall b. b -> b) -> a -> a, fun f x => f x) in
Promise(Num, (f Promise(forall b. b -> b, fun x => x)) 3)
let f : forall a. (forall b. b -> b) -> a -> a = fun f x => f x in
(f (fun x => x : forall b. b -> b) 3) : Num

7
src/examples/forall3.ncl
View File

@ -1,3 +1,4 @@
Promise(
((forall a. a -> a) -> Num) -> Num,
fun f => f Promise(forall b. b -> b, fun y => y) ) (fun g => 3)
let f0 : ((forall a. a -> a) -> Num) -> Num = fun f =>
f (fun y => y : forall b. b -> b)
in
f0 (fun g => 3)

6
src/examples/forall4.ncl
View File

@ -1,3 +1,3 @@
let g = Promise(forall a. a -> a, fun y => (fun x => x) y) in
let f = Promise(forall a. a -> a, fun y => g y) in
f
let g : forall a. a -> a = fun y => (fun x => x) y in
let f : forall a. a -> a = fun y => g y in
f

19
src/examples/lists-all-any.ncl
View File

@ -1,7 +1,7 @@
let Y = fun f => (fun x => f (x x)) (fun x => f (x x)) in
let foldr_ =
fun self f acc l =>
if isZero (length l) then acc
if length l == 0 then acc
else
let h = head l in
let t = tail l in
@ -9,20 +9,9 @@ let foldr_ =
f next_acc h
in
let foldr = Y foldr_ in
let and = Promise(Bool -> Bool -> Bool,
fun x y =>
if x then
if y then true else false
else false)
in
let or = Promise(Bool -> Bool -> Bool,
fun x y =>
if x then
true
else
if y then true else false)
in
let and : Bool -> Bool -> Bool = fun x y => x && y in
let or : Bool -> Bool -> Bool = fun x y => x || y in
let all = fun pred l => foldr and true (map pred l) in
let any = fun pred l => foldr or false (map pred l) in
let isZ = fun x => isZero x in
let isZ = fun x => x == 0 in
or (any isZ [1, 1, 1, 1]) (all isZ [0, 0, 0, 0])

2
src/examples/lists-flatten.ncl
View File

@ -9,6 +9,6 @@ let foldl_ =
seq next_acc (self f next_acc t)
in
let foldl = Y foldl_ in
let concat = Promise(List -> List -> List, fun x y => x @ y) in
let concat : List -> List -> List = fun x y => x @ y in
let flatten = foldl concat [] in
flatten [[1,2],[3,4],[]]

8
src/examples/mergeEnriched.ncl
View File

@ -1,7 +1,7 @@
let or = Promise(Bool -> Bool -> Bool, fun a b =>
if a then true else b) in
let and = Promise(Bool -> Bool -> Bool, fun a b =>
if a then (if b then true else false) else false) in
let or : Bool -> Bool -> Bool = fun a b =>
if a then true else b in
let and : Bool -> Bool -> Bool = fun a b =>
if a then (if b then true else false) else false in
let oneOrTwo = fun l x =>
if and (isNum x)
(or (isZero (x + (-1))) (isZero (x + (-2)))) then

4
src/examples/std.ncl
View File

@ -1,4 +1,4 @@
let safePlus = fun x y => Promise(Num, Promise(Num, x) + Promise(Num, y)) in
let safePlus = fun x y => ((x : Num) + (y : Num) : Num) in
let const = fun x y => if isNum y then y else 2 in
let safeAppTwice = fun f y => Promise(Num -> Num, f) ( Promise(Bool -> Num, f) y) in
let safeAppTwice = fun f y => (f : Num -> Num) ((f : Bool -> Num) y) in
safeAppTwice (const 3) true

8
src/examples/std2.ncl
View File

@ -1,7 +1,7 @@
let const = fun x y => x in
let safeAppTwice = fun f y => f (f y) in
let ma = Promise((Dyn -> Num) -> Dyn -> Num, safeAppTwice)
(Promise(Dyn -> Dyn -> Dyn, const) Promise(Bool, 1))
Promise(Bool, true)
let ma = (safeAppTwice : (Dyn -> Num) -> Dyn -> Num)
((const : Dyn -> Dyn -> Dyn) (1 : Bool))
(true : Bool)
in
Promise(Dyn, ma)
ma : Dyn

77
src/grammar.lalrpop
View File

@ -11,8 +11,6 @@ use codespan::FileId;
grammar<'input>(src_id: FileId);
pub Term: RichTerm = SpTerm<RichTerm>;
SpTerm<Rule>: RichTerm =
<l: @L> <t: Rule> <r: @R> => match t {
RichTerm {term: t, pos: _} => RichTerm {
@ -21,6 +19,8 @@ SpTerm<Rule>: RichTerm =
}
};
TypeAnnot: (usize, Types, usize) = ":" <l: @L> <ty: Types> <r: @R> => (l, ty, r);
LeftOp<Op, Current, Previous>: RichTerm =
<t1: Current> <op: Op> <t2: Previous> => mk_term::op2(op, t1,
t2);
@ -29,24 +29,45 @@ LeftOpLazy<Op, Current, Previous>: RichTerm =
<t1: Current> <op: Op> <t2: Previous> =>
mk_app!(Term::Op1(op, t1), t2);
pub Term: RichTerm = {
SpTerm<RichTerm>,
SpTerm<TypedTerm>,
};
TypedTerm: RichTerm = {
<t: SpTerm<RichTerm>> <ann: TypeAnnot> => {
let (l, ty, r) = ann;
RichTerm::from(Term::Promise(ty.clone(), mk_label(ty, src_id, l, r), t))
}
};
RichTerm: RichTerm = {
<l: @L> "fun" <ps:Pattern+> "=>" <t: SpTerm<Term>> <r: @R> => {
<l: @L> "fun" <ps:Pattern+> "=>" <t: SpTerm<RichTerm>> <r: @R> => {
let pos = Some(mk_span(src_id, l, r));
ps.into_iter().rev().fold(t, |t, p| RichTerm {
term: Box::new(Term::Fun(p, t)),
pos: pos.clone()
})
},
"let" <id:Ident> "=" <t1:SpTerm<Term>> "in" <t2:SpTerm<Term>> =>
mk_term::let_in(id, t1, t2),
"if" <b:SpTerm<Term>> "then" <t:SpTerm<Term>> "else" <e:SpTerm<Term>> =>
"let" <id:Ident> <ann: TypeAnnot?> "=" <t1: Term> "in" <t2:SpTerm<RichTerm>> => {
let t1 = if let Some((l, ty, r)) = ann {
let pos = t1.pos.clone();
RichTerm::new(Term::Promise(ty.clone(), mk_label(ty, src_id, l, r), t1), pos)
}
else {
t1
};
mk_term::let_in(id, t1, t2)
},
"if" <b:Term> "then" <t:Term> "else" <e:SpTerm<RichTerm>> =>
mk_app!(Term::Op1(UnaryOp::Ite(), b), t, e),
"import" <s: Str> => RichTerm::from(Term::Import(s)),
SpTerm<InfixExpr>,
};
Applicative: RichTerm = {
<t1:SpTerm< Applicative>> <t2: SpTerm<Atom>> => mk_app!(t1, t2),
<t1:SpTerm<Applicative>> <t2: SpTerm<Atom>> => mk_app!(t1, t2),
<op: UOp> <t: SpTerm<Atom>> => mk_term::op1(op, t),
<op: BOpPre> <t1: SpTerm<Atom>> <t2: SpTerm<Atom>> => mk_term::op2(op, t1, t2),
SpTerm<RecordOperationChain>,
@ -62,24 +83,22 @@ RecordOperationChain: RichTerm = {
<t: SpTerm<RecordOperand>> "." <id: Ident> => mk_term::op1(UnaryOp::StaticAccess(id), t),
<t: SpTerm<RecordOperand>> ".$" <t_id: SpTerm<Atom>> => mk_term::op2(BinaryOp::DynAccess(), t_id, t),
<t: SpTerm<RecordOperand>> "-$" <t_id: SpTerm<Atom>> => mk_term::op2(BinaryOp::DynRemove(), t_id, t),
<r: SpTerm<RecordOperand>> "$[" <id: SpTerm<Term>> "=" <t: SpTerm<Term>> "]" =>
<r: SpTerm<RecordOperand>> "$[" <id: Term> "=" <t: Term> "]" =>
mk_term::op2(BinaryOp::DynExtend(t), id, r),
};
Atom: RichTerm = {
"(" <SpTerm<Term>> ")",
<l: @L> "Promise(" <ty: Types> "," <t: SpTerm<Term>> ")" <r: @R> =>
RichTerm::from(Term::Promise(ty.clone(), mk_label(ty, src_id, l, r), t)),
<l: @L> "Assume(" <ty: Types> "," <t: SpTerm<Term>> ")" <r: @R> =>
"(" <Term> ")",
<l: @L> "Assume(" <ty: Types> "," <t: Term> ")" <r: @R> =>
RichTerm::from(Term::Assume(ty.clone(), mk_label(ty, src_id, l, r), t)),
<l: @L> "Contract(" <ty: Types> ")" <r: @R> =>
RichTerm::from(Term::Contract(ty.clone(), mk_label(ty, src_id, l, r))),
"Default(" <t: SpTerm<Term>> ")" => RichTerm::from(Term::DefaultValue(t)),
<l: @L> "ContractDefault(" <ty: Types> "," <t: SpTerm<Term>> ")" <r: @R> =>
"Default(" <t: Term> ")" => RichTerm::from(Term::DefaultValue(t)),
<l: @L> "ContractDefault(" <ty: Types> "," <t: Term> ")" <r: @R> =>
RichTerm::from(Term::ContractWithDefault(ty.clone(),
mk_label(ty, src_id, l, r), t)
),
"Docstring(" <s: Str> "," <t: SpTerm<Term>> ")" => RichTerm::from(Term::Docstring(s, t)),
"Docstring(" <s: Str> "," <t: Term> ")" => RichTerm::from(Term::Docstring(s, t)),
"num literal" => RichTerm::from(Term::Num(<>)),
Bool => RichTerm::from(Term::Bool(<>)),
<StrChunks>,
@ -105,7 +124,7 @@ Atom: RichTerm = {
RichTerm::from(Term::Op2(BinaryOp::DynExtend(t), id_t, rec))
})
},
"[" <terms: (SpTerm<Atom> ",")*> <last: SpTerm<Term>?> "]" => {
"[" <terms: (SpTerm<Atom> ",")*> <last: Term?> "]" => {
let terms : Vec<RichTerm> = terms.into_iter()
.map(|x| x.0)
.chain(last.into_iter()).collect();
@ -114,10 +133,28 @@ Atom: RichTerm = {
};
RecordField: Either<(Ident, RichTerm), (RichTerm, RichTerm)> = {
<id: Ident> "=" <t: SpTerm<Term>> =>
Either::Left((id, t)),
"$" <id: SpTerm<Term>> "=" <t: SpTerm<Term>> =>
Either::Right((id, t)),
<id: Ident> <ann: TypeAnnot?> "=" <t: Term> => {
let t = if let Some((l, ty, r)) = ann {
let pos = t.pos.clone();
RichTerm::new(Term::Promise(ty.clone(), mk_label(ty, src_id, l, r), t), pos)
}
else {
t
};
Either::Left((id, t))
},
"$" <id: SpTerm<Atom>> <ann: TypeAnnot?> "=" <t: Term> => {
let t = if let Some((l, ty, r)) = ann {
let pos = t.pos.clone();
RichTerm::new(Term::Promise(ty.clone(), mk_label(ty, src_id, l, r), t), pos)
}
else {
t
};
Either::Right((id, t))
}
}
Pattern: Ident = {

53
src/program.rs
View File

@ -599,8 +599,8 @@ g true",
#[test]
fn type_contracts() {
let res = eval_string(
"let safePlus = Promise(Num -> Num -> Num , fun x => fun y => x + y) in
safePlus Promise(Num , 54) Promise(Num , 6)",
"let safePlus : Num -> Num -> Num = fun x => fun y => x + y in
safePlus (54 : Num) (6 : Num)",
);
assert_eq!(Ok(Term::Num(60.)), res);
@ -610,13 +610,13 @@ safePlus Promise(Num , 54) Promise(Num , 6)",
fn fibonacci() {
let res = eval_string(
"let Y = Assume(((Num -> Num) -> Num -> Num) -> Num -> Num, fun f => (fun x => f (x x)) (fun x => f (x x))) in
let dec = Promise(Num -> Num, fun x => x + (-1)) in
let or = Promise(Bool -> Bool -> Bool, fun x => fun y => if x then x else y) in
let dec : Num -> Num = fun x => x + (-1) in
let or : Bool -> Bool -> Bool = fun x => fun y => if x then x else y in
let fibo = Promise(Num -> Num, Y (fun fibo =>
(fun x => if or (isZero x) (isZero (dec x)) then 1 else (fibo (dec x)) + (fibo (dec (dec x)))))) in
let val = Promise(Num, 4) in
fibo val",
let fibo : Num -> Num = Y (fun fibo =>
(fun x => if or (isZero x) (isZero (dec x)) then 1 else (fibo (dec x)) + (fibo (dec (dec x))))) in
let val : Num = 4 in
fibo val",
);
assert_eq!(Ok(Term::Num(5.)), res);
@ -624,12 +624,7 @@ fibo val",
#[test]
fn promise_fail() {
let res = eval_string(
"let bool = fun l t => if isBool t then t else blame l in
Promise(Bool, 5)
",
);
let res = eval_string("let bool = fun l t => if isBool t then t else blame l in 5 : Bool");
if let Ok(_) = res {
panic!("This expression should return an error!");
@ -715,35 +710,35 @@ Assume(#alwaysTrue -> #alwaysFalse, not ) true
#[test]
fn enum_simple() {
let res = eval_string("Promise(<foo, bar>, `foo)");
let res = eval_string("`foo : <foo, bar>");
assert_eq!(res, Ok(Term::Enum(Ident("foo".to_string()))));
let res = eval_string("Promise(forall r. <foo, bar | r>, `bar)");
let res = eval_string("`bar : forall r. <foo, bar | r>");
assert_eq!(res, Ok(Term::Enum(Ident("bar".to_string()))));
eval_string("Promise(<foo, bar>, `far)").unwrap_err();
eval_string("`far : <foo, bar>").unwrap_err();
}
#[test]
fn enum_complex() {
let res = eval_string(
"let f = Promise(forall r. <foo, bar | r> -> Num,
fun x => switch { foo => 1, bar => 2, _ => 3, } x) in
f `bar",
"let f : forall r. <foo, bar | r> -> Num =
fun x => switch { foo => 1, bar => 2, _ => 3, } x in
f `bar",
);
assert_eq!(res, Ok(Term::Num(2.)));
let res = eval_string(
"let f = Promise(forall r. <foo, bar | r> -> Num,
fun x => switch { foo => 1, bar => 2, _ => 3, } x) in
f `boo",
"let f : forall r. <foo, bar | r> -> Num =
fun x => switch { foo => 1, bar => 2, _ => 3, } x in
f `boo",
);
assert_eq!(res, Ok(Term::Num(3.)));
eval_string(
"let f = Promise(<foo, bar> -> Num,
fun x => switch { foo => 1, bar => 2, } x) in
f `boo",
"let f : <foo, bar> -> Num =
fun x => switch { foo => 1, bar => 2, } x in
f `boo",
)
.unwrap_err();
@ -751,7 +746,7 @@ Assume(#alwaysTrue -> #alwaysFalse, not ) true
assert_eq!(
eval_string(
"let x = 3 in
switch { foo => 1, _ => x, } (3 + 2)"
switch { foo => 1, _ => x, } (3 + 2)"
),
Ok(Term::Num(3.))
);
@ -913,11 +908,11 @@ Assume(#alwaysTrue -> #alwaysFalse, not ) true
f next_acc h
in
let foldr = Y foldr_ in
let and = Promise(Bool -> Bool -> Bool,
let and : Bool -> Bool -> Bool =
fun x => fun y =>
if x then
if y then true else false
else false)
else false
in
let all = fun pred => fun l => foldr and true (map pred l) in
let isZ = fun x => isZero x in

266
src/typecheck.rs
View File

@ -4,7 +4,8 @@
//!
//! Typechecking can be made in to different modes:
//! - **Strict**: correspond to traditional typechecking in strongly, statically typed languages.
//! This happens inside a `Promise` block.
//! This happens inside a `Promise` block. Promise block are introduced by the typing operator `:`,
//! as in `1 + 1 : Num` or `let f : Num -> Num = fun x => x + 1 in ..`.
//! - **Non strict**: do not enforce any typing, but still store the annotations of let bindings in
//! the environment, and continue to traverse the AST looking for other `Promise` blocks to
//! typecheck.
@ -22,7 +23,7 @@
//!
//! ```
//! // Rejected
//! Promise(Num, let id = fun x => x in seq (id "a") (id 5))
//! let id = fun x => x in seq (id "a") (id 5) : Num
//! ```
//!
//! Indeed, `id` is given the type `_a -> _a`, where `_a` is a unification variable, but is not
@ -35,7 +36,7 @@
//!
//! ```
//! // Accepted
//! Promise(Num, let id = Promise(forall a. a -> a, fun x => x) in seq (id "a") (id 5))
//! let id : forall a. a -> a = fun x => x in seq (id "a") (id 5) : Num
//! ```
//!
//! In non-strict mode, all let-bound expressions are given type `Dyn`, unless annotated.
@ -1790,87 +1791,86 @@ mod tests {
)
.unwrap_err();
parse_and_typecheck("Promise(Str, \"hello\")").unwrap();
parse_and_typecheck("Promise(Num, \"hello\")").unwrap_err();
parse_and_typecheck("\"hello\" : Str").unwrap();
parse_and_typecheck("\"hello\" : Num").unwrap_err();
}
#[test]
fn promise_complicated() {
// Inside Promises we typecheck strictly
parse_and_typecheck("(fun x => if x then x + 1 else 34) false").unwrap();
parse_and_typecheck("Promise(Bool -> Num, fun x => if x then x + 1 else 34) false")
parse_and_typecheck("let f : Bool -> Num = fun x => if x then x + 1 else 34 in f false")
.unwrap_err();
// not annotated let bindings type to Dyn
parse_and_typecheck(
"let id = Promise(Num -> Num, fun x => x) in
Promise(Num, id 4)",
"let id : Num -> Num = fun x => x in
(id 4 : Num)",
)
.unwrap();
parse_and_typecheck(
"let id = fun x => x in
Promise(Num, id 4)",
(id 4 : Num)",
)
.unwrap_err();
// lambdas don't annotate to Dyn
parse_and_typecheck("(fun id => Promise(Num, id 4)) (fun x => x)").unwrap();
parse_and_typecheck("(fun id => (id 4 : Num)) (fun x => x)").unwrap();
// But they are not polymorphic
parse_and_typecheck("(fun id => Promise(Num, id 4) + Promise(Bool, id true)) (fun x => x)")
parse_and_typecheck("(fun id => (id 4 : Num) + (id true : Bool)) (fun x => x)")
.unwrap_err();
// Non strict zones don't unify
parse_and_typecheck("(fun id => (id 4) + Promise(Bool, id true)) (fun x => x)").unwrap();
parse_and_typecheck("(fun id => (id 4) + (id true: Bool)) (fun x => x)").unwrap();
// We can typecheck any contract
parse_and_typecheck(
"let alwaysTrue = fun l t => if t then t else blame l in
Promise(#alwaysTrue -> #alwaysTrue, fun x => x)",
(fun x => x) : #alwaysTrue -> #alwaysTrue",
)
.unwrap();
// Only if they're named the same way
parse_and_typecheck("Promise(#(fun l t => t) -> #(fun l t => t), fun x => x)").unwrap_err();
parse_and_typecheck("(fun x => x) : #(fun l t => t) -> #(fun l t => t)").unwrap_err();
}
#[test]
fn simple_forall() {
parse_and_typecheck(
"let f = Promise(forall a. a -> a, fun x => x) in
Promise(Num, if (f true) then (f 2) else 3)",
"let f : forall a. a -> a = fun x => x in
(if (f true) then (f 2) else 3) : Num",
)
.unwrap();
parse_and_typecheck(
"let f = Promise(forall a. (forall b. a -> b -> a), fun x y => x) in
Promise(Num, if (f true 3) then (f 2 false) else 3)",
"let f : forall a. (forall b. a -> b -> a) = fun x y => x in
(if (f true 3) then (f 2 false) else 3) : Num",
)
.unwrap();
parse_and_typecheck(
"let f = Promise(forall a. (forall b. b -> b) -> a -> a, fun f x => f x) in
f Promise(forall y. y -> y, fun z => z)",
"let f : forall a. (forall b. b -> b) -> a -> a = fun f x => f x in
f (fun z => z : forall y. y -> y)",
)
.unwrap();
parse_and_typecheck(
"let f = Promise(forall a. (forall b. a -> b -> a), fun x y => y) in
"let f : forall a. (forall b. a -> b -> a) = fun x y => y in
f",
)
.unwrap_err();
parse_and_typecheck(
"Promise(
((forall a. a -> a) -> Num) -> Num,
fun f => let g = Promise(forall b. b -> b, fun y => y) in f g)
"((fun f => let g : forall b. b -> b = fun y => y in f g)
: ((forall a. a -> a) -> Num) -> Num)
(fun x => 3)",
)
.unwrap_err();
parse_and_typecheck(
"let g = Promise(Num -> Num, fun x => x) in
let f = Promise(forall a. a -> a, fun x => g x) in
f",
"let g : Num -> Num = fun x => x in
let f : forall a. a -> a = fun x => g x in
f",
)
.unwrap_err();
}
@ -1878,97 +1878,89 @@ mod tests {
#[test]
fn forall_nested() {
parse_and_typecheck(
"let f = Promise(forall a. a -> a, let g = Assume(forall a. (a -> a), fun x => x) in g) in
Promise(Num, if (f true) then (f 2) else 3)",
"let f : forall a. a -> a = let g = Assume(forall a. (a -> a), fun x => x) in g in
(if (f true) then (f 2) else 3) : Num",
)
.unwrap();
parse_and_typecheck(
"let f = Promise(forall a. a -> a, let g = Promise(forall a. (a -> a), fun x => x) in g g) in
Promise(Num, if (f true) then (f 2) else 3)",
"let f : forall a. a -> a = let g = Assume(forall a. (a -> a), fun x => x) in g g in
(if (f true) then (f 2) else 3) : Num",
)
.unwrap();
parse_and_typecheck(
"let f = Promise(forall a. a -> a, let g = Promise(forall a. (forall b. (b -> (a -> a))), fun y x => x) in g 0) in
Promise(Num, if (f true) then (f 2) else 3)",
"let f : forall a. a -> a = let g : forall a. (forall b. (b -> (a -> a))) = fun y x => x in g 0 in
(if (f true) then (f 2) else 3) : Num",
)
.unwrap();
}
#[test]
fn enum_simple() {
parse_and_typecheck("Promise(<bla>, `bla)").unwrap();
parse_and_typecheck("Promise(<bla>, `blo)").unwrap_err();
parse_and_typecheck("`bla : <bla>").unwrap();
parse_and_typecheck("`blo : <bla>").unwrap_err();
parse_and_typecheck("Promise(<bla, blo>, `blo)").unwrap();
parse_and_typecheck("Promise(forall r. <bla | r>, `bla)").unwrap();
parse_and_typecheck("Promise(forall r. <bla, blo | r>, `bla)").unwrap();
parse_and_typecheck("`blo : <bla, blo>").unwrap();
parse_and_typecheck("`bla : forall r. <bla | r>").unwrap();
parse_and_typecheck("`bla : forall r. <bla, blo | r>").unwrap();
parse_and_typecheck("Promise(Num, switch { bla => 3, } `bla)").unwrap();
parse_and_typecheck("Promise(Num, switch { bla => 3, } `blo)").unwrap_err();
parse_and_typecheck("(switch { bla => 3, } `bla) : Num").unwrap();
parse_and_typecheck("(switch { bla => 3, } `blo) : Num").unwrap_err();
parse_and_typecheck("Promise(Num, switch { bla => 3, _ => 2, } `blo)").unwrap();
parse_and_typecheck("Promise(Num, switch { bla => 3, ble => true, } `bla)").unwrap_err();
parse_and_typecheck("(switch { bla => 3, _ => 2, } `blo) : Num").unwrap();
parse_and_typecheck("(switch { bla => 3, ble => true, } `bla) : Num").unwrap_err();
}
#[test]
fn enum_complex() {
parse_and_typecheck("Promise(<bla, ble> -> Num, fun x => switch {bla => 1, ble => 2,} x)")
parse_and_typecheck("(fun x => switch {bla => 1, ble => 2,} x) : <bla, ble> -> Num")
.unwrap();
parse_and_typecheck(
"Promise(<bla, ble> -> Num,
fun x => switch {bla => 1, ble => 2, bli => 4,} x)",
"(fun x => switch {bla => 1, ble => 2, bli => 4,} x) : <bla, ble> -> Num",
)
.unwrap_err();
parse_and_typecheck(
"Promise(<bla, ble> -> Num,
fun x => switch {bla => 1, ble => 2, bli => 4,} (embed bli x))",
"(fun x => switch {bla => 1, ble => 2, bli => 4,} (embed bli x)) : <bla, ble> -> Num",
)
.unwrap();
parse_and_typecheck(
"Promise(Num,
(fun x =>
"(fun x =>
(switch {bla => 3, bli => 2,} x) +
(switch {bli => 6, bla => 20,} x) ) `bla)",
(switch {bli => 6, bla => 20,} x) ) `bla : Num",
)
.unwrap();
// TODO typecheck this, I'm not sure how to do it with row variables
parse_and_typecheck(
"Promise(Num,
(fun x =>
"(fun x =>
(switch {bla => 3, bli => 2,} x) +
(switch {bla => 6, blo => 20,} x) ) `bla)",
(switch {bla => 6, blo => 20,} x) ) `bla : Num",
)
.unwrap_err();
parse_and_typecheck(
"let f = Promise(
forall r. <blo, ble | r> -> Num,
fun x => (switch {blo => 1, ble => 2, _ => 3, } x ) ) in
Promise(Num, f `bli)",
"let f : forall r. <blo, ble | r> -> Num =
fun x => (switch {blo => 1, ble => 2, _ => 3, } x) in
f `bli : Num",
)
.unwrap();
parse_and_typecheck(
"let f = Promise(
forall r. <blo, ble, | r> -> Num,
fun x => (switch {blo => 1, ble => 2, bli => 3, } x ) ) in
"let f : forall r. <blo, ble, | r> -> Num =
fun x => (switch {blo => 1, ble => 2, bli => 3, } x) in
f",
)
.unwrap_err();
parse_and_typecheck(
"let f = Promise(
forall r. (forall p. <blo, ble | r> -> <bla, bli | p> ),
fun x => (switch {blo => `bla, ble => `bli, _ => `bla, } x ) ) in
"let f : forall r. (forall p. <blo, ble | r> -> <bla, bli | p>) =
fun x => (switch {blo => `bla, ble => `bli, _ => `bla, } x) in
f `bli",
)
.unwrap();
parse_and_typecheck(
"let f = Promise(
forall r. (forall p. <blo, ble | r> -> <bla, bli | p> ),
fun x => (switch {blo => `bla, ble => `bli, _ => `blo, } x ) ) in
"let f : forall r. (forall p. <blo, ble | r> -> <bla, bli | p>) =
fun x => (switch {blo => `bla, ble => `bli, _ => `blo, } x) in
f `bli",
)
.unwrap_err();
@ -1976,114 +1968,96 @@ mod tests {
#[test]
fn static_record_simple() {
parse_and_typecheck("Promise({bla : Num, }, { bla = 1; })").unwrap();
parse_and_typecheck("Promise({bla : Num, }, { bla = true; })").unwrap_err();
parse_and_typecheck("Promise({bla : Num, }, { blo = 1; })").unwrap_err();
parse_and_typecheck("{bla = 1} : {bla : Num}").unwrap();
parse_and_typecheck("{bla = true} : {bla : Num}").unwrap_err();
parse_and_typecheck("{blo = 1} : {bla : Num}").unwrap_err();
parse_and_typecheck("Promise({bla : Num, blo : Bool}, { blo = true; bla = 1; })").unwrap();
parse_and_typecheck("{blo = true; bla = 1} : {bla : Num, blo : Bool}").unwrap();
parse_and_typecheck("Promise(Num, { blo = 1; }.blo)").unwrap();
parse_and_typecheck("Promise(Num, { bla = true; blo = 1; }.blo)").unwrap();
parse_and_typecheck("Promise(Bool, { blo = 1; }.blo)").unwrap_err();
parse_and_typecheck("{blo = 1}.blo : Num").unwrap();
parse_and_typecheck("{bla = true; blo = 1}.blo : Num").unwrap();
parse_and_typecheck("{blo = 1}.blo : Bool").unwrap_err();
parse_and_typecheck(
"let r = Promise({bla : Bool, blo : Num}, {blo = 1; bla = true; }) in
Promise(Num, if r.bla then r.blo else 2)",
"let r : {bla : Bool, blo : Num} = {blo = 1; bla = true; } in
(if r.bla then r.blo else 2) : Num",
)
.unwrap();
// It worked at first try :O
parse_and_typecheck(
"let f = Promise(
forall a. (forall r. {bla : Bool, blo : a, ble : a | r} -> a),
fun r => if r.bla then r.blo else r.ble)
"let f : forall a. (forall r. {bla : Bool, blo : a, ble : a | r} -> a) =
fun r => if r.bla then r.blo else r.ble
in
Promise(Num,
if (f {bla = true; blo = false; ble = true; blip = 1; }) then
(f {bla = true; blo = 1; ble = 2; blip = `blip; })
else
(f {bla = true; blo = 3; ble = 4; bloppo = `bloppop; }))",
(if (f {bla = true; blo = false; ble = true; blip = 1; }) then
(f {bla = true; blo = 1; ble = 2; blip = `blip; })
else
(f {bla = true; blo = 3; ble = 4; bloppo = `bloppop; })) : Num",
)
.unwrap();
parse_and_typecheck(
"let f = Promise(
forall a. (forall r. {bla : Bool, blo : a, ble : a | r} -> a),
fun r => if r.bla then r.blo else r.ble)
"let f : forall a. (forall r. {bla : Bool, blo : a, ble : a | r} -> a) =
fun r => if r.bla then r.blo else r.ble
in
Promise(Num,
f {bla = true; blo = 1; ble = true; blip = `blip; })
",
(f {bla = true; blo = 1; ble = true; blip = `blip}) : Num",
)
.unwrap_err();
parse_and_typecheck(
"let f = Promise(
forall a. (forall r. {bla : Bool, blo : a, ble : a | r} -> a),
fun r => if r.bla then (r.blo + 1) else r.ble)
"let f : forall a. (forall r. {bla : Bool, blo : a, ble : a | r} -> a) =
fun r => if r.bla then (r.blo + 1) else r.ble
in
Promise(Num,
f {bla = true; blo = 1; ble = 2; blip = `blip; })
",
(f {bla = true; blo = 1; ble = 2; blip = `blip; }) : Num",
)
.unwrap_err();
}
#[test]
fn dynamic_record_simple() {
parse_and_typecheck("Promise({ _ : Num }, { $(if true then \"foo\" else \"bar\") = 2; } )")
parse_and_typecheck("{ $(if true then \"foo\" else \"bar\") = 2; } : {_ : Num}").unwrap();
parse_and_typecheck("({ $(if true then \"foo\" else \"bar\") = 2; }.$(\"bla\")) : Num")
.unwrap();
parse_and_typecheck(
"Promise(Num, { $(if true then \"foo\" else \"bar\") = 2; }.$(\"bla\"))",
)
.unwrap();
parse_and_typecheck(
"Promise(
Num,
{ $(if true then \"foo\" else \"bar\") = 2; $(\"foo\") = true; }.$(\"bla\"))",
"({ $(if true then \"foo\" else \"bar\") = 2; $(\"foo\") = true; }.$(\"bla\")) : Num",
)
.unwrap_err();
parse_and_typecheck("Promise( { _ : Num}, { foo = 3; bar = 4; })").unwrap();
parse_and_typecheck("{ foo = 3; bar = 4; } : {_ : Num}").unwrap();
}
#[test]
fn seq() {
parse_and_typecheck("Promise(Num, seq false 1)").unwrap();
parse_and_typecheck("Promise(forall a. (forall b. a -> b -> b), fun x y => seq x y)")
.unwrap();
parse_and_typecheck("let xDyn = false in let yDyn = 1 in Promise(Dyn, seq xDyn yDyn)")
.unwrap();
parse_and_typecheck("seq false 1 : Num").unwrap();
parse_and_typecheck("(fun x y => seq x y) : forall a. (forall b. a -> b -> b)").unwrap();
parse_and_typecheck("let xDyn = false in let yDyn = 1 in (seq xDyn yDyn : Dyn)").unwrap();
}
#[test]
fn simple_list() {
parse_and_typecheck("[1, \"2\", false]").unwrap();
parse_and_typecheck("Promise(List, [\"a\", 3, true])").unwrap();
parse_and_typecheck("Promise(List, [Promise(forall a. a -> a, fun x => x), 3, true])")
.unwrap();
parse_and_typecheck("Promise(forall a. a -> List, fun x => [x])").unwrap();
parse_and_typecheck("[\"a\", 3, true] : List").unwrap();
parse_and_typecheck("[(fun x => x : forall a. a -> a), true] : List").unwrap();
parse_and_typecheck("fun x => [x] : forall a. a -> List").unwrap();
parse_and_typecheck("[1, Promise(Num, \"2\"), false]").unwrap_err();
parse_and_typecheck("Promise(List, [Promise(String,1), true, \"b\"])").unwrap_err();
parse_and_typecheck("Promise(Num, [1, 2, \"3\"])").unwrap_err();
parse_and_typecheck("[1, (\"2\" : Num), false]").unwrap_err();
parse_and_typecheck("[(1 : String), true, \"b\"] : List").unwrap_err();
parse_and_typecheck("[1, 2, \"3\"] : Num").unwrap_err();
}
#[test]
fn lists_operations() {
parse_and_typecheck("Promise(List -> List, fun l => tail l)").unwrap();
parse_and_typecheck("Promise(List -> Dyn, fun l => head l)").unwrap();
parse_and_typecheck(
"Promise(forall a. (forall b. (a -> b) -> List -> List), fun f l => map f l)",
)
.unwrap();
parse_and_typecheck("Promise(List -> List -> List, fun l1 => fun l2 => l1 @ l2)").unwrap();
parse_and_typecheck("Promise(Num -> List -> Dyn , fun i l => elemAt l i)").unwrap();
parse_and_typecheck("fun l => tail l : List -> List").unwrap();
parse_and_typecheck("fun l => head l : List -> Dyn").unwrap();
parse_and_typecheck("fun f l => map f l : forall a. (forall b. (a -> b) -> List -> List)")
.unwrap();
parse_and_typecheck("(fun l1 => fun l2 => l1 @ l2) : List -> List -> List").unwrap();
parse_and_typecheck("(fun i l => elemAt l i) : Num -> List -> Dyn ").unwrap();
parse_and_typecheck("Promise(forall a. (List -> a), fun l => head l)").unwrap_err();
parse_and_typecheck("(fun l => head l) : forall a. (List -> a)").unwrap_err();
parse_and_typecheck(
"Promise(forall a. (forall b. (a -> b) -> List -> b), fun f l => elemAt (map f l) 0)",
"(fun f l => elemAt (map f l) 0) : forall a. (forall b. (a -> b) -> List -> b)",
)
.unwrap_err();
}
@ -2091,8 +2065,8 @@ mod tests {
#[test]
fn imports() {
let mut resolver = SimpleResolver::new();
resolver.add_source(String::from("good"), String::from("Promise(Num, 1 + 1)"));
resolver.add_source(String::from("bad"), String::from("Promise(Num, false)"));
resolver.add_source(String::from("good"), String::from("1 + 1 : Num"));
resolver.add_source(String::from("bad"), String::from("false : Num"));
resolver.add_source(
String::from("proxy"),
String::from("let x = import \"bad\" in x"),
@ -2124,30 +2098,28 @@ mod tests {
#[test]
fn recursive_records() {
parse_and_typecheck("Promise({a : Num, b : Num}, { a = Promise(Num,1); b = a + 1})")
.unwrap();
parse_and_typecheck("Promise({a : Num, b : Num}, { a = Promise(Num,true); b = a + 1})")
.unwrap_err();
parse_and_typecheck("Promise({a : Num, b : Bool}, { a = 1; b = Promise(Bool, a) } )")
.unwrap_err();
parse_and_typecheck("Promise({a : Num}, { a = Promise(Num, 1 + a) })").unwrap();
parse_and_typecheck("{a : Num = 1; b = a + 1} : {a : Num, b : Num}").unwrap();
parse_and_typecheck("{a : Num = true; b = a + 1} : {a : Num, b : Num}").unwrap_err();
parse_and_typecheck("{a = 1; b : Bool = a} : {a : Num, b : Bool}").unwrap_err();
parse_and_typecheck("{a : Num = 1 + a} : {a : Num}").unwrap();
}
#[test]
fn let_inference() {
parse_and_typecheck("Promise(Num, let x = 1 + 2 in let f = fun x => x + 1 in f x)")
.unwrap();
parse_and_typecheck("Promise(Num, let x = 1 + 2 in let f = fun x => x ++ \"a\" in f x)")
parse_and_typecheck("(let x = 1 + 2 in let f = fun x => x + 1 in f x) : Num").unwrap();
parse_and_typecheck("(let x = 1 + 2 in let f = fun x => x ++ \"a\" in f x) : Num")
.unwrap_err();
// Fields in recursive records are treated in the type environment in the same way as let-bound expressions
parse_and_typecheck("Promise({a : Num, b : Num}, { a = 1; b = 1 + a })").unwrap();
parse_and_typecheck("{a = 1; b = 1 + a} : {a : Num, b : Num}").unwrap();
parse_and_typecheck(
"Promise({f : Num -> Num}, { f = fun x => if isZero x then 1 else 1 + (f (x + (-1)));})"
).unwrap();
"{ f = fun x => if isZero x then 1 else 1 + (f (x + (-1)));} : {f : Num -> Num}",
)
.unwrap();
parse_and_typecheck(
"Promise({f : Num -> Num}, { f = fun x => if isZero x then false else 1 + (f (x + (-1)))})"
).unwrap_err();
"{ f = fun x => if isZero x then false else 1 + (f (x + (-1)))} : {f : Num -> Num}",
)
.unwrap_err();
}
/// Regression test following [#144](https://github.com/tweag/nickel/issues/144). Check that
@ -2173,19 +2145,19 @@ mod tests {
let mut res = parse_and_typecheck(
"let extend = Assume(forall c. { | c} -> {a: Str | c}, 0) in
Promise(Num, let bad = extend {a = 1;} in 0)",
(let bad = extend {a = 1;} in 0) : Num",
);
assert_row_conflict(res);
parse_and_typecheck(
"let extend = Assume(forall c. { | c} -> {a: Str | c}, 0) in
let remove = Assume(forall c. {a: Str | c} -> { | c}, 0) in
Promise(Num, let good = remove (extend {}) in 0)",
(let good = remove (extend {}) in 0) : Num",
)
.unwrap();
res = parse_and_typecheck(
"let remove = Assume(forall c. {a: Str | c} -> { | c}, 0) in
Promise(Num, let bad = remove (remove {a = \"a\"}) in 0)",
(let bad = remove (remove {a = \"a\"}) in 0) : Num",
);
assert_row_conflict(res);
}

29
stdlib/lists.ncl
View File

@ -1,37 +1,38 @@
{
lists = {
concat = Promise(List -> List -> List, fun l1 l2 => l1 @ l2);
concat : List -> List -> List = fun l1 l2 => l1 @ l2;
foldl = Promise(forall a. (a -> Dyn -> a) -> a -> List -> a,
foldl : forall a. (a -> Dyn -> a) -> a -> List -> a =
fun f fst l =>
if length l == 0 then
fst
else
let rest = foldl f fst (tail l) in
seq rest (f rest (head l)));
seq rest (f rest (head l));
fold = Promise(forall a. (Dyn -> a -> a) -> List -> a -> a,
fold : forall a. (Dyn -> a -> a) -> List -> a -> a =
fun f l fst =>
if length l == 0 then
fst
else
f (head l) (fold f (tail l) fst));
f (head l) (fold f (tail l) fst);
cons = Promise(Dyn -> List -> List, fun x l => [x] @ l);
cons : Dyn -> List -> List = fun x l => [x] @ l;
filter = Promise((Dyn -> Bool) -> List -> List,
filter : (Dyn -> Bool) -> List -> List =
fun pred l =>
fold (fun x acc => if pred x then acc @ [x] else acc) l []);
fold (fun x acc => if pred x then acc @ [x] else acc) l [];
flatten = Promise(List -> List, fun l =>
fold (fun l acc => acc @ Assume(List, l)) l []);
flatten : List -> List =
fun l =>
fold (fun l acc => acc @ Assume(List, l)) l [];
all = Promise((Dyn -> Bool) -> List -> Bool,
all : (Dyn -> Bool) -> List -> Bool =
fun pred l =>
fold (fun x acc => if pred x then acc else false) l true);
fold (fun x acc => if pred x then acc else false) l true;
any = Promise((Dyn -> Bool) -> List -> Bool,
any : (Dyn -> Bool) -> List -> Bool =
fun pred l =>
fold (fun x acc => if pred x then true else acc) l false);
fold (fun x acc => if pred x then true else acc) l false;
}
}