(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
| 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 |
| 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 |
| 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 |
| 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; _,_; _×_; -,_) |
| 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 |
| 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 #-} |
| 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) |
| #| 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 |
| 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 |