{-# OPTIONS --cubical-compatible #-}
module Padova2025.ProgrammingBasics.DependentFunctions where

Dependent functions#

For most functions in blackboard mathematics and ordinary programming, the result type is independent of the input value. For instance, no matter the value of n, half n is always of type ℕ. Similarly, to matter the value of x, not x is always of type Bool.

But there are also functions where the result type does depend on the input value. A basic example is the so-called polymorphic identity function. Unlike idBool : Bool → Bool or idℕ : Nat → Nat, the polymorphic identity function works at all types.

More precisely, the polymorphic identity function takes as input…

1. a value X : Set and
2. a value a : X,

and then returns the same value a. So the result type depends on the value of the input X. In Agda we write this up as follows.

id : (X : Set) → X → X
id X a = a

We could then use this function as follows.

open import Padova2025.ProgrammingBasics.Naturals.Base

example-usage : ℕ
example-usage = id ℕ four

We will shortly define the type Vector A n of length-n lists of elements of A. We could then imagine the following example for a dependent function:

replicate : (A : Set) → (n : ℕ) → A → Vector A n
-- Read a type `A`, a number `n`, an element `x : A` as input
-- and output a length-`n` list of copies of `x`.

five-dimensional-zero-vector      = replicate ℕ 5 zero
three-dimensional-all-ones-vector = replicate ℕ 3 one

twice : ℕ → ℕ
twice zero     = zero
twice (succ x) = succ (succ (twice x))

twice : (x : ℕ) → ℕ
twice zero     = zero
twice (succ x) = succ (succ (twice x))

Example: Polymorphic constant function#

Implement a function K which reads as input…

1. a type X (i.e. a value X : Set),
2. a type Y,
3. a value x : X and
4. a value y : Y,

… and returns x.

K : {!!}
K = {!!}

K : (X : Set) → (Y : Set) → X → Y → X
K X Y x y = x