PTV/radn-rs
1
1
Fork 0
Code Issues 3 Pull Requests Packages Projects Releases Wiki Activity

impls in tests

Browse Source
This commit is contained in:
AF 2023-03-26 18:49:22 +00:00
parent 5d9a0a10df
commit 504c0abc4c
2 changed files with 49 additions and 114 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
src/func/test_suite.rs
View File

@ -9,10 +9,10 @@ pub trait FunctorTestSuite: WeakFunctor + Eqr {
pub fn functor_follows_laws<T: Functor + FunctorTestSuite>() -> R {
let mut res = R::default();
T::sample(|pa| {
res += fmap_respects_identity::<T, _, _>(|| pa(2));
res += fmap_respects_identity::<T, _>(|| pa(2));
});
T::sample(|pa| {
res += fmap_respects_composition::<T, _, _, _, _, _, _>(|x| x + 5, |x| x + 3, || pa(2));
res += fmap_respects_composition::<T, _, _, _>(|x| x + 5, |x| x + 3, || pa(2));
});
res
}
@ -20,12 +20,12 @@ pub fn functor_follows_laws<T: Functor + FunctorTestSuite>() -> R {
pub fn applicative_follows_laws<T: Applicative + FunctorTestSuite>() -> R {
let mut res = functor_follows_laws::<T>();
T::sample(|pa| {
res += seq_respects_identity::<T, _, _>(|| pa(2));
res += seq_respects_identity::<T, _>(|| pa(2));
});
T::sample(|pa| {
T::sample(|pg| {
T::sample(|pf| {
res += seq_respects_composition::<T, _, _, _, _, _, _, _, _>(
res += seq_respects_composition::<T, _, _, _, _, _>(
|| pf(|x| x + 5),
|| pg(|x| x + 3),
|| pa(2),
@ -33,21 +33,21 @@ pub fn applicative_follows_laws<T: Applicative + FunctorTestSuite>() -> R {
})
})
});
res += seq_is_homomorphic::<T, _, _, _, _>(|x| x + 3, || 2);
res += seq_is_homomorphic::<T, _, _>(|x| x + 3, || 2);
T::sample(|pf| {
res += seq_respects_interchange::<T, _, _, _, _, _>(|| pf(|x| x + 3), || 2);
res += seq_respects_interchange::<T, _, _, _>(|| pf(|x| x + 3), || 2);
});
T::sample(|pa| {
T::sample(|pf| {
res += seq_can_be_expressed_via_la2::<T, _, _, _, _, _>(|| pf(|x| x + 3), || pa(2));
res += seq_can_be_expressed_via_la2::<T, _, _, _>(|| pf(|x| x + 3), || pa(2));
})
});
T::sample(|pa| {
res += fmap_can_be_expressed_via_seq::<T, _, _, _, _>(|x| x + 3, || pa(2));
res += fmap_can_be_expressed_via_seq::<T, _, _>(|x| x + 3, || pa(2));
});
T::sample(|pa| {
T::sample(|pb| {
res += discard_can_be_expressed_via_seq_or_la2::<T, _, _, _, _>(|| pa(2), || pb(2));
res += discard_can_be_expressed_via_seq_or_la2::<T, _, _>(|| pa(2), || pb(2));
})
});
res
@ -57,29 +57,25 @@ pub fn monad_follows_laws<T: Monad + FunctorTestSuite>() -> R
where {
let mut res = applicative_follows_laws::<T>();
T::sample(|pa| {
res += bind_respects_left_identity::<T, _, _, _, _>(|x| pa(x + 3), || 2);
res += bind_respects_left_identity::<T, _, _>(|x| pa(x + 3), || 2);
});
T::sample(|pa| {
res += bind_respects_right_identity::<T, _, _>(|| pa(2));
res += bind_respects_right_identity::<T, _>(|| pa(2));
});
T::sample(|pa| {
T::sample(|pg| {
T::sample(|pf| {
res += bind_is_associative::<T, _, _, _, _, _, _>(
|x| pf(x + 5),
|x| pg(x + 3),
|| pa(2),
);
res += bind_is_associative::<T, _, _, _>(|x| pf(x + 5), |x| pg(x + 3), || pa(2));
})
})
});
T::sample(|pa| {
T::sample(|pf| {
seq_can_be_expressed_via_bind::<T, _, _, _, _, _>(|| pf(|x| x + 3), || pa(2));
seq_can_be_expressed_via_bind::<T, _, _, _>(|| pf(|x| x + 3), || pa(2));
})
});
T::sample(|pa| {
res += fmap_can_be_expressed_via_bind::<T, _, _, _, _>(|x| x + 3, || pa(2));
res += fmap_can_be_expressed_via_bind::<T, _, _>(|x| x + 3, || pa(2));
});
res
}

131
src/func/tests.rs
View File

@ -88,13 +88,8 @@ impl AddAssign<R> for R {
}
}
pub fn fmap_respects_identity<
'a,
T: 'a + Functor + Eqr,
A: 'a + Debug + PartialEq,
FA0: Fn() -> T::F<'a, A>,
>(
fa0: FA0,
pub fn fmap_respects_identity<'a, T: 'a + Functor + Eqr, A: 'a + Debug + PartialEq>(
fa0: impl Fn() -> T::F<'a, A>,
) -> R {
T::eqr("identity: fmap id == id", T::fmap(|a| a, fa0()), fa0())
}
@ -105,13 +100,10 @@ pub fn fmap_respects_composition<
A: 'a,
B: 'a,
C: 'a + Debug + PartialEq,
F: 'a + Copy + Fn(B) -> C,
G: 'a + Copy + Fn(A) -> B,
FA0: Fn() -> T::F<'a, A>,
>(
f: F,
g: G,
fa0: FA0,
f: impl 'a + Copy + Fn(B) -> C,
g: impl 'a + Copy + Fn(A) -> B,
fa0: impl Fn() -> T::F<'a, A>,
) -> R {
T::eqr(
"composition: fmap (f . g) == fmap f . fmap g",
@ -120,13 +112,8 @@ pub fn fmap_respects_composition<
)
}
pub fn seq_respects_identity<
'a,
T: 'a + Applicative + Eqr,
A: 'a + Debug + PartialEq,
FA0: Fn() -> T::F<'a, A>,
>(
fa0: FA0,
pub fn seq_respects_identity<'a, T: 'a + Applicative + Eqr, A: 'a + Debug + PartialEq>(
fa0: impl Fn() -> T::F<'a, A>,
) -> R {
T::eqr(
"identity: pure id <*> v = v",
@ -143,13 +130,10 @@ pub fn seq_respects_composition<
C: 'a + Debug + PartialEq,
F: 'a + Fn(B) -> C,
G: 'a + Fn(A) -> B,
FF0: Fn() -> T::F<'a, F>,
FG0: Fn() -> T::F<'a, G>,
FA0: Fn() -> T::F<'a, A>,
>(
ff0: FF0,
fg0: FG0,
fa0: FA0,
ff0: impl Fn() -> T::F<'a, F>,
fg0: impl Fn() -> T::F<'a, G>,
fa0: impl Fn() -> T::F<'a, A>,
) -> R {
T::eqr(
"composition: pure (.) <*> u <*> v <*> w = u <*> (v <*> w)",
@ -164,16 +148,9 @@ pub fn seq_respects_composition<
)
}
pub fn seq_is_homomorphic<
'a,
T: 'a + Applicative + Eqr,
A: 'a,
B: 'a + Debug + PartialEq,
A0: Fn() -> A,
F: 'a + Fn(A) -> B,
>(
f: F,
a0: A0,
pub fn seq_is_homomorphic<'a, T: 'a + Applicative + Eqr, A: 'a, B: 'a + Debug + PartialEq>(
f: impl 'a + Fn(A) -> B,
a0: impl Fn() -> A,
) -> R {
T::eqr(
"homomorphism: pure f <*> pure x = pure (f x)",
@ -188,11 +165,9 @@ pub fn seq_respects_interchange<
A: 'a,
B: 'a + Debug + PartialEq,
F: 'a + Fn(A) -> B,
A0: 'a + Fn() -> A,
FF0: Fn() -> T::F<'a, F>,
>(
ff0: FF0,
a0: A0,
ff0: impl Fn() -> T::F<'a, F>,
a0: impl 'a + Fn() -> A,
) -> R {
T::eqr(
"interchange: u <*> pure y = pure ($ y) <*> u",
@ -207,11 +182,9 @@ pub fn seq_can_be_expressed_via_la2<
A: 'a,
B: 'a + Debug + PartialEq,
F: 'a + Fn(A) -> B,
FA0: Fn() -> T::F<'a, A>,
FF0: Fn() -> T::F<'a, F>,
>(
ff0: FF0,
fa0: FA0,
ff0: impl Fn() -> T::F<'a, F>,
fa0: impl Fn() -> T::F<'a, A>,
) -> R {
T::eqr(
"seq via la2: (<*>) = liftA2 id",
@ -225,11 +198,9 @@ pub fn fmap_can_be_expressed_via_seq<
T: 'a + Applicative + Eqr,
A: 'a,
B: 'a + Debug + PartialEq,
F: 'a + Copy + Fn(A) -> B,
FA0: Fn() -> T::F<'a, A>,
>(
f: F,
fa0: FA0,
f: impl 'a + Copy + Fn(A) -> B,
fa0: impl Fn() -> T::F<'a, A>,
) -> R {
T::eqr(
"fmap via seq: fmap f x = pure f <*> x",
@ -243,11 +214,9 @@ pub fn discard_can_be_expressed_via_seq_or_la2<
T: 'a + Applicative + Eqr,
A: 'a,
B: 'a + Debug + PartialEq,
FA0: 'a + Fn() -> T::F<'a, A>,
FB0: 'a + Fn() -> T::F<'a, B>,
>(
fa0: FA0,
fb0: FB0,
fa0: impl 'a + Fn() -> T::F<'a, A>,
fb0: impl 'a + Fn() -> T::F<'a, B>,
) -> R {
T::eqr(
"discard via seq: u *> v = (id <$ u) <*> v",
@ -260,16 +229,9 @@ pub fn discard_can_be_expressed_via_seq_or_la2<
)
}
pub fn bind_respects_left_identity<
'a,
T: 'a + Monad + Eqr,
A: 'a,
B: 'a + Debug + PartialEq,
F: 'a + Fn(A) -> T::F<'a, B>,
A0: Fn() -> A,
>(
f: F,
a0: A0,
pub fn bind_respects_left_identity<'a, T: 'a + Monad + Eqr, A: 'a, B: 'a + Debug + PartialEq>(
f: impl 'a + Fn(A) -> T::F<'a, B>,
a0: impl Fn() -> A,
) -> R {
T::eqr(
"left identity: pure a >>= k = k a",
@ -278,13 +240,8 @@ pub fn bind_respects_left_identity<
)
}
pub fn bind_respects_right_identity<
'a,
T: 'a + Monad + Eqr,
A: 'a + Debug + PartialEq,
FA0: Fn() -> T::F<'a, A>,
>(
fa0: FA0,
pub fn bind_respects_right_identity<'a, T: 'a + Monad + Eqr, A: 'a + Debug + PartialEq>(
fa0: impl Fn() -> T::F<'a, A>,
) -> R {
T::eqr(
"right identity: m >>= bind = m",
@ -293,19 +250,10 @@ pub fn bind_respects_right_identity<
)
}
pub fn bind_is_associative<
'a,
T: 'a + Monad + Eqr,
A: 'a,
B: 'a,
C: 'a + Debug + PartialEq,
F: 'a + Clone + Fn(B) -> T::F<'a, C>,
G: 'a + Clone + Fn(A) -> T::F<'a, B>,
FA0: 'a + Fn() -> T::F<'a, A>,
>(
f: F,
g: G,
fa0: FA0,
pub fn bind_is_associative<'a, T: 'a + Monad + Eqr, A: 'a, B: 'a, C: 'a + Debug + PartialEq>(
f: impl 'a + Clone + Fn(B) -> T::F<'a, C>,
g: impl 'a + Clone + Fn(A) -> T::F<'a, B>,
fa0: impl 'a + Fn() -> T::F<'a, A>,
) -> R {
T::eqr(
r"associativity: m >>= (\x -> k x >>= h) = (m >>= k) >>= h",
@ -320,11 +268,9 @@ pub fn seq_can_be_expressed_via_bind<
A: 'a,
B: 'a + Debug + PartialEq,
F: 'a + Fn(A) -> B,
FA0: 'a + Fn() -> T::F<'a, A>,
FF0: Fn() -> T::F<'a, F>,
>(
ff0: FF0,
fa0: FA0,
ff0: impl Fn() -> T::F<'a, F>,
fa0: impl 'a + Fn() -> T::F<'a, A>,
) -> R {
T::eqr(
r"seq via bind: m1 <*> m2 = m1 >>= (\x1 -> m2 >>= (\x2 -> pure (x1 x2)))",
@ -333,16 +279,9 @@ pub fn seq_can_be_expressed_via_bind<
)
}
pub fn fmap_can_be_expressed_via_bind<
'a,
T: 'a + Monad + Eqr,
A: 'a,
B: 'a + Debug + PartialEq,
F: 'a + Copy + Fn(A) -> B,
FA0: 'a + Fn() -> T::F<'a, A>,
>(
f: F,
fa0: FA0,
pub fn fmap_can_be_expressed_via_bind<'a, T: 'a + Monad + Eqr, A: 'a, B: 'a + Debug + PartialEq>(
f: impl 'a + Copy + Fn(A) -> B,
fa0: impl 'a + Fn() -> T::F<'a, A>,
) -> R {
T::eqr(
"fmap via bind: fmap f xs = xs >>= return . f",