What are dependent types?: for programmers
Types can describe facts about values. Start with a list-length example, then watch Osprey check an actual identity proof.
For programmers. 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
- Dependent types let a type describe facts about a value, such as how many items a list contains. They connect programming with precise mathematical claims. Osprey is a functional language with proof tools written in Osprey itself. Here is what its checker already does.
- Think of a list whose type includes its length. A function that needs exactly three items can reject a list of four before it runs. That is the idea behind dependent types. This length example explains the idea; it is not an Osprey API.
- Take a claim called p. A proof of p is evidence that p is true. A function can accept that evidence and return it unchanged. The statement is: for every claim p, evidence for p produces evidence for p.
- This is the actual Osprey source for that identity proof. It says: given a proposition p and evidence h for p, return h. Osprey's kernel reads the claim and the proof term, then checks that the evidence matches the claim.
- Run the kernel and both cases appear. Identity is accepted because the proof has the required type. A deliberately wrong term is refused, with the reason printed. You are watching real output, not a scripted green tick.
- Today Osprey checks this identity and a proof that chains two implications. That does not automatically prove your application correct. You still state the claim and build the evidence. Osprey is actively evolving, and this small checked fragment is where to start.