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
View gist:efc17e810fb2c2bd57cd5a9a6251cd5d


const shift = ([ctor, term], inc, depth) => {
  switch (ctor) {

    case "Var":
      return Var(term.index < depth ? term.index : term.index + inc);

    case "Typ":
MaiaVictor /
Created Jul 30, 2019
propositional equality in Formality
T Eq <A : Type, a : A> {b : A}
| refl : Eq(A, a, a)
sym : {~A : Type, ~a : A, ~b : A, e : Eq(A, a, b)} -> Eq(A, b, a)
case<Eq> e
| refl => refl<A>(~a)
: Eq(A, b, a)
cong : {~A : Type, ~B : Type, ~a : A, ~b : A, ~f : {a : A} -> B, e : Eq(A, a, b)} -> Eq(B, f(a), f(b))
case<Eq> e
MaiaVictor /
Last active Jul 28, 2019
Formality FAQ - atualizado 27 de Julho de 2019

O que é o Formality?

Formality é uma linguagem de programação funcional em desenvolvimento, e que será lançada oficialmente ainda esse ano. Ela é uma linguagem bem "hardcore", com tipos dependentes e provas formais, inspirada em Haskell/Agda/Coq, mas com uma série de diferenciais, principalmente no que diz respeito ao runtime (optimal reductions, paralelismo, runtime fusion, etc.), visando combinar todo esse alto nível matemático com o potencial de ser realmente eficiente na prática. Essa é a carinha atual dela:

// Datatypes estilo Haskell

// O tipo de números naturais
T Nat
| succ {pred : Nat}
// With self-types, the λ-encoding of an inductive datatype coincides with its
// own inductive hypothesis. Because of that, induction is just identity!

// ::::::::::
// :: Bool ::
// ::::::::::

// data Bool : Set where
//   T : Bool
View formality_induction.js
// Congruence of equality
def cong
{~A : Type} =>
{~B : Type} =>
{~x : A} =>
{~y : A} =>
{~e : <x == y>} =>
{~f : {x : A} -> B} =>
rwt e <k @ <(f x) == (f k)>> $(f x)
MaiaVictor /
Last active Jul 2, 2019
Formality-Core tutorial

Formality-Core Tutorial

This tutorial aims to teach how to effectively develop Formality-Core code, assuming experience in functional programming languages, in special Haskell. Formality-Core is a minimal language based on elementary affine logic, making it compatible with optimal reductions. It can be seen as the GHC Core to the upcoming Formality language. Its minimalism, the lack of a type system, and its unusual boxed duplication system make it a very bare-bones language that isn't easy to work with directly, demanding that the programmer learns some delicate techniques to be productive.

1. Core features

Before proceeding, you should have Formality-Core installed, and be familiar with its core features and syntax. If you're not yet, please read the entire Language section of the wiki.

2. Algebraic Datatypes

View linear.agda
data Bool : Set where
true : Bool
false : Bool
data Nat : Set where
suc : Nat -> Nat
zer : Nat
data Vec (A : Set) : (n : Nat) -> Set where
MaiaVictor /
Last active Jun 29, 2019
Fast modular exponentiation with functional Nat due to optimal reductions

Fast modular exponentiation with Nat and optimal reductions

Functional programmers have a case of love and hate with the unary Nat type:

data Nat = Succ Nat | Zero

Love, because Nat is arguably the most intutive and mathematically elegant way to represent natural numbers. Hate, because it is so computationally slow that using it in practice is unfeasible. Imagine, for example, computing 123^1000 mod 137 with Nat. Just writing 123^1000 would need more terabytes than atoms in the universe, so that surely won't work. Or would it?

View gist:1efa2b241bccbc193fffaf7375017fd8
Hello! I'm looking for sprites in the Fire Emblem 7 style. Here are 3 references:
View shouldntbeapuzzle.agda
data FooBar (A : Set) (B : Set) : Set where
foo : A -> (A -> FooBar B A) -> FooBar A B
bar : B -> (B -> FooBar B A) -> FooBar A B
end : A -> B -> FooBar A B
data Pair (A : Set) (B : Set) : Set where
pair : (a : A) -> (b : B) -> Pair A B
get-snd : {A : Set} {B : Set} -> FooBar A B -> B
get-fst : {A : Set} {B : Set} -> FooBar A B -> A
You can’t perform that action at this time.