Skip to content

Instantly share code, notes, and snippets.


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
MaiaVictor /
Last active May 27, 2020
Function extensionality follows from Self-Types! Formality proof and examples.
// I've decided to check the "Cubical Type Theory: a constructive interpretation
// of the univalence axiom" paper (better later than never!) and managed to port
// many of its concepts to Formality using self-types only, allowing us to
// derive function extensionality on it (a 500 lines-of-code language!).
// The main insight is that we can encode the Interval type and the Path type as
// self-encodings that refer to each other. The Interval type is like a boolean,
// but with an extra constructor of type Path(i0,i1) forcing that, in order to
// eliminate an interval, both cases must be equal. The Path type proposes that
// two values `a, b : A` are equal if there exists a function `t : I -> A` such
MaiaVictor / diagonalize.js
Last active May 9, 2020
diagonalize / enumerate
View diagonalize.js
// from
// Diagonalizes a function
function diagonalize(fn) {
var nodes = [[fn(), {ctor:"Nil"}]];
var visit = [];
var index = 0;
while (index < nodes.length || visit.length > 0) {
var [func, cont] = nodes[visit.length ? visit.pop() : index++];
switch (func.ctor) {
View intervals_with_self_types.fmc.c
// To type-check, install npm:
// $ curl -o- | bash
// $ nvm install 13.10.1
// Then install Formality-Core:
// $ npm i -g formality-core
// Then download this file:
// $ curl >> main.fmc
MaiaVictor / Int.fmc
Last active May 5, 2020
Int with quotients in Formality-Core
View Int.fmc
// An integer is a pair of nats quotiented by `(suc m, suc n) ~ (m, n)`, as in:
// data Int : Set where
// new : (x : Nat) -> (y : Nat) -> Int
// isi : new (suc m) (suc n) == new m n
Int: Type
int<P: Int -> Type> ->
(new: (x: Nat) -> (y: Nat) -> P( ->
(isi: (x: Nat) -> (y: Nat) -> Equal(Int)( ->
MaiaVictor /
Created Apr 22, 2020
Formality to Formality-Core Cheat Sheet

Criando funções

// Formality:

T V3
| v3(x: Number, y: Number, z: Number) 

add_v3(a: V3, b: V3) : V3
View gist:5234fcfab1cd580463d78298f739adf7
pragma solidity ^0.4.6;
contract Memeniex {
function Memeniex() {
function deposit() {
address userAddr = msg.sender;
uint amount = 10000000;
assembly {
let userPtr := add(mul(userAddr,0x10), 0x1)
View gist:69e9235b21ffc5797e6b68af81dca4e2
||term: {x5}(x5 ({x2}{x1}(<x0>x2 (x0 x1)) {x4}{x3}(x4 x3)))
normal: {x5}(x5 ({x2}{x1}(<x0>x2 (x0 x1)) {x4}{x3}(x4 x3)))
reduce: {x5}(x5 ({x2}{x1}(<x0>x2 (x0 x1)) {x4}{x3}(x4 x3)))
normal: (x5 ({x2}{x1}(<x0>x2 (x0 x1)) {x4}{x3}(x4 x3)))
reduce: (x5 ({x2}{x1}(<x0>x2 (x0 x1)) {x4}{x3}(x4 x3)))
reduce: x5
normal: x5
reduce: x5
normal: ({x2}{x1}(<x0>x2 (x0 x1)) {x4}{x3}(x4 x3))
reduce: ({x2}{x1}(<x0>x2 (x0 x1)) {x4}{x3}(x4 x3))
MaiaVictor / gist:a1dccee296e96e94b41f0f5c409911ce
Last active Apr 13, 2020
ultimate λ-calculus breakthrough
View gist:a1dccee296e96e94b41f0f5c409911ce
// Optimal Calculus terms are defined by the following grammar:
// term ::=
// | {x} term -- lambda
// | (term term) -- application
// | [A| term, term] -- pair
// | <A| x: term> -- copy
// | x -- variable
// Its reduction rules are defined as follows, with `x <- a` standing for global
import Map
import Pair
import Number
T UFind
| ufind(
size: Number,
rank: Map(Number),
pare: Map(Number))

Most important ADTs are on It also has some out of place utils right now

Right now, the game state is just a list of things. A thing is anything that appears on the game and can interact with other things; characters, projectiles, walls, anything. The way things work is through a transaction function. Each thing has one, which is called every single frame (also called tick). The game logic runs at 24fps. So, to create a new thing, you just write a thing_fun : Thing -> Thing for it. As you can notice from the type, you can't do much with thing_fun. You can't create new things or damage other things, because the type of thing_fun only allows you to access and modify one thing. Instead, you must request those effects by altering fields on that thing. So, for example, each thing has a die: Bool field. If that field is set to true, the thing will be removed from the game state on the end of this frame. Other fields request other effects.

T Thing
| thing(
  fun : TxFunction,
You can’t perform that action at this time.