| namespace System | |
| { | |
| /// <summary>Mathematical functions for binomials</summary> | |
| public static class Binomials | |
| { | |
| // / \ | |
| // | n | from n | |
| // | | | |
| // | k | choose k | |
| // \ / |
| module Lambda where | |
| -- https://www.youtube.com/watch?v=O0TgP7GKkSY | |
| -- https://gist.github.com/pedrominicz/127ab01cec689cc3d69f32e6c4f758bb | |
| data Term | |
| = App Term Term | |
| | Lam Term | |
| | Var Int | |
| deriving (Eq, Show) |
In Part 1 we have developed a basic set of rules for
a simple quantitative dependently typed theory. The rules were, however, non-directional (or nondeterministic). By this,
I mean that there could be multiple instances of rules that would lead to the same conclusion. For example, consider the
sequent 0 A : *, 0 B : *, ω f : A → B, ω a : A ⊢ ω (f a) : B. We could derive this sequent at least in two ways:
This note summarizes what Juvix can learn from the implementation of Idris 2. References:
Quantitative type theory (QTT) is an extension of dependent type theory which allows us to track the number of computational (non-erased) uses of variables in well-typed lambda terms. With such usage information, QTT allows us to combine dependent types with substructural types, such as linear, affine or relevant types.
While in a Martin-Löf style type theory typing judgments are of form
x1 : A1, ..., xn : An ⊢ b : B, in QTT the bindings in the context
| // Equality with values | |
| // ==================== | |
| // A Boolean is a set with two values | |
| T Bool | |
| | true; | |
| | false; | |
| // Boolean not is a function that receives a bool and returns a bool | |
| bool_not(a: Bool): Bool |
| // I've decided to check the "Cubical Type Theory: a constructive interpretation | |
| // of the univalence axiom" paper (better later than never!) and managed to port | |
| // many of its concepts to Formality using self-types only, allowing us to | |
| // derive function extensionality on it (a 500 lines-of-code language!). | |
| // The main insight is that we can encode the Interval type and the Path type as | |
| // self-encodings that refer to each other. The Interval type is like a boolean, | |
| // but with an extra constructor of type `i0 == i1` forcing that, in order to | |
| // eliminate an interval, both cases must be equal. The Path type proposes that | |
| // two values `a, b : A` are equal if there exists a function `t : I -> A` such |
Datatypes in the Formality programming language are built out of an unusual
structure: the self-type. Roughly speaking, a self-type is a type that can
depend or be a proposition on it's own value. For instance, the consider the
2 constructor datatype Bool:
The originality of these Gists varies drastically. Most are inspired by the work of others, in that case, all merit goes to the original authors. I have linked everything used as reference material on the Gists themselves.
