↓Skip to main content
  1. Notes/

Dependent Types

  • type parameters can be arbitrary values, not only types
  • types with arguments
type List(len: Nat, a: Type) = 
	| Nil : List(0, a)
	| Cons(a, List(len, a)) : List(len+1, a))

Nat corresponds to a number, it is not represented in binary but by zero element Z and successor function S

type Nat = 
	| Z : Nat
	| S(n: Nat) : Nat

type List(len: Nat, a: Type) = 
	| Nil : List(Z, a)
	| Cons(a, List(len, a)) : List(S(len), a))