module Padova2025.ProgrammingBasics.HigherOrder where

Higher-order functions

open import Padova2025.ProgrammingBasics.Booleans
open import Padova2025.ProgrammingBasics.Operators

Exercise: Unary tautologies

Implement a function is-tautology₁? which checks whether a given input function is constantly true.

For instance, for the function f defined by f x = x, the result of is-tautology₁ f should be false.

is-tautology₁ : (Bool → Bool) → Bool
is-tautology₁ f = {!!}

Exercise: Binary tautologies

Implement a function is-tautology₂? which checks whether a given input function of two arguments is constantly true.

For instance, for the function f defined by f x y = true, the result of is-tautology₂ f should be true.

is-tautology₂ : (Bool → Bool → Bool) → Bool
is-tautology₂ f = {!!}

Exercise: Types are first-class values

Most statically typed programming languages have a strict separation between values (which then exist only at runtime) and types (which then exist only at compiletime, and which are erased in the resulting machine code). In Agda, types are values in their own right—indeed, they are values of the type Set—and we can freely manipulate them.

For instance, define a function Endo which inputs a type X and outputs the type X → X of functions from X to X:

Endo : Set → Set
Endo X = {!!}