116 lines
3.9 KiB
Org Mode
116 lines
3.9 KiB
Org Mode
:PROPERTIES:
|
||
:ID: f6c9e1a7-8465-4cef-9481-2b803d0c43d4
|
||
:END:
|
||
#+title: afp_lab_1
|
||
#+filetags: :notes:uni:
|
||
<2025-01-20 Mon>
|
||
* Installation of Agda:
|
||
** Step 1
|
||
#+BEGIN_SRC eshell
|
||
sudo apt-get install zlib1g-dev libncurses5-dev
|
||
#+END_SRC
|
||
|
||
then install ghc
|
||
- https://www.haskell.org/ghcup/
|
||
|
||
Now that you have cabal installed, use it to install Agda as a Haskell package:
|
||
#+BEGIN_SRC eshell
|
||
cabal update
|
||
cabal install Agda
|
||
#+END_SRC
|
||
** 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:
|
||
[[file:~/master-folder/Uni/ADVFUNC/afp-learning-2024-2025/files/LectureNotes/files/exercises/my-lab1.lagda.md][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.
|