Skip to content

Instantly share code, notes, and snippets.

MaiaVictor

Block or report user

Report or block MaiaVictor

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
View fm_micro_benchmark.md

stress.hs:

data Bits
  = Be
  | B0 Bits
  | B1 Bits
  deriving Show

data Pair a b
View debugging_life.txt
- implementei um garbage collector pro novo reduce()
- testei o gc e ele nao alterava o termo, entao parecia certo
- joguei o gc no reduce(), o resultado final deu errado
- como o reduce() funcionava sem o gc, deve ter algum caso onde o gc altera o programa
- dei um log em todas as chamadas do gc dentro do reduce() pra ver qual alterava o programa
- nenhuma, o gc estava funcionando impecavelmente bem
- se o gc nao altera o programa, como colocar ele dentro do reduce faz o reduce parar de funcionar? wtf?
- carreguei o reducer antigo no novo e, pra cada redução do novo, printei a reducao do antigo
- isso me levou ao exato loop onde o reducer novo fazia algo que alterava sua reducao final
- percebi que nesse loop, era uma aplicacao de um lambda que nao usava sua variavel
View equal.fm.js
// Equal.fm
// ========
//
// The propositional equality type. A value (proof) of type
// `Equal(A,a,b)` contains the reflexive constructor that
// `a` equals itself, which implies `b` is equal to `a` iff
// `b` reduces to `a`.
// Definition
// ----------
View parse.fm.js
import Maybe
import Nat
import String
import Unit
// Consumes a String and returns the rest and the parsed value, if any
Parser(A) : Type
(str : String) -> [: String, Maybe(A)]
// Å parser that just return some value
@MaiaVictor
MaiaVictor / scott_vs_usual.js
Last active Nov 13, 2019
Scott vs Usual encoded data in JavaScript, quick performance comparison
View scott_vs_usual.js
const scott = (() => {
const cons = (head, tail) => (got) => {
return got.cons(head, tail);
};
const nil = (got) => {
got.nil;
};
return {cons, nil};
View no.js
var arr = new ArrayBuffer(8);
var u32 = new Uint32Array(arr);
var f64 = new Float64Array(arr);
function show(u64) {
var bits = "";
for (var j = 0; j < 2; ++j) {
for (var i = 0; i < 32; ++i) {
bits += (u64[j] >>> (32 - i - 1)) & 1;
}
@MaiaVictor
MaiaVictor / using_js_nums_to_store_64bits.js
Last active Nov 7, 2019
Using JS numbers to store 64 bits losslesly
View using_js_nums_to_store_64bits.js
var arr = new ArrayBuffer(8);
var u32 = new Uint32Array(arr);
var f64 = new Float64Array(arr);
function show(u64) {
var bits = "";
for (var j = 1; j >= 0; --j) {
for (var i = 0; i < 32; ++i) {
bits += (u64[j] >>> (32 - i - 1)) & 1;
}
View aaa.js
// A program that doubles the size of a datatype with a known size (like Vectors)
// With direct, well-founded recursion (not allowed, but actually right):
mul2b : {s : Nat, n : Cat(s)} -> Cat(dbl(s))
case/Cat n
| csucc => csucc(succ(dbl(n.s)), csucc(dbl(n.s), mul2b(n.s, n.pred)))
| czero => czero
: Cat(dbl(n.n))
View Vect.fm
import Nat
import Fin
import Equal
Vect : {A : Type, n : Nat} -> Type
{i : Fin(%n)} -> A
nil : {~A : Type} -> Vect(A, 0n0)
{i} absurd(no_fin_zero(i), ~A)
View equality.md
syntax description
a == b A type asserting that a is equal to b
refl(~x) A proof that x == x
sym(~e) Given e : a == b, proves b == a
cong(~f, ~e) For any f, given e : a == b, proves f(a) == f(b)
t :: rewrite x in P(x) with e Given e : a == b and t : P(a), proves P(b)

Here, a == b is a type specifying that a is equal to b. It is not a proof, it is merely "a question". To prove it, you must construct a term x of type a == b. The only way to do it directly is with refl(~t), which proves that a term is equal to itself. That is, for any t, proves t == t. So, for example:

You can’t perform that action at this time.