Kazark

module Guard

%default total
%access public export

data Guarded : (a -> Bool) -> a -> Type where
  Guard : (pred : a -> Bool) -> (subject : a) -> (prf : pred subject = True)
        -> Guarded pred subject

data GuardedIsBogus : Type where

Kazark

module AndOr

%default total
%access private

TData : Type -> Type -> Nat -> Type
TData a _ Z = a
TData a b (S Z) = (a, b)
TData _ b (S (S Z)) = b
TData _ _ _ = Void

Kazark

export PROMPT_COMMAND="__posh_git_ps1 '${debian_chroot:+($debian_chroot)}\[\033[01;32m\]\u@\h\[\033[01;34m\] \w' '\[\033[34m\]\$\[\033[00m\] '"

Kazark

#include <limits.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>

typedef struct MaybeULong {
  const unsigned long nothing;
  const unsigned long x;
} MaybeULong;

Kazark

module Bijection

%default total
%access public export

infixr 5 <=>

record (<=>) a p where
  constructor Biject
  ap : a -> p

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

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

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

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

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