{-# OPTIONS --cubical-compatible #-}
module Padova2025-zh-TW.ProgrammingBasics.Booleans where

布林值#

下面這三行程式碼引進一個新的資料型別 Bool。這個型別恰好包含兩個值：false 與 true：

data Bool : Set where
  false : Bool
  true  : Bool

在 Agda 中，每個 term 都有某個型別。term 的型別以冒號標示。因此 term false 與 true 的型別是 Bool，而 Bool 本身的型別是 Set。我們把型別想像成裝著值的容器，類似黑板數學中的集合。 型別 Set 是 Agda 內建的，不需要（也無法）手動定義。它包含所有所謂的小型（small）資料型別。

-- true : Bool : Set : Set₁ : Set₂ : …

範例：常數#

有了布林值的型別，我們就能引進簡單的常數：

our-first-constant : Bool
our-first-constant = true

不太刺激——沒有函數的話，我們只能選擇 false 與 true 這兩個平凡的右手邊。

範例：恆等函數#

讓我們來實作第一個函數：恆等函數，它把每個輸入值映射到自己，也就是把 false 映射到 false、把 true 映射到 true。和 Haskell 一樣，也和大多數其他程式語言不同，定義函數不需要任何特殊的關鍵字。

以下是所需程式碼的樣板：

idBool : Bool → Bool   -- 輸入 `→` 請打 `\->`、`\to` 或 `\rightarrow`
idBool x = {!!}

idBool : Bool → Bool   -- 輸入 `→` 請打 `\->`、`\to` 或 `\rightarrow`
idBool x = x

在定義的右手邊，我們第一次遇到「hole」，也就是顯示為 {!!} 的佔位符。在 Agda 中，我們經常以互動的方式建構程式 或證明；hole 就是主要的互動點。在程式碼中插入問號 ?，再用 C-c C-l（也就是 Ctrl-c Ctrl-l）重新載入檔案， 就能產生一個 hole。

請依照下面的提示完成第一個習題，實作恆等函數。

範例：否定#

第二個範例，來實作否定函數。它應該把 false 映射到 true，反之亦然：

not : Bool → Bool
not = {!!}

not : Bool → Bool
not false = true
not true  = false

和大多數其他程式語言不同，Agda 沒有內建的 if 關鍵字；取而代之，我們用 pattern matching 來按情況定義函數。 更棒的是，我們不必自己列出所有可能的情況；可以借助 Agda 的輔助功能替我們完成，做法請見提示。

執行函數#

在黑板數學以及大多數程式語言中，以引數呼叫函數的通用語法是 f(x)，例如 sin(π)。Agda 遵循 lambda 演算與 Haskell 的傳統，改用（以空白分隔的）並置寫法 f x：

example-run : Bool
example-run = {!!}

example-run : Bool
example-run = not our-first-constant

在這個 hole 裡填入 not our-first-constant，或是你自己選擇的更複雜的函數呼叫。接著按 C-c C-v， 輸入你想求值的運算式（此處是 example-run），就能觀察結果。