# -*- org -*-
# | ~C-x C-a~ | transform org ~org-agda~ blocks to literate Agda blocs        |
# | ~C-x C-a~ | transform literate Agda code delimiters to org ~org-agda~ src |
#
#
# C-c C-= to see constraints.

#+TITLE: A Gentle Introduction to Agda
#+DESCRIPTION: A quick taste of dependently-typed programming: Agda ≈ Haskell on steroids (proofs).
#+AUTHOR: Musa Al-hassy
#+EMAIL: alhassy@gmail.com

*Warning*
➪ When using [[https://github.com/alhassy/org-agda-mode][org-agda]], must have blank newlines _before_ the ~\end{code}~ and ~#+end_src~ markers.
➪ C-c C-v C-t, org-babel-tangle, works as expected however Agda does not allow two files of the
  shape ~X.lagda~ and ~X.agda~, and so tangled code should ideally be relocated or not even bothered
  with in-favour of using org-mode with org-agda.
➪ org-agda does not respect Org-mode's COMMENT mechanism. but acknowledges EXAMPLEs in-place of SRCs.
➪ org-agda-mode is a bit slow ---it was written with little to no Lisp knowledge.
  It needs to be updated.

* Imports

First, some necessary imports:
\begin{code}
module today where
open import today-generated

import Level as Level
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Unary using (Decidable)
open import Relation.Nullary

open import Data.Unit
open import Data.Nat as Nat hiding (_⊓_)
open import Data.Bool
open import Data.Product
open import Data.List as List
open import Data.Char as Char
open import Data.String as String
open import Function

{- Org-agda has a bug: If you remove the next empty new line, it crashes. -}
{- One requires an empty line before the closing marker. -}

\end{code}
bye


* Records ≅ Products

0. Generics ⇒ “∀” if no type provided
   + Type variables

1. Inference ⇒ curly braces

2. “Set” is read TYPE!

3. C-c C-r ⇒ help me get started; “refine”
4. C-c C-, ⇒ get goal

5. C-c C-a ⇒ automatically write the program

\begin{code}
first₀ : (A B : Set) → A × B → A
first₀ = λ A B p → proj₁ p

{- C-c c-a -}
first₁ : (A B : Set) → A × B → A
first₁ = λ A B → proj₁

{- C-c C-c ⇒ case analysis -}
first₂ : (A B : Set) → A × B → A
first₂ A B (a , b) = a

sad-usage : ℕ
sad-usage = first₀ ℕ Bool (3 , true)

first : {A B : Set} → A × B → A
first = proj₁
\end{code}

* Binary Trees

\begin{code}
{- “Tree” is a VALUE of the type Set. -}
data Tree (A : Set) : Set where
  Leaf : A → Tree A
  _∇_  : (left right : Tree A) → Tree A
  -- \nabla

ex₀ : Tree ℕ
ex₀ = Leaf zero

{-
Statements ≈ Expressions
Types      ≈ Value
-}

Shawn : Set₁
Shawn = Set  -- ≈ Set₀

Dan : Set₂
Dan = Set₁

𝔹 : Set
𝔹 = Bool

infix 5 _∇_
infix 6 _′

_′ : {A : Set} →  A → Tree A
a ′ = Leaf a

ex₁ : Tree 𝔹
ex₁ = ((true ′ ∇ false ′) ∇ (false ′ ∇ false ′)) ∇ true ′
\end{code}

+ M-. ⇒ jump to defn

* FYI! “Lists are Trees where ∇ is associative”!
\begin{code}
{- When we go to lists, this is “reverse” -}
mirror : {A : Set} → Tree A → Tree A
mirror (Leaf x) = Leaf x
mirror (l ∇ r)  = mirror r ∇ mirror l

ex₂ : Tree ℕ
ex₂ = ((0 ′ ∇ 1 ′) ∇ (2 ′ ∇ 3 ′)) ∇ 4 ′

{- my unit test -}
_ : mirror ex₂ ≡ Leaf 4 ∇ ((Leaf 3 ∇ Leaf 2) ∇ (Leaf 1 ∇ Leaf zero))
_ = refl
\end{code}

* COMMENT footer

The org-agda and literate.el come from:
https://github.com/alhassy/org-agda-mode

Need to ensure org-indent-mode is off when going to agda.

# Local Variables:
# eval: (setq org-src-preserve-indentation 't)
# eval: (load-file "~/org-agda-mode/literate.el")
# End: