Skip to content

Instantly share code, notes, and snippets.

View maxsnew's full-sized avatar

Max S. New maxsnew

150 followers · 95 following
View GitHub Profile
@maxsnew
maxsnew / ChurchList.agda
Created April 12, 2024 17:13
Church Lists in Cubical Agda
module ChurchList where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
import Cubical.Data.List as List
open import Cubical.Data.List using (List)
private
variable ℓ : Level
@maxsnew
maxsnew / sexp.v
Created December 6, 2018 19:26
Decidable Equality for Sexpressions
Require Import Coq.Bool.Bool.
Inductive Sexp :=
| Atom : bool -> Sexp
| List : Forest -> Sexp
with
Forest :=
| Nil : Forest
| Cons : Sexp -> Forest -> Forest.
@maxsnew
maxsnew / equi-recursive-success.rkt
Last active July 25, 2018 20:01
Trying to encode a bidirectional lambda-calculus in Typed Racket with structural types
#lang typed/racket
(define-type Var String)
(define-type Type (U 'Base (List '-> Type Type)))
(define-type Ctx (Listof (Pair Var Type)))
(define-type Expr (U Var (List 'App Expr Term) (List 'Asc Type Term)))
(define-type Lam (List 'Lam Var Term))
(define-type Term (U Expr Lam))
(define-predicate lam? Lam)
@maxsnew
maxsnew / earlier.py
Created February 20, 2018 19:10
When should the type error happen?
def print_upper(s : str):
up_s = s.upper()
def printer(n : int):
acc = ""
for i in range(0,n):
acc += up_s
return acc
return printer
@maxsnew
maxsnew / gist:77bc24ad961e38553186
Created October 11, 2014 14:11
Scribble Interaction
[mnew:~CODE/racket/Redex-Enum-Paper]$ scribble --latex --dest x paper.scrbl (master)
[Output to x/paper.tex]
Warning: some cross references may be broken due to undefined tags:
(counter ("figure" "fig:benchmark-lines"))
(counter ("figure" "fig:benchmark-lines" "value"))
(counter ("figure" "fig:benchmark-overview"))
(counter ("figure" "fig:benchmark"))
(counter ("figure" "fig:correlation" "value"))
(counter ("figure" "fig:benchmark-overview" "value"))
(counter ("figure" "fig:benchmark" "value"))
@maxsnew
maxsnew / lifetime-error-fixed.rs
Last active August 29, 2015 14:07
Non-deterministic Lifetime Error
extern crate graphviz;
use graphviz as dot;
use std::str;
type Nd = uint;
type Ed = (uint, uint);
struct Graph<'a> {
nodes: Vec<&'a str>,
edges: Vec<Ed>,
@maxsnew
maxsnew / Request.elm
Created February 7, 2014 00:14
IO Request Serialization example
data Request = PutS String
| Exit Int
| GetS
port out : Signal (Maybe Request)
@maxsnew
maxsnew / Bug.html
Created February 6, 2014 23:51
Record Serialization Bug
<!DOCTYPE html>
<html>
<head>
<title>Test</title>
<script src="resources/elm-runtime.js"></script>
<script src="build/Ports.js"></script>
</head>
<body>
<h1>Test</h1>
<div id="bug"></div>
@maxsnew
maxsnew / gist:8217425
Created January 2, 2014 10:33
Elm profiling
Thu Jan 2 04:03 2014 Time and Allocation Profiling Report (Final)
elm +RTS -p -RTS --make blog/Interactive-Programming.elm
total time = 0.38 secs (1525 ticks @ 1000 us, 4 processors)
total alloc = 2,372,599,408 bytes (excludes profiling overheads)
COST CENTRE MODULE %time %alloc
MAIN MAIN 95.4 96.9
@maxsnew
maxsnew / gist:8168230
Created December 29, 2013 07:09
elm-repl hlint output
./Environment.hs:31:26: Warning: Redundant bracket
Found:
(show k) ++ ": " ++ p ++ "=" ++ v
Why not:
show k ++ ": " ++ p ++ "=" ++ v
./Environment.hs:37:1: Error: Eta reduce
Found:
reset compilerPath workingDirectory
= Repl compilerPath Map.empty Map.empty