org_roam/20250120113936-afp_lab_1.org

afp_lab_1

• Installation of Agda:
  • Step 1
  • Step 2
• Exercises:

<2025-01-20 Mon>

Installation of Agda:

Step 1

sudo apt-get install zlib1g-dev libncurses5-dev

then install ghc

• https://www.haskell.org/ghcup/

Now that you have cabal installed, use it to install Agda as a Haskell package:

cabal update
cabal install Agda

Step 2

Most users will want to install the standard library. You can install this as any other Agda library (see Library Management). See the agda-stdlib project’s installation instructions for the steps to take to install the latest version. https://github.com/agda/agda-stdlib https://agda.readthedocs.io/en/latest/tools/package-system.html#package-system

Exercises:

my lab1

```agda data Bool : Type where true false : Bool ```

In Agda, the snippet `data Bool : Type where true false : Bool` is a definition of a simple data type named `Bool`. Let’s break down and explain all the components and words in this snippet:

—

### 1. `data`

• What it means: This keyword introduces a new data type definition in Agda.
• Purpose: Defines a type that consists of one or more constructors, which are used to create values of the type.
• In this case: The `data` keyword is used to define the `Bool` type.

—

### 2. `Bool`

• What it is: The name of the data type being defined.
• Purpose: Represents a type that has exactly two possible values: `true` and `false`.
• In this case: `Bool` is a common type used to represent truth values in logic (true or false).

—

### 3. `:` (colon)

• What it means: Indicates a type declaration in Agda.
• Purpose: Separates the name of the data type (`Bool`) from its type (`Type`).
• In this case: `Bool : Type` declares that `Bool` is a type itself (i.e., a type of values).

—

### 4. `Type`

• What it is: The universe of all types in Agda.

• Purpose: In Agda, types are first-class citizens, and `Type` represents the "type of types." For instance:

  • `Bool : Type` means `Bool` is a type.
  • If you define a type `ℕ : Type` for natural numbers, it also belongs to `Type`.
• In this case: `Bool` is defined as a type that belongs to this universe.

—

### 5. `where`

• What it means: Introduces the constructors (values) of the type.
• Purpose: Lists the specific ways you can construct or create values of the newly defined type.
• In this case: `where` introduces the two constructors, `true` and `false`, which are the only possible values of the `Bool` type.

—

### 6. `true false`

• What they are: The constructors of the `Bool` type.

• Purpose: Constructors are functions (or constants) that produce values of the type. Here:

  • `true : Bool` means `true` is a value of type `Bool`.
  • `false : Bool` means `false` is a value of type `Bool`.
• In this case: These two constructors define all possible values of `Bool`.

—

### 7. `Bool` after the `:`

• What it means: Specifies the type of each constructor.
• Purpose: Ensures that each constructor produces a value of the correct type (`Bool` in this case).
• In this case: Both `true` and `false` are of type `Bool`.

—

### Complete Meaning The entire definition can be read as:

1. Define a new type called `Bool`.
2. `Bool` belongs to the universe of types (`Type`).

3. The `Bool` type has two constructors:

   • `true` (a value of type `Bool`).
   • `false` (a value of type `Bool`).

—

### Example Usage in Agda You can use `Bool` in various ways: ```agda – A function that negates a Bool not : Bool → Bool not true = false not false = true

– A value of type Bool myBool : Bool myBool = true ```

This showcases how the `Bool` type and its constructors (`true` and `false`) can be used in programs.