Skip to content

Instantly share code, notes, and snippets.

View Kazark's full-sized avatar

Keith Pinson Kazark

  • Undisclosed
View GitHub Profile
@Kazark
Kazark / MaybeMonad.org
Created March 19, 2021 14:45
Monad as a value versus as part of the language semantics (in Scala)
(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
Kazark / NTypes.agda
Last active November 30, 2020 21:37
What if Pair and Either were primitive, and other arities of product and coproduct types were generated from them?
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
Kazark / Length.agda
Created September 18, 2020 19:00
Example of a preorder that is not a partial order
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
Kazark / Alg.agda
Last active September 17, 2020 02:58
Basic definition of an algebra off the top of my head (not level-polymorphic) (without looking at stdlib)
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
Kazark / Point.agda
Created September 11, 2020 17:23
Cartesian Coordinate Pairs in the 2-Space of Naturals is a Partial Order, but not a Total Order
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
Kazark / Two.agda
Last active August 21, 2020 21:57
Lawfulness of applicative implementations than compile for homogenous pair
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
Kazark / FunctionalAbstractions.lhs
Created August 7, 2020 15:00
Exercises to familiarize yourself with many standard typeclasses
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
Kazark / Example.scala
Created August 5, 2020 19:09
Cats .widen (covariant functors) and .narrow (contravariant functors): both are for upcasts, and thus safe
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
Kazark / sqrt.scm
Created July 2, 2020 22:20
A playful implementation of square root in Guile, with a Haskell flavor
#| 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
Kazark / CurryHoward.lhs
Last active June 6, 2024 23:47
Curry-Howard Tutorial in Literate Haskell
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