Lecture Notes: Types and Functions in Idris 2

1. Primitive Types, Program Structure, and Constants

Idris provides built-in primitive types for basic operations and text manipulation, alongside a strict program structure.

Primitives: Int, Integer, Double, Char, String, Ptr (foreign pointers), and Bool (True and False).

Rules:

• Type declarations are mandatory: Every top-level definition must explicitly state its type.

• Indentation & Order: Order matters (definitions must precede use), and indentation dictates block structure.

• The Prelude: Automatically imported, providing basic I/O, arithmetic, and standard data types.

Code Example: Primitive Constants & Basic Program Structure

module Prims

x : Int
x = 94

foo : String
foo = "Sausage machine"

bar : Char
bar = 'Z'

quux : Bool
quux = False

Idris requires an explicit type signature (x : Int) for top-level declarations.

2. Algebraic Data Types

Data types use syntax similar to Haskell and must start with a capital letter.

• Recursive Structures (Nat): Unary natural numbers built out of zero (Z) and the successor of another number (S).
• Polymorphic Containers (List): Defined as either empty (Nil) or a head element prepended to a tail ((::)).
• Fixity Declarations: Infix operators can be custom-defined and assigned precedence and associativity.

Code Example: Defining Nat and List

-- Unary Natural numbers (from the standard library)
data Nat = Z | S Nat

-- Polymorphic Lists
data List a = Nil | (::) a (List a)

-- Registering a custom fixity for the list cons operator
infixr 10 ::

Idris uses unary natural numbers (Nat) alongside machine integers: their inductive structure makes them exceptionally clean for writing proofs and relating to dependent types later, while the compiler optimizes them for performance under the hood. infixr means use infix, right associative, with 10 precedence value (0-100).

3. Functions, Pattern Matching, and Scope

Functions are implemented via pattern matching, using a single colon (:) for type signatures.

• Namespaces: Function names, data constructors, and type constructors share a single namespace.
• where Clauses: Allow local helper functions and constants to share scope with the parent function.
• Totality Checking: By default, functions must be covering (handling all possible input patterns), preventing runtime match errors.
• Holes (?): Incomplete code segments prefixed with ? allow developers to query the type checker for expected types and available local variables.

Code Example: Pattern Matching, where, and Holes

-- Top-level function with pattern matching
plus : Nat -> Nat -> Nat
plus Z y = y
plus (S k) y = S (plus k y)

-- Using a where clause for helper functions
reverse : List a -> List a
reverse xs = revAcc [] xs 
  where
    revAcc : List a -> List a -> List a
    revAcc acc [] = acc
    revAcc acc (x :: xs) = revAcc (x :: acc) xs

-- Using a hole for incremental development
main : IO ()
main = putStrLn ?greeting

:t greeting at the REPL when ?greeting is present gives students immediate feedback on what type is expected, turning the type checker into an interactive assistant.

4. Advanced Feature 1: First-Class Dependent Types

In Idris, types are first-class citizens—they can be computed, manipulated, and passed to functions just like regular values.

• Dependent Types: Types can depend on runtime values.
• Example (isSingleton): A function that computes a Type based on a Bool flag.

Code Example: Computing Types Dynamically

-- Computes a type based on a boolean flag
isSingleton : Bool -> Type
isSingleton True  = Nat
isSingleton False = List Nat

-- Return type changes depending on the value of the input argument!
mkSingle : (x : Bool) -> isSingleton x
mkSingle True  = 0
mkSingle False = []

In mainstream languages (like Java or Python) types are static metadata erased before runtime. Here, a value (True or False) dictates what type is returned.

5. Advanced Feature 2: Vectors (Vect)

Vectors are lists indexed by their exact length (Nat), encoded at the type level.

• Type Signature: data Vect : Nat -> Type -> Type
• Compile-Time Guarantees: Functions like vector concatenation (++) prove statically that the resulting vector length is the sum of the inputs (n + m). If you accidentally write k + k instead of k + m, the type checker catches it.

Code Example: Type-Safe Vector Concatenation

data Vect : Nat -> Type -> Type where
  Nil  : Vect Z a
  (::) : a -> Vect k a -> Vect (S k) a

-- The type guarantees length safety statically
(++) : Vect n a -> Vect m a -> Vect (n + m) a
(++) Nil ys = ys
(++) (x :: xs) ys = x :: xs ++ ys

Error message if we break this invariant. The type checker will output a unification error showing a mismatch between plus k k and plus k m, proving that length errors are caught at compile time, not production.

6. Advanced Feature 3: Finite Sets (Fin)

Finite sets capture bounded natural numbers from 0 to n - 1, making them ideal for safe indexing.

• Definition: data Fin : Nat -> Type

• FZ represents zero (for sets of size S k).

• FS k represents the successor index.

• Safe Indexing (index): Because Fin n statically bounds the index, looking up an element in a vector requires no runtime bounds checks and makes impossible cases (like indexing an empty Nil vector) unrepresentable.

Code Example: Bounded Indexing Without Runtime Checks

data Fin : Nat -> Type where
  FZ : Fin (S k)
  FS : Fin k -> Fin (S k)

-- Safe vector lookup
index : Fin n -> Vect n a -> a
index FZ     (x :: xs) = x
index (FS k) (x :: xs) = index k xs
-- Notice: No case for Nil is needed because Fin Z is uninhabited!

The compiler knows Nil is impossible because a Fin n cannot be constructed for n = Z. This eliminates entire classes of bugs (like IndexOutOfBoundsException) statically.