What are dependent types?: for mathematicians
Types can describe facts about values. Start with a list-length example, then watch Osprey check an actual identity proof.
For mathematicians. Choose the other audience version or browse the complete series.
Lean is the development oracle for compatible proofs; Osprey checks them independently. Known unsound reference behaviour must be refused, and changing a discipline requires fresh proof validation.
What this demonstrates
The length-indexed list is a conceptual introduction, not a shipped Osprey API. Ordinary Osprey programs retain Hindley-Milner type inference; dependent proof terms belong to a separate checking discipline.
Read the guide and try it yourself. Osprey is actively evolving; the guide distinguishes the recorded demonstration from current corpus progress.
Actual source
Continue learning
Use the Workbench · Current Mathlib port evidence · All twelve films
Transcript
- A dependent type can refer to a value. A later argument or result can then have a type determined by an earlier argument. This is a foundation of modern proof assistants. Osprey is a functional programming language whose current proof kernel checks a small collection of such terms.
- Consider a list type carrying its length. A list of three entries and a list of four entries then have different types. An operation can require exactly the length it needs. This notation is conceptual, not a shipped Osprey type.
- Read p as a proposition and h as a proof of p. The judgement h : p says h has type p. So a claim is a type, and evidence for it is a term of that type. The statement is checked, not just annotated.
- The source states: for every proposition p, a proof of p yields a proof of p. The term takes p and h, then returns h. Its type is a dependent function type, because the result type mentions the first argument p.
- The kernel accepts identity because the proof term has the stated dependent function type. It rejects the deliberate variant that promises q while returning evidence for p. The reasons come from the real run. That pair is the demonstration.
- Identity is the starting example, not the limit of the implementation. Osprey also checks imported logic proofs and natural-number addition commutativity, using inductive definitions and dependent elimination. The library port is already underway. These checked proofs and their dependencies are here in the repository.