jcreedcmu

{-# OPTIONS --without-K #-}
module RtnzDatabase where

open import HoTT

Σ' = Σ -- renaming just so we can make the following syntax decl
syntax Σ' A (λ x → B) = ∃ x ∶ A · B

FinSet = Set -- not really constraining to finite, just conveying intent

jcreedcmu

I think I may have figured out the solution to a puzzle I put to
myself a few years ago, about generating random noise subject to some
particularly persnickety constraints.

Is there a random distribution of functions ℝ² → ℝ such that

(a) it's reasonably efficient to compute samples locally. Let's say we
can (after fixing a sample) that we can compute f(x, y) in constant
expected time.
(b) the distribution is rotation/translation invariant

jcreedcmu

{-# OPTIONS --without-K --rewriting #-}
module Parametricity where

-- This agda file contains my understanding/reconstruction/digestion of the ideas in
-- "A Presheaf Model of Parametric Type Theory" (Bernardy, Coquand, Moulin, 2015)
-- and Moulin's thesis
-- "Internalizing Parametricity"
-- http://publications.lib.chalmers.se/records/fulltext/235758/235758.pdf

open import HoTT hiding ( O; Path; _*_ ; !)

jcreedcmu

{-# OPTIONS --without-K #-}
module InternalCategories where

open import HoTT hiding ( [_] )

record Cat (X : Set) : Set₁ where
  constructor cat
  field
    hom : X → X → Set
    _⋆_ : {x y z : X} → hom x y → hom y z → hom x z

jcreedcmu

////////
// The vm module lets you run a string containing javascript code 'in
// a sandbox', where you specify a context of global variables that
// exist for the duration of its execution. This works more or less
// well, and if you're in control of the code that's running, and you
// have a reasonable protocol in mind// for how it expects a certain
// context to exist and interacts with it --- like, maybe a plug-in
// API for a program, with some endpoints defined for it that do
// useful domain-specific things --- your life can go smoothly.

jcreedcmu

const foo = {hello: "struff", q: {bar: "bar", baz: "baz"}};

type Replace<T, U> = {
  [P in keyof U]: U[P] extends string ? T : Replace<T, U[P]>;
}
type FooType = typeof foo;
type GenFoo<T> = Replace<T, FooType>;

function xform(input: GenFoo<string>): GenFoo<number> {

jcreedcmu

{-# OPTIONS --without-K --rewriting #-}
module Coglue {n : Set} where

open import HoTT hiding (Span ; S ; span=)

postulate
  # : Set
  ι : n → #

record Span : Set₁ where

jcreedcmu

type Union =
  { type: 'A', a: string } |
  { type: 'B', b: number }

type FilterType<T, K> = (T extends { type: K } ? T : never);
type RemoveType<T, K> = (T extends K ? never : T);

type MappedUnion = {[P in Union['type']]: RemoveTypeFromRecord<FilterType<Union, P>, 'type'>};

type MappedUnionTarget = {

jcreedcmu

type Rec = {
  'text': string,
  'bool': boolean
};

type Un =
  | {t: 'text', v: string}
  | {t: 'bool', v: boolean};

type Datum<K, V> = { t: K, v: V };

jcreedcmu

{-# OPTIONS --without-K #-}
module Cayley where

open import HoTT

-- The type of categories whose set of objects is X
record Cat (X : Set) : Set₁ where
  constructor cat
  field
    hom : X → X → Set