MonoidMusician

{-# OPTIONS --cubical --safe #-}
module Cubical.Parametricity where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma.Properties
open import Cubical.Foundations.Everything
open import Cubical.Data.Everything hiding (Iso ; compIso)

MonoidMusician

module Test.AppendOverlap where

import Data.Semigroup (class Semigroup, (<>))
import Data.Tuple (Tuple(..))
import Prim.Row (class Nub, class Union)
import Record (union)
import Unsafe.Coerce (unsafeCoerce)

unsafeSplit ::
  forall left right nubbed.

MonoidMusician

MonoidMusicianʼs Type Theory Musings

Welcome to my (un)scrambled thoughts on all things from the intersection of homotopy type theory, functional programming, and set theory! Thereʼs going to be a lot of terminology being thrown around, but donʼt be intimidated: hopefully Iʼll either describe the term, link to a definition/explanation, or youʼll be able to figure it out from context (or just skip it!). I do believe the best way to be clear is to be precise with language and to use established terminology, but because I am synthesizing pretty disparate areas of knowledge, most people wonʼt know all the terms.

My goal with these are to raise some new perspectives on common themes, and cross-pollinate these fields with each other.

MonoidMusician

import algebra.module

open list

-- The binomial coefficient, defined recursively on the natural numbers
def B : ℕ → ℕ → ℕ
| _ 0 := 1
| 0 _ := 0
| (n+1) (k+1) := B n (k+1) + B n k

MonoidMusician

-- This work by Nick Scheel is licensed under CC0 1.0
-- https://creativecommons.org/publicdomain/zero/1.0/

-- A basic framework for graph theory on multidigraphs in Lean
-- and a proof that no_watershed_condition is sufficient to
-- establish that a graph has a unique sink for each vertex
--
-- I hope to give some introduction to the syntax of how Lean works here,
-- but I assume some familiarity with functions, pattern matching,
-- type theory, and proofs.

MonoidMusician

module LeibnizGADT where

import Prelude

import Control.Monad.Eff.Exception.Unsafe (unsafeThrow)
import Data.Leibniz (type (~), coerce, coerceSymm, liftLeibniz, liftLeibniz1of2, liftLeibniz2of2, lowerLeibniz1of2, lowerLeibniz2of2, symm)
import Data.Tuple (Tuple(..))

-- Solution to https://www.reddit.com/r/purescript/comments/4x1jq3/approximating_gadts_in_purescript/d6bzlez/
data T a

MonoidMusician

-- | A change for a single key is an addition, removal, or update.
data MapChange v dv
  = Add v
  | Remove
  | Update dv

-- | A change for each possible key.
newtype MapChanges k v dv = MapChanges (Map k (MapChange v dv))

prune :: forall k v. Array (Tuple k (Maybe v)) -> Array (Tuple k v)

MonoidMusician

module Merging where

import Type.Row (class ListToRow, class RowListNub, class RowToList)

{-
exports.unsafeMerge = function(r1) {
  return function(r2) {
    var r = {};
    for (var k1 in r2) {
      if ({}.hasOwnProperty.call(r2, k1)) {

MonoidMusician

Questionable etymological reconstruction of Haskell into Latin via the great Wiktionary (Victiōnārium).

Haskell

1. An English patronymic surname derived from the Old Norse given name Áskell.
2. A Jewish surname derived from the equivalent of English Ezekiel.

Let’s go with #1, because #2 seems unlikely (even Ezekiel isn’t very common), and finding a cognate would most likely result in a boring Greek/Hebrew borrowing of Ezekiel (all the rage during post-classical periods especially – hellloo Ecclesiastical Latin).

Fun fact: Haskell was never a common given name and it died off in the 1930s: http://www.babynamewizard.com/voyager#prefix=haskell&sw=both&exact=true

MonoidMusician

module Main where

import Prelude
import Data.Maybe (Maybe(..), fromMaybe)
import Unsafe.Coerce (unsafeCoerce)

type Id = forall a. a -> a
newtype ID = ID Id

mkID :: Id -> ID