Kazark

(setq org-confirm-babel-evaluate nil)
(setq org-babel-scala-command "/usr/local/Cellar/dotty/3.0.0-RC1/bin/scala")
(setq org-babel-scala-wrapper-method "%s")
(unless (boundp 'org-babel-scala-evaluate)
  (load-file "~/.emacs.d/ob-scala.el"))

object Nothing extends RuntimeException

Kazark

module NTypes where

open import Data.Empty using (⊥)
open import Agda.Builtin.Unit using (⊤)
open import Data.Nat using (ℕ; zero; suc)
open import Function using (id; _∘_)

infixr 5 _∧_ _v_ _-ary_to_ _,_

record _∧_ (a : Set) (b : Set) : Set where

Kazark

module Length where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; trans)
open import Data.List using (List; _∷_; []; length)
open import Data.Nat using (ℕ; _≤_; s≤s; z≤n)
open import Data.Product using (∃-syntax; _,_; _×_; -,_)
open import Relation.Nullary using (¬_)

_ℕList≤_ : List ℕ → List ℕ → Set

Kazark

module Alg where

open import Data.Nat using (ℕ; zero; suc)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_)
open import Data.List using (List; _∷_; [])
open import Data.Product using (∃-syntax; -,_)

NOp : ℕ → Set → Set
NOp zero a = a

Kazark

module Point where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; trans)
open import Relation.Nullary using (¬_)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Function using (_∘_)
open import Data.Nat.Properties using (+-comm; +-identityʳ)
open import Data.Product using (∃-syntax; _,_; _×_; -,_)

Kazark

module Two where

open import Level using (Level)
open import Function using (_∘_; id; _$_)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎; step-≡; step-≡˘)

data Two (A : Set) : Set where
  TwoOf : A → A → Two A

Kazark

We are going to be redefining a bunch of things that are in prelude in order to
make them explicit and all in one place:

> {-# LANGUAGE NoImplicitPrelude #-}

It is best for learning to be able to write concretized signatures of typeclass
functions when defining instances:

> {-# LANGUAGE InstanceSigs #-}

Kazark

package example

import cats._
import cats.implicits._

sealed trait List[+A]
case object Nil extends List[Nothing]
final case class Cons[A](head: A, tail: List[A]) extends List[A]

final case class Co[I, A](run : I => A)

Kazark

#| An obfuscated Haskell-style solution to exercise 1.7 from SICP in Guile.
 |
 | The basis of this solution is the idea: the numerical method for square root
 | does not inherently have any notion of what is means for the solution to be
 | "good enough"; that is an _orthogonal_ concern. The inherent idea, in its
 | purest form, is a limit of the algorithm considered as a function of the
 | number of iterations. Therefore, it would be pleasing in our implementation
 | to divorce the idea of what "good enough" means from our expression of the
 | algorithm. But this requires an infinite data structure, because if we do not
 | have an infinite data structure, we must from the first think about when to

Kazark

This is a tutorial on the Curry-Howard correspondence, or the correspondence
between logic and type theory, written by Keith Pinson, who is still a learner
on this subject. If you find an error, please let me know.

This is a Bird-style literate Haskell file. Everything is a comment by default.
Lines of actual code start with `>`. I recommend that you view it in an editor
that understands such things (e.g. Emacs with `haskell-mode`). References will
also be made to Scala, for programmers less familiar with Haskell.

We will need to turn on some language extensions. This is not an essay on good