lambda_types/
primitives.rs

1crate::define! {
2    /// Identity function. Returns its input.
3    /// ```text
4    /// λx.x
5    /// ```
6    pub fn Identity ::= { Input. Input };
7    /// Takes two values and returns the first.
8    /// ```text
9    /// λa.λb.a
10    /// ```
11    pub fn FirstOf ::= { Input. (Constant<Input>) };
12    /// Returns its type parameter, ignoring input.
13    /// ```text
14    /// λv.I
15    /// ```
16    pub fn Constant<I> ::= { _Ignored. I };
17    /// Takes two values and returns the second.
18    /// ```text
19    /// λa.λb.b
20    /// ```
21    pub fn SecondOf ::= { _Ignored. Identity };
22    
23    /// Composes a function with another.
24    /// Note that this returns a [`Composed`], for more ergonomic point-free form.
25    /// ```text
26    /// λf.λg.(λx.f(gx))
27    /// ```
28    pub fn Compose ::= { A. B. (Composed<A, B>) };
29    
30    /// The composition of two functions. See [`Compose`].
31    /// ```text
32    /// λx.FGx
33    /// ```
34    pub fn Composed<F, G>
35        ::= { Input. { F, { G, Input }}}
36    where
37        G: Input,
38        F: {G, Input};
39    
40    /// Takes a function and an input, and returns the function applied to said input.
41    /// ```text
42    /// λf.λx.fx
43    /// ```
44    pub fn Apply
45        ::= { Fn. Input. { Fn, Input }}
46    where
47        Fn: Input;
48
49    /// S combinator. Takes three inputs, and applies the first to the second and third.
50    /// ```text
51    /// λx.λy.λz.xz(yz)
52    /// ```
53    pub fn Sheinfinkel ::= { X. Y. Z. {X, Z, { Y, Z }}} where
54        X: Z, Y: Z, {X, Z}: {Y, Z};
55
56    /// Takes a function that takes two arguments and the first argument to said function,
57    /// and returns a function that takes the second argument and runs the function with both.
58    /// See [`Curried`].
59    /// ```text
60    /// λf.λx.(λy.fxy)
61    /// ```
62    pub fn Curry
63        ::= { Fn. Input. (Curried<Fn, Input>) };
64    
65    /// Function that curries the first type argument with the second and the input. See [`Curry`].
66    /// ```text
67    /// λy.FXy
68    /// ```
69    pub fn Curried<Fn, X> ::= { Y. { Fn, X, Y }} where
70        Fn: X,
71        {Fn, X}: Y;
72}
lambda_types/primitives.rs

lambda_types/
primitives.rs
