jozefg

Operator P : (0).
[P(N)] =def= [natrec(N; unit; _._.void)].

Theorem one-not-zero : [not(=(zero; succ(zero); nat))] {
  auto;
  assert [P(succ(zero))];
  aux {
    unfold <P>; hyp-subst ← #1 [h.natrec(h; _; _._._)];
    reduce; auto
  };

jozefg

||| The proof of the halting problem here is pretty much
||| what you would expect, we apply the standard diagonalization
||| trick to prove that if we have a halting oracle there is a
||| program which both does and doesn't terminate.

Operator dec : (0).
[dec(M)] =def= [plus(M; not(M))].

Theorem has-value-wf : [{A : base} member(has-value(A); U{i})] {
  unfold <has-value>; auto

jozefg

signature COROUTINE =
sig
  type ('a, 'b, 'r) t

  val await : ('a, 'b, 'a) t
  val yield : 'b -> ('a, 'b, unit) t

  (* Monadic interface and stuffs *)
  val map    : ('c -> 'd) -> ('a, 'b, 'c) t -> ('a, 'b, 'd) t
  val return : 'c -> ('a, 'b, 'c) t

jozefg

signature TAG =
sig
  type tagged
  type 'a tag

  val new    : unit -> 'a tag
  val tag    : 'a tag -> 'a -> tagged
  val untag  : 'a tag -> tagged -> 'a option
end

jozefg

module realize where
open import Relation.Nullary
import Data.Unit as U
import Data.Empty as E
open import Data.Product
open import Data.Sum
open import Data.Nat

data Lam : Set where
  var : ℕ → Lam

jozefg

module realize where
open import Relation.Nullary
import      Data.Empty       as E
open import Data.Product
open import Data.Sum
open import Data.Nat

data Term : Set where
  var    : ℕ → Term
  lam    : Term → Term

jozefg

module ind-rec where
open import Data.Empty
open import Data.Product
open import Function
open import Level

record ⊤ {ℓ : Level} : Set ℓ where
  constructor tt

mutual

jozefg

#lang racket

;; This compiles some nontrivial subset of scheme with let, letrec, let*
;; quote, set!, and if to some subset of Scheme which is CPSed, has no
;; nested lambdas and is explicitly closure converted. Mostly done to stretch
;; my legs a bit with Racket.

(define *primops*
  '(+ - * / equal? < = and or not display cons car list box unbox set-box!))

jozefg

module Main where
import Control.Concurrent
import Control.Concurrent.STM
import Control.Exception
import Control.Monad

-- To start with, an intermezzo of the book's definition of Async and some key
-- operations on it.
data Async a = Async { pid :: ! ThreadId
                     , getAsync :: STM (Either SomeException a)

jozefg

{-# LANGUAGE FlexibleContexts #-}
module PickRandom where
import Data.List (group, sort)
import Control.Monad
import Control.Monad.Random (MonadRandom, getRandomR)
import qualified Control.Foldl as F

-- Pick a value uniformly from a fold
pickRandom :: MonadRandom m => a -> F.FoldM m a a
pickRandom a = F.FoldM choose (return (a, 0 :: Int)) (return . fst)