rntz

#include <stdio.h>
#define MAGIC 99586915107664152904966939075856564224.0

int main() {
    float x = MAGIC;
    if (x == 1.0/(1.0/x)) printf("float division involutive.\n");
    if (x != 1/(1/x)) printf("... but not with 1/(1/x).\n");
    double y = MAGIC;
    if (y == 1/(1/y)) printf("... but it is with doubles.\n");
    return 0;

rntz

-- The Datafun runtime.
module Runtime where

import qualified Data.Set as Set
import Data.Set (Set)

class Eq a => Preord a where
  (<:) :: a -> a -> Bool

class Preord a => Semilat a where

rntz

-- The axiom of choice is equivalent to the following schema:
--
--     (∀(a ∈ A) ∃(b ∈ B) P(a,b))
--     implies
--     ∃(f ∈ A → B) ∀(a ∈ A) P(a, f(a))
--
-- Here I give two interpretations of this statement into Agda's constructive
-- type theory:
--
-- 1. Interpreting ∃ "constructively" as Σ. Values of Σ come with a witness

rntz

#lang racket

(require syntax/parse/define)

;; Let's define a quasiquoter that generates contracts.
(define-for-syntax quasiquote-contract
  (syntax-parser
    #:literals (unquote unquote-splicing)
    [(_ name:id) #''name]
    [(_ ,x:expr) #'x]

rntz

(* Based on http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf *)
exception TypeError

type tp = Base | Fn of tp * tp
let subtype (x: tp) (y: tp): bool = x = y

type sym = {name: string; id: int}

let next_id = ref 0
let nextId() = let x = !next_id in next_id := x + 1; x

rntz

;; Based on http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf
#lang racket

;; Checks that a term has a type and returns its denotation.
(define (check cx tp-expect term)
  (match term
    [`(lambda (,x) ,body)
     (match-define `(-> ,A ,B) tp-expect)
     (define thunk (check (hash-set cx x A) B body))
     (lambda (env) (lambda (v) (thunk (hash-set env x v))))]

rntz

record Preorder (A : Set) : Set1 where
  field rel : (x y : A) → Set
  field ident : ∀{x} → rel x x
  field compo : ∀{x y z} → rel x y → rel y z → rel x z

open Preorder public

-- "indiscrete if P has a least element, discrete otherwise"
data Zub {A} (P : Preorder A) : A → A → Set where
  refl : ∀{x} → Zub P x x

rntz

#lang racket

;; The fringe of a tree is all the things in it that aren't conses - including
;; '(). For example, the fringe of '((1 . 2) ((3)) 4) is '(1 2 3 () () 4 ()).
(define example '((1 . 2) ((3)) 4))
(define example-fringe '(1 2 3 () () 4 ()))

;; (fringe tree) computes a "stream" of the fringe of a tree. In this case, a
;; "stream" is a function that takes a function getter and calls (getter elem
;; rest), where elem is the next element in the stream and rest is a stream of

rntz

postulate
  A : Set
  _≤_ : A → A → Set
  ⊥ : A
  _∨_ : A → A → A
  id : ∀{a} → a ≤ a
  _•_ : ∀{a b c} → a ≤ b → b ≤ c → a ≤ c

data Tree : Set where
  empty : Tree

rntz

{-# OPTIONS --postfix-projections #-}
open import Data.List using (List; []; _∷_; _++_)
open import Function using (flip)
open import Level
open import Relation.Binary using (Rel; _=[_]⇒_)
open import Relation.Binary.PropositionalEquality

module Reverse2 where

-- Some general abstract nonsense.